working on prover

doc/proving.md

@@ -216,7 +216,7 @@ A note on matching. There may be many ways to match a given proof goal
 to the conclusion of a rule. Different matches can result in different
 sub-goals, which may affect whether a proof succeeds. IVy doesn't
 attempt to verify that the match it finds is unique. For this
-reasing, when sub-goals are produced, it may be a good idea to give
+reason, when sub-goals are produced, it may be a good idea to give
 the match explicitly (as we did above, though in this case there is
 only one match).
 
@@ -238,7 +238,7 @@ definitional schema. As an example, consider the following schema:
 This schema shows how to construct a fresh function `fun` from two functions:
 
 - `base` gives the value of the function for inputs less than or equal to zero.
-- `step` gives the value for positive *X* in terms of `X` and the value for `X-1`
+- `step` gives the value for positive *X* in terms of *X* and the value for *X*-1
 
 A definition schema such as this requires that the defined function
 symbol be fresh. With this schema, we can define a recursive function that
@@ -332,7 +332,7 @@ Naming
 If we can prove that something exists, we can give it a name. That is,
 we can reason according to this schema:
 
-    schema naming = {
+    schema existsE = {
         type t
 	relation p(X:t)
         property exists X. p(X)
@@ -346,19 +346,20 @@ This rule gives a name to a value satisfying *p*, provided we can show that such
     property exists Y. succ(X,Y)
 
     function next(X:t):t
+
     property succ(X,next(X))
-    proof naming with n = next(X), p(Y) = succ(X,Y)
+    proof existsE with n = next(X), p(Y) = succ(X,Y)
 
-This generates a proof goal `exists Y. succ(X,Y)` that is discharged by `auto` using the property above.
+This generates a proof goal `exists Y. succ(X,Y)` that is discharged
+by `auto` using the property above.
 
-This kind of argument is common enough that IVy provides a shorthand for it:
+This kind of argument is common enough that IVy provides a shorthand
+for it:
 
-    function next(X:t):t
     property exists Y. succ(X,Y) named next(X)
 
 This transforms the property to `succ(X,next(X))`, provided `next` is
-fresh. Readers familiar with logic may recognize this transformation as
-"Skolemization".
+new. Readers may recognize this transformation as "Skolemization".
 
 
 Hierarchical proof development
@@ -411,12 +412,12 @@ Now suppose we want to prove an extra property using `t_theory`:
         property [prop] f(f(X)) > X
 
     }
-    with t_theory.expanding, t_theory.transivity
+    with t_theory.expanding, t_theory.transitivity
 
 The 'with' clause says that the properties `expanding` and
 `transitivy` from isolate `t_theory` should be included in the context when
 proving `extra.prop`. The interpretation of *t* as the integers
-and the definiton of *f* as the successor function will be ignored.
+and the definiton of *f* as the successor function are ignored.
 
 Exporting properties
 --------------------

examples/ivy/indexset2.ivy

@@ -0,0 +1,189 @@
+#lang ivy1.6
+
+# Here, we prove a basic fact about finite sets: is X and Y are disjoint
+# subsets of S, then |X| + |Y| <= |S|. This can be used to show that any two
+# majorities of S have an element in common.
+
+# We set up the problem with two types: the *basis* type and the
+# *index* type, both isomorphic to the integers. Our sets are subsets
+# of the basis type, while their cardinalities a members of the index
+# type. In other words ordinals are in basis, while cardinals are in
+# index. The separation of these two types is used to avoid
+# non-stratified functions.
+
+# We definte a module that takes basis and index types, and provides the following
+# interface:
+
+# 1) a type *set* representing finite subsets of the basis type
+# 2) a basis element *n* that is an upper bound on set elements (so the basis is finite)
+# 3) a *member* relation
+# 4) a relation *disjoint* beteween sets
+# 5) a function *card* giving the cardinality of a set as an index
+# 6) a function *cnt* gives the cardinality of the basis elements less than E
+# 7) an action `empty` returning the empty set
+
+# The spec can then be stated as disjoint(X,Y) -> card(X)+card(Y) <= cnt(n).
+
+# The implementation defines card and cnt recursively over the basis type. Ideally, the
+# basis type should provide a recursion schema, but here we just give the instantions
+# of the recursion schema as axioms.
+
+# We then give an inductive invariant with parameter B. This states that the theorem holds
+# for elements of the sets X and Y less than B. We then instantiate the induction schema for
+# basis using the invariant.
+
+# This all seems straightforward, but it was tricky to figure out how to set up the problem
+# without function cycles. Also, see the comment below about integer arithmetic. For the
+# basis type, we used the succesor relation to avoid using airthmetic on this type.
+
+include collections
+include order
+
+module indexset(basis,index) = {
+
+    type set 
+
+    individual n : basis.t
+    relation member(E:basis.t,S:set)
+    function card(S:set) : index.t
+    relation majority(S:set)
+
+    action empty returns(s:set)
+    action add(s:set,e:basis.t) returns (s:set)
+
+    axiom [n_positive] n > 0
+
+    object spec = {
+
+	property majority(X) & majority(Y) -> exists E. (member(E,X) & member(E,Y))
+
+	after empty {
+	    assert ~member(E,s);
+	}
+
+	after add {
+	    assert member(X,s) <-> (member(X,old s) | X = e)
+	}
+    }
+
+    isolate succ_fact = {
+    	object spec = {
+    	    property basis.succ(X:basis.t,Y:basis.t) <-> (Y-1 = X)
+    	}
+    }
+    with basis.impl
+
+    function cnt(E:basis.t) : index.t
+    function cardUpTo(S:set,B:basis.t) : index.t
+
+    isolate counting = {
+
+
+    	object spec = {
+
+    	    property [cnt_base] cnt(0) = 0
+    	    property [cnt_step] F > 0 & basis.succ(E,F) -> cnt(F) = cnt(E) + 1
+
+    	    property [cardUpTo_base] cardUpTo(S,0) = 0
+    	    property [cardUpTo_step] basis.succ(B,BS) & BS > 0 ->
+    					cardUpTo(S,BS) = cardUpTo(S,B)+1 if member(B,S) else cardUpTo(S,B)
+    	}
+
+    	object impl = {
+
+    	    definition cnt(X) = 0 if X <= 0 else cnt(X-1) + 1
+    	    proof rec[basis.t]
+
+    	    definition cardUpTo(S,B) =
+    		0 if B <= 0 else (cardUpTo(S,B-1)+1 if member(B-1,S) else cardUpTo(S,B-1))
+    	    proof rec[basis.t]
+
+    	}
+    } with basis.spec.transitivity, basis.spec.antisymmetry, basis.spec.totality, succ_fact,nodeset.n_positive
+
+    relation disjoint(X:set,Y:set)
+
+    isolate disjointness = {
+
+    	object spec = {
+
+
+    	    definition disjoint(X,Y) = forall E. ~(member(E,X) & member(E,Y))
+
+    	    property disjoint(X,Y) -> card(X) + card(Y) <= cnt(n)
+
+    	}
+
+    	object impl = {
+    	    derived inv(X,Y,B) = 
+    		disjoint(X,Y) -> cardUpTo(X,B) + cardUpTo(Y,B) <= cnt(B)
+
+    	    property exists L. (L >= 0 & forall B. (B >= 0 & ~inv(X,Y,B) -> ~inv(X,Y,L) & L <= B))
+    	    named lerr(X,Y)
+    	    proof lep[basis.t]
+
+    	    object succ_lemma = {
+    		object spec = {
+    		    property [induc] exists E. basis.succ(E,lerr(X,Y))
+    		}
+    		isolate iso = spec with succ_fact
+    	    }
+
+    	    definition card(S) = cardUpTo(S,n)
+
+    	    interpret index.t -> int
+    	}
+
+    }
+    with counting,basis
+
+
+    object impl = {
+
+    	object spec = {
+
+    	definition majority(X) = 2 * card(X) > cnt(n)
+
+    	# tricky: we interpret the index type as the integers, so we can use addition
+    	# without axioms. we have set up the above so the index type is never the domain of
+    	# a function. a bug in IVy's logic fragmetn checker seems to allow us to get away with this,
+    	# and it works, but I don't know if Z3 is actually a decision procedure for this case.
+
+    	interpret index.t -> int
+
+    	# Here is the implementation of the set type using an unsorted array. The above reasoning
+    	# is actually independent of the definition of "member" below. Hopefully, this definition
+    	# will not confuse Z3. If it did, we would have to put these definitions into their own isolate.
+
+    	instance arridx : unbounded_sequence
+    	instance arr:array(arridx.t,basis.t)
+
+    	# Tricky: this is a bit of aspect-orientation. It turns the type `set` into a struct
+    	# with just one field called `repr`. This field gives the concrete representation of a
+    	# set as an array. To an isolate the doesn't use the definition of `member` below,
+    	# the tpye `set` will still appear to be uninterpreted.
+
+    	destructor repr(X:set) : arr.t
+
+    	definition member(y:basis.t,X:set) = exists Z. 0 <= Z & Z < repr(X).end & repr(X).value(Z) = y
+
+    	implement empty {
+    	    repr(s) := arr.create(0,0)
+    	}
+
+    	implement add {
+    	    if ~member(e,s) {
+    		repr(s) := repr(s).resize(repr(s).end.next,e)
+    	    }
+    	}
+    }
+    }
+}
+
+
+instance nodeord : unbounded_sequence
+instance nodecard : unbounded_sequence
+instance nodeset : indexset(nodeord,nodecard)
+
+isolate iso_n = nodeset with nodeord,nodecard
+

ivy/include/order.ivy

@@ -1,9 +1,9 @@
 #lang ivy1.6
 
 module totally_ordered(t) = {
-    property (T:t < U & U < V) -> (T < V)
-    property ~(T:t < U & U < T)
-    property T:t < U | T = U | U < T
+    property [transitivity] (T:t < U & U < V) -> (T < V)
+    property [antisymmetry] ~(T:t < U & U < T)
+    property [totality] T:t < U | T = U | U < T
 }
 
 module totally_ordered_with_zero(t) = {

ivy/ivy_ast.py

@@ -531,6 +531,7 @@ def name(self):
     def defines(self):
         return [(c.defines(),lineno(c)) for c in self.args]
 
+
 class SchemaBody(AST):
     def __str__(self):
         return '{\n' + '\n'.join(str(arg) for arg in self.args) + '}\n'

ivy/ivy_check.py

@@ -95,8 +95,6 @@ def check_module():
 
     missing = []
 
-    for x,y in im.module.isolates.iteritems():
-        print 'isolate= {}:{} '.format(x,y)
     isolate = ivy_compiler.isolate.get()
     if isolate != None:
         isolates = [isolate]