stashing again

doc/proving.md

@@ -112,9 +112,9 @@ have these symbols in their signature).
 Schemata
 ========
 
-A *schema* is a compound judgment that a collection of judgments as
-input (the premises) and produces a judgment as output (the
-conclusion). The meaning of schema is that we can provide any
+A *schema* is a compound judgment that takse a collection of judgments
+as input (the premises) and produces a judgment as output (the
+conclusion). If the schema is valid, then we can provide any
 type-correct values for the premises and the conclusion will follow.
 
 Here is a simple example of a schema taken as an axiom:
@@ -124,17 +124,22 @@ Here is a simple example of a schema taken as an axiom:
 	type r
         function f(X:d) : r
         #--------------------------
-        property X=Y -> f(X) = f(Y)
+        property X = Y -> f(X) = f(Y)
     }
 
 The schema is contained in curly brackets and gives a list of premises
 following a conclusion. In this case, it says that, given types *d* and *r* and a function *f* from
-*d* to *r*, we can infer that, for all *X*,*Y*, *X*=*Y* implies
+*d* to *r* and any values *X*,*Y* of type *d*,  we can infer that *X*=*Y* implies
 *f*(*X*) = *f*(*Y*). The dashes separating the premises from the conclusion are
 just a comment. The conclusion is always the last judgement in the rule.
 
-The keyword `axiom` tells IVy that this rule should be taken as
-primitive, without proof. 
+The keyword `axiom` tells IVy that this rule should be taken as a
+given, without proof. However, as we will see, the default `auto`
+tactic treats a schema differently from a simple proposition. That is,
+a schema is never used by default, but instead must be explicitly
+instantiated.  This allows is to express and use facts that, if they
+occerred in a verification condition, would take us outside the
+decidable fragment.
 
 Any judgment that has been admitted in the current context can be
 *applied* in a proof. When we apply a schema, we supply values for its
@@ -159,7 +164,7 @@ discovers the following assignment:
 After plugging in this assignment, the conclusion of the rule exactly matches
 the property to be proved, so the property is admitted.
 
-The problem of finding an assignment such as the one above is called
+The problem of finding an assignment such as the one above is one of
 "second order matching".  It is a hard problem, and the answer is not
 unique. In case IVy did not succeed in finding the above match, we
 could also write the proof more explicitly, like this:
@@ -167,11 +172,12 @@ could also write the proof more explicitly, like this:
     proof
         apply congruence with d=t, r=t, X=Z, Y=n, f(N)=N+1
 
-Each of the above equations acts as a constraint on the assignment. That is,
-it must convert *d* to *t*, *r* to *t*, *X* to *Z* and so on. By giving such equations,
-we can narrow the possibilities down to just one assignment. We don't have to do this,
-however. We can also give a subset of the desired assignment, relying on Ivy's
-matching algorithm to fill in the rest.
+Each of the above equations acts as a constraint on the
+assignment. That is, it must convert *d* to *t*, *r* to *t*, *X* to
+*Z* and so on. By giving such equations, we can narrow the
+possibilities down to just one assignment. Alternatively, we can also
+give a subset of the desired assignment, relying on Ivy's matching
+algorithm to fill in the rest.
 
 It's also possible to write constraints that do not allow for any
 assignment. In this case, Ivy complains that the provided match is
@@ -273,22 +279,126 @@ Theorems
 --------
 
 Thus far, we have seen schemata used only as axioms. However, we can also
-prove the validity of a schema as a *theorem*. Here's a simple example:
+prove the validity of a schema as a *theorem*. For example, here is a theorem
+expressing the transitivity of equality:
 
-    theorem [simple] {
+    theorem [trans] {
+        type t
+        property X:t = Y
+        property Y:t = Z
+        #--------------------------------
+        property X:t = Z
+    }
+
+We don't need a proof for this, since the `auto` tactic can handle it. Here is a rule
+for eliminating existential quantifiers:
+
+theorem [elimA] {
+    type t
+    function p(X:t) : bool
+    property forall Y. p(Y)
+    #--------------------------------
+    property p(X)
+}
+
+It says, for any predicate *p*, if `p(Y)` holds for all *Y*, then
+`p(X)` holds for a particular *X*. Again, the `auto` tactic can prove
+this. Now let's derive a consequence of these facts. A function *f* is
+*idempotent* if applying twice gives the same result as applying it
+once. This theorem says that, if *f* is idempotent, then applying three
+times is the same as applying it once:
+
+    theorem [idem2] {
         type t
         function f(X:t) : t
-        property forall X. f(f(x)) = f(x)
+        property forall X. f(f(X)) = f(X)
         #--------------------------------
-        
+        property f(f(f(X))) = f(X)
+    }
+
+The auto tactic can't prove this because the presmise contains a
+function cycle with a universally quantified variable. Here's the
+error message it gives:
+
+    error: The verification condition is not in logic epr.
+
+    Note: the following functions form a cycle:
+      function f(V0:t) : t
+
+This means we'll need to apply some other tactic. Here is one possible proof:
+
+    proof
+        apply trans with Y = f(f(X));
+        apply elimA with X = f(X);
+        apply elimA with X = X
+
+We think this theorem holds because `f(f(f(X)))` is equal to `f(f(X))`
+(by idempotence of *f*) which in turn is equal to `f(X)` (again, by
+idempotence of *f*). This means we want to apply the transitivy rule, where
+the intermediate term *Y* is `f(f(x))`. Notice we have to give the value of *Y*
+explicitly. Ivy isn't clever enough to guess this intermediate term for us.
+This gives us the following two proof subgoals:
+
+    theorem [prop2] {
+        type t
+        function f(V0:t) : t
+        property [prop5] forall X. f(f(X)) = f(X)
+        #----------------------------------------
+        property f(f(f(X))) = f(f(X))
+    }
+
+
+    theorem [prop3] {
+        type t
+        function f(V0:t) : t
+        property [prop5] forall X. f(f(X)) = f(X)
+        #----------------------------------------
+        property f(f(X)) = f(X)
+    }
+
+Now we see the the conclusion in both cases is an instance of the
+idempotence assumption, for a particular value of *X*. This means
+we can apply the `elimA` rule that we proved above. In the first case,
+the value of `X` for which we are claiming idempotence is `f(X)`.
+With this assignment, IVy can match `p(X)` to `f(f(f(X))) = f(X)`.
+Thi substituion produces a new subgoal as follows:
+
+    theorem [prop2] {
+        type t
+        function f(V0:t) : t
+        property [prop5] forall X. f(f(X)) = f(X)
+        #----------------------------------------
+        property forall Y. f(f(f(Y))) = f(f(Y))
+    }
+
+This goal is trivial, since the conclusion is exactly the same as one
+of the premises, except for the names of bound variables. Ivy proves
+this goal automatically and drops it from the list. This leaves the
+second subgoal `prop3` above. We can also prove this using `elimA`. In
+this case `X` in the `elimA` rule corresponds to `X` in our goal.
+Thus, we write `apply elimA with X = X`. This might seem a little
+strange, but keep in mind that the `X` on the left refers to `X` in
+the `elimA` rule, while `X` on the right refers to `X` in our goal. It
+just happens that we chose the same name for both variables.
+
+Ance again, the subgoal we obtain is trivial and Ivy drops it. Since
+there are no more subgoals, the proof is now complete.
+
+# ### The deduction library
+
+Facts like `trans` and `elimA` above are included in the library
+`deduction`. This library contains a complete set of rules of a system
+[natural deduction](https://en.wikipedia.org/wiki/Natural_deduction)
+for first-order logic with equality.
+
 
 Recursion
 ---------
 
 Recursive definitions are permitted in IVy by instantiating a
-definitional schema. As an example, consider the following axiom schema:
+*definitional schema*. As an example, consider the following axiom schema:
 
-    axiom [ rec[t] ] {
+    axiom [rec[t]] {
 	type q
 	function base(X:t) : q
 	function step(X:q,Y:t) : q
@@ -307,17 +417,27 @@ symbol be fresh. With this schema, we can define a recursive function that
 adds the non-negative numbers less than or equal to *X* like this:
 
     function sum(X:t) : t
-    definition sum(X:t) = 0 if X <= 0 else (X + sum(X-1))
+
+    definition [defsum] {
+       sum(X:t) = 0 if X <= 0 else (X + sum(X-1))
+    }
     proof
        apply rec[t]
 
-IVy matches this definition to the schema `rec[t]` with the following
-assignment:
+Notice that we wrote the definition as a schema rather than a simple
+proposition.  This is because it has a universally quantified variable
+`X` under arithmetic operators, which puts it outside the decidable
+fragment. Becuase this definitoin is a schema, when we want to use it,
+we'll have to apply it explicitly,
+
+In order to admit this definition, we applied the definition
+schema `rec[t]`. Ivy infers the following assignment:
 
     q=t, base(X) = 0, step(X,Y) = Y + X, fun(X) = sum(X)
 
 This allows the recursive definition to be admitted, providing that
-`sum` is fresh in the current context.
+`sum` is fresh in the current context (i.e., we have not previously refered to
+`sum` except to declare its type).
 
 When we instantiate a theory, it generally comes with a recursion
 schema for the given type.  For example, if we say:
@@ -332,12 +452,13 @@ Suppose we want to define a function that takes an additional
 parameter. For example, before summing, we want to divide all the
 numbers by *N*. We can define such a function like this:
 
-    definition sumdiv(N,X) = 0 if X <= 0 else (X/N + sumdiv(N,X-1))
+    definition [defsumdiv]
+        sumdiv(N,X) = 0 if X <= 0 else (X/N + sumdiv(N,X-1))
     proof
        apply rec[t]
 
-In matching the recursion schema `rec[t]`, IVy will extend the free
-function symbols in the schema with an extra parameter *N* so that
+In matching the recursion schema `rec[t]`, IVy will extend the
+function symbols in the premises of `rec[t]` with an extra parameter *N* so that
 schema becomes:
 
     axiom [ rec[t] ] = {
@@ -354,9 +475,11 @@ The extended schema matches the definition, with the following assignment:
     q=t, base(N,X)=0, step(N,X,Y)=Y/N+X, fun(N,X) = sum2(N,X)
     
 This is somewhat as if functions were "curried", in which case the
-free symbol `fun` would match the term `sum2 N`. The upshot of this is
-that to match the recursion schema, a function definition must be
-recursive in its last parameter.
+free symbol `fun` would match the curried function term `sumdiv N`.
+Since Ivy's logic doesn't allow for partial application of functions,
+extended matching provides an alternative. Notice that, 
+to match the recursion schema, a function definition must be
+recursive in its *last* parameter.
 
 Induction
 ---------
@@ -386,6 +509,14 @@ This produces two sub-goals, a base case and an induction step:
     property X <= 0 -> sum(X) <= X
     property sum(X) <= X -> sum(X+1) <= X + 1
 
+Unfortunately, the `auto` tactic can't prove these goals using the
+definition of `sum`, because this definition is a schema. Fortunately,
+it suffices to instantiate this schema just for the specific `X`
+in our subgoals. 
+
+Because the definition of `sum` is problematic in this way.
+
+
 The `auto` tactic can prove both of these using the definition of
 `sum`, if we allow it to use undecidable theories. Later, we'll see a
 more reliable way to do this, however.

ivy/ivy_ast.py

@@ -137,6 +137,9 @@ class Definition(Formula):
             return Atom(equals,self.args)
         return Iff(*self.args)
 
+class DefinitionSchema(Definition):
+    pass
+
 class Implies(Formula):
     """
     Implication of formulas

ivy/ivy_compiler.py

@@ -628,6 +628,7 @@ def compile_action_def(a,sig):
 def compile_defn(df):
     has_consts = any(not isinstance(p,ivy_ast.Variable) for p in df.args[0].args)
     sig = ivy_logic.sig.copy() if has_consts else ivy_logic.sig
+    is_schema = isinstance(df,ivy_ast.DefinitionSchema)
     with ivy_ast.ASTContext(df):
         with sig:
             for p in df.args[0].args:
@@ -653,6 +654,9 @@ def compile_defn(df):
                     eqn = ivy_ast.Atom('=',(df.args[0],df.args[1]))
                     eqn = sortify_with_inference(eqn)
                     df = ivy_logic.Definition(eqn.args[0],eqn.args[1])
+            if is_schema:
+                df = ivy_logic.DefinitionSchema(*df.args)
+                iu.dbg('type(df)')
             return df
     
 def compile_schema_prem(self,sig):
@@ -870,6 +874,7 @@ class IvyDomainSetup(IvyDeclInterp):
     def definition(self,ldf):
         label = ldf.label
         df = ldf.formula
+        iu.dbg('type(df)')
         df = compile_defn(df)
         self.add_definition(ldf.clone([label,df]))
         self.domain.updates.append(DerivedUpdate(df))
@@ -1351,7 +1356,7 @@ def check_properties(mod):
         return prop
             
     import ivy_proof
-    prover = ivy_proof.ProofChecker(mod.labeled_axioms,[],mod.schemata)
+    prover = ivy_proof.ProofChecker(mod.labeled_axioms,mod.definitions,mod.schemata)
 
     for prop in props:
         if prop.id in pmap:

ivy/ivy_lexer.py

@@ -185,7 +185,7 @@ def t_SYMBOL(t):
     return t
 
 def t_LABEL(t):
-    r'\[[_a-zA-Z0-9]+\]'
+    r'\[[_a-zA-Z0-9\]\[]+\]'
     t.type = reserved.get(t.value,'LABEL')
     return t
 

ivy/ivy_logic.py

@@ -247,6 +247,8 @@ class Definition(AST):
     def __eq__(self,other):
         return type(self) is type(other) and all(x == y for (x,y) in zip(self.args,other.args))
 
+class DefinitionSchema(Definition):
+    pass
 
 
 lg_ops = [lg.Eq, lg.Not, lg.Globally, lg.Eventually, lg.And, lg.Or, lg.Implies, lg.Iff, lg.Ite, lg.ForAll, lg.Exists, lg.Lambda, lg.NamedBinder]

ivy/ivy_module.py

@@ -140,7 +140,8 @@ class Module(object):
         for ldf in self.definitions:
             cnst = ldf.formula.to_constraint()
             if all(isinstance(p,il.Variable) for p in ldf.formula.args[0].args):
-                theory.append(cnst) # TODO: make this a def?
+                if not isinstance(ldf.formula,il.DefinitionSchema):
+                    theory.append(cnst) # TODO: make this a def?
         # extensionality axioms for structs
         for sort in sorted(self.sort_destructors):
             destrs = self.sort_destructors[sort]

ivy/ivy_parser.py

@@ -842,12 +842,43 @@ def p_optproof_symbol(p):
     'optproof : PROOF proofstep'
     p[0] = p[2]
     
-def p_top_definition_defns(p):
-    'top : top DEFINITION defns optproof'
-    p[0] = p[1]
-    p[0].declare(DefinitionDecl(*[addlabel(mk_lf(x),'def') for x in p[3]]))
-    if p[4] is not None:
-        p[0].declare(ProofDecl(p[4]))
+if iu.get_numeric_version() <= [1,6]:
+    def p_top_definition_defns(p):
+        'top : top DEFINITION defns optproof'
+        p[0] = p[1]
+        p[0].declare(DefinitionDecl(*[addlabel(mk_lf(x),'def') for x in p[3]]))
+        if p[4] is not None:
+            p[0].declare(ProofDecl(p[4]))
+else:
+
+    def p_optlabel_label(p):
+        'optlabel : LABEL'
+        p[0] = Atom(p[1][1:-1],[])
+        p[0].lineno = get_lineno(p,1)
+
+    def p_optlabel(p):
+        'optlabel : '
+        p[0] = None
+
+    def p_gdefn_defn(p):
+        'gdefn : defn'
+        p[0] = p[1]
+
+    def p_gdefn_lcb_defn_rcb(p):
+        'gdefn : LCB defn RCB'
+        p[0] = DefinitionSchema(*p[2].args)
+        p[0].lineno = p[2].lineno
+
+    def p_top_definition_optlabel_gdefn_optproof(p):
+        'top : top DEFINITION optlabel gdefn optproof'
+        lf = LabeledFormula(p[3],p[4])
+        lf.lineno = get_lineno(p,2)
+        iu.dbg('type(lf.formula)')
+        p[0] = p[1]
+        p[0].declare(DefinitionDecl(addlabel(lf,'def')))
+        if p[5] is not None:
+            p[0].declare(ProofDecl(p[5]))
+
 
 def p_top_progress_defns(p):
     'top : top PROGRESS defns'

ivy/ivy_proof.py

@@ -41,7 +41,7 @@ class ProofChecker(object):
         """
     
         self.axioms  = list(axioms)
-        self.definitions = dict((d.formula.defines(),d) for d in definitions)
+        self.definitions = dict((d.formula.defines().name,d) for d in definitions)
         self.schemata = schemata.copy() if schemata is not None else dict()
         for ax in axioms:
             self.schemata[ax.name] = ax
@@ -56,7 +56,7 @@ class ProofChecker(object):
         """
 
         sym = defn.formula.defines()
-        if sym in self.definitions:
+        if sym.name in self.definitions:
             raise Redefinition(defn,"redefinition of {}".format(sym))
         if sym in self.deps:
             raise Circular(defn,"symbol {} defined after reference".format(sym))
@@ -71,7 +71,7 @@ class ProofChecker(object):
                 raise NoMatch(defn,"recursive definition does not match the given schema")
         else:
             subgoals = []
-        self.definitions[sym] = defn
+        self.definitions[sym.name] = defn
         
     def admit_proposition(self,prop,proof=None):
         """ Admits a proposition with proof.  If a proof is given it
@@ -141,9 +141,14 @@ class ProofChecker(object):
 
     def setup_matching(self,decl,proof):
         schemaname = proof.schemaname()
-        if schemaname not in self.schemata:
+        if schemaname in self.schemata:
+            schema = self.schemata[schemaname]
+        elif schemaname in self.definitions:
+            schema = self.definitions[schemaname]
+            schema = clone_goal(schema,goal_prems(schema),goal_conc(schema).to_constraint())
+        else:
+            iu.dbg('self.definitions.keys()')
             raise ProofError(proof,"No schema {} exists".format(schemaname))
-        schema = self.schemata[schemaname]
         schema = rename_goal(schema,proof.renaming())
         schema = transform_defn_schema(schema,decl)
         prob = match_problem(schema,decl)

ivy/ivy_theory.py

@@ -287,10 +287,11 @@ def get_assumes_and_asserts(preconds_only):
             assumes.append((foo,action))
         
     for ldf in im.module.definitions:
-        if ldf.formula.defines() not in ilu.symbols_ast(ldf.formula.rhs()):
-            macros.append((ldf.formula.to_constraint(),ldf))
-        else: # can't treat recursive definition as macro
-            assumes.append((ldf.formula.to_constraint(),ldf))
+        if not isinstance(ldf.formula,il.DefinitionSchema):
+            if ldf.formula.defines() not in ilu.symbols_ast(ldf.formula.rhs()):
+                macros.append((ldf.formula.to_constraint(),ldf))
+            else: # can't treat recursive definition as macro
+                assumes.append((ldf.formula.to_constraint(),ldf))
 
     for ldf in im.module.labeled_axioms:
         if not ldf.temporal:

test/ind1.ivy

@@ -5,11 +5,17 @@ interpret t -> int
 
 function sum(X:t) : t
 
-definition sum(X:t) = 0 if X <= 0 else (X + sum(X-1))
+definition [def_sum] {
+    sum(X:t) = 0 if X <= 0 else (X + sum(X-1))
+}
 proof
     apply rec[t]
 
-property sum(Y) >= Y
+property sum(X) >= X
 proof
-    apply ind[t] with X = Y;
+    apply ind[t];
+    assume sum;
+    defergoal;
+    assume sum;
     showgoals
+