stashing

doc/proving.md

@@ -272,8 +272,11 @@ like this:
         showgoals;
         apply socrates_species
 
-When checking the proof, the `showgoals` tactic has the effect of printing the current list
-of proof goals, leaving the goals unchanged.
+When checking the proof, the `showgoals` tactic has the effect of
+printing the current list of proof goals, leaving the goals unchanged.
+A good way to develop a proof is to start with just `showgoals`, and to add tactics
+before this. Running the Ivy proof checker in an Emacs compilation buffer
+is a convenient way to do this. 
 
 Theorems
 --------
@@ -487,7 +490,7 @@ Induction
 The `auto` tactic can't generally prove properties by induction. For
 that IVy needs manual help. To prove a property by induction, we define
 an invariant and prove it by instantiating an induction schema. Here is
-an example of such a schema:
+an example of such a schema, that works for the non-negative integers:
 
    axiom ind[t] = {
        relation p(X:t)
@@ -497,68 +500,95 @@ an example of such a schema:
        property p(X)    
    }
 
-Suppose we want to prove that `sum(X)` is always greater than or equal
-to *X*:
+Like the recursion schema `rec[t]`, the induction schema `ind[t]` is
+part of the integer theory, and becomes available when we interpret
+type `t` as `int`.
+
+Suppose we want to prove that `sum(Y)` is always greater than or equal
+to *Y*, that is:
+
+    property sum(Y) >= Y
+
+We can prove this by applying our induction schema:
 
-    property sum(X) >= X
     proof
-       apply ind[t]
+        apply ind[t];
+        assume sum with X = Y;
+        defergoal;
+        assume sum with X = Y + 1;
 
-This produces two sub-goals, a base case and an induction step:
+
+Applying `ind[t]` 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. 
+The `auto` tactic can't prove these goals because the definition of
+`sum` is a schema that must explicitly instantiated (if we try it,
+we'll get counterexamples). Fortunately, it suffices to instantiate
+this schema just for the specific arguments of `sum` in our
+subgoals. For the base case, we need to instantiate the definition for
+`X`, while for the induction step, we need `X+1`. Notice that we
+referred to the definiton of `sum` by the name `sum`.  Alternatively,
+we can name the definition itself and refer to it by this name.
 
-Because the definition of `sum` is problematic in this way.
+After instantiating the definition of `sum`, our two subgoals look like this:
+
+    ind1.ivy: line 21: Proof goals:
+
+    theorem [prop5] {
+        property [def2] sum(Y + 1) = (0 if Y + 1 <= 0 else Y + 1 + sum(Y + 1 - 1))
+        property sum(Y) >= Y -> sum(Y + 1) >= Y + 1
+    }
 
 
-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.
+    theorem [prop4] {
+        property [def2] sum(Y) = (0 if Y <= 0 else Y + sum(Y - 1))
+        property Y:t <= 0 -> sum(Y) >= Y
+    }
+
+
+Because these goals are quantifier-free the `auto` tactic can easily
+handle them, so our proof is complete.
 
-Generally, when a theory such as the theory of integer arithmetic is
-instantiated, a suitable induction schema such as the above is made
-available.
 
 Naming
 ------
 
-If we can prove that something exists, we can give it a name.
-For example, suppose that we can prove that, for every *X*, there
-exists a *Y* such that `succ(X,Y)`. The there exists a function
-that, given an *X*, produces such a *Y*. We can define such a function
-called `next` in the following way:
+If we can prove that something exists, we can give it a name.  For
+example, suppose that we can prove that, for every *X*, there exists a
+*Y* such that `succ(X,Y)`. The there exists a function that, given an
+*X*, produces such a *Y*. We can define such a function called `next`
+in the following way:
 
     property exists Y. succ(X,Y) named next(X)
 
-Provided we can prove the property, and that `next` is fresh, we can infer
-that, for all *X*, `succ(X,next(X))` holds. Defining a function in this way,
-(that is, as a "Skolem function") can be quite useful in constructibg a proof.
-It doesn't, however, give us any way to *compute* the function `next`.
-
-
+Provided we can prove the property, and that `next` is fresh, we can
+infer that, for all *X*, `succ(X,next(X))` holds. Defining a function
+in this way, (that is, as a Skolem function) can be quite useful in
+constructibg a proof.  However, since proofs in Ivy are not generally
+constructive, we have no way to *compute* the function `next`, so we
+can't use it in extracted code.
 
 Hierarchical proof development
 ==============================
 
-A proof structured as a sequence of judgments isn't very
-organized. Moreover, as the proof context gets larger, it becomes
-increasingly difficult for the automated prover to handle it.
+As the proof context gets larger, it becomes increasingly difficult
+for the automated prover to handle all of the judgements we have
+admitted. This is especially true as combining facts or theories may
+take us outside the automated prover's decidable fragment. For this
+reason, we need some way to break the proof into manageable parts.
+For this purpose, IVy provides a mechanism to structure the proof into
+a collection of localized proofs called *isolates*.
 
 Isolates
 --------
 
-IVy provides a mechanism to structure the proof into a collection of
-localized proofs called "isolates". An isolate is a restricted proof
-context. An isolate can make parts of its proof context available to
-other isolates and keep other parts hidden. Moreover, isolates can
-contain isolates, allowing us to structure a proof development
-hierarchically.
+An isolate is a restricted proof context. An isolate can make parts of
+its proof context available to other isolates and keep other parts
+hidden. Moreover, isolates can contain isolates, allowing us to
+structure a proof development hierarchically.
 
 Suppose, for example, that we want to define a function *f*, but keep
 the exact definition hidden, exposing only certain properties of the
@@ -577,14 +607,18 @@ function. We could write something like this:
 
     }
 
+Any names declared within the isolate belong to its namespace. For
+example, the names of the two properties above are
+`t_theory.expanding` and `t_theory.transitivity`.
+
 The isolate contains four statements. The first, says the type `t` is
 to be interpreted as the integers. This instantiates the theory of the
 integers for type `t`, giving the usual meaning to operators like `+`
 and `<`. The second defines *f* to be the integer successor function.
 
 The remaining two statements are properties about *t* and *f* to
-prove. These properties are proved using only the context of the
-isolate, without any facts declared outside.
+be proved. These properties are proved using only the context of the
+isolate, without any judgments admitted outside.
 
 Now suppose we want to prove an extra property using `t_theory`:
 
@@ -603,16 +637,17 @@ and the definiton of *f* as the successor function are ignored.
 Exporting properties
 --------------------
 
-As an alternative, we cal tell IVY which facts in `t_theory` are to be
-made available to other isolates and which are to be hidden. We place
-the hidden parts in a component object called `impl`:
+As a more convenient alternative, we can tell IVy which facts in
+`t_theory` are to be made available to other isolates and which are to
+be hidden. We place the hidden parts in a section called
+`implementation`:
 
     type t
     function f(X:t) : t
 
     isolate t_theory = {
 
-        object impl = {
+        implementation {
             interpret t -> int
 	    definition f(X) = X + 1
         }
@@ -622,7 +657,7 @@ the hidden parts in a component object called `impl`:
 
     }
 
-Now, we can bring in the visible parts of `t_theory` like this:
+Now, we can use just the visible parts of `t_theory` like this:
 
     isolate extra = {
  
@@ -631,6 +666,15 @@ Now, we can bring in the visible parts of `t_theory` like this:
     }
     with t_theory
 
+Hiding a theory inside an isolate in this way is a very useful
+technique for keeping verification conditions decidable. Although
+definitions in the implementation section of an isolate are hidden
+from the `auto` tactic while proving other isolates, they can still be
+used when extracting executable code. Also, other isolates can still
+use the implementation declarations by explicitly referring to them.
+In particular, attaching the clause `with t` to any isolate will cause
+the `auto` tactic to use the integer theory for `t` in that isolate.
+
 Hierarchies of isolates
 -----------------------
 
@@ -645,7 +689,7 @@ structured like this:
  
 	isolate t_theory = {
 
-	    object impl = {
+	    implementation {
 		interpret t -> int
 		definition f(X) = X + 1
 	    }
@@ -668,27 +712,16 @@ Thus far, proof developments have been presented in order. That is,
 judgements occur in the file in the order in which they are admitted
 to the proof context.
 
-In practice, this strict ordering can be inconvenient, or at least not
-very pedagogically sound. For example suppose we are developing a
-representation of sets based on arrays. We would like to specify first
-the visible parts of the interface (for example the algebraic
-properties of sets) and then later give the actual definitions of the
-set operations in terms of array operations.
+In practice, this strict ordering can be inconvenient. For example,
+from the point of view of clear presentation, it may often be better
+to state a theorem, and *then* develop a sequence of auxiliary
+definitions and lemmas needed to prove it.  Moreover, when developing
+an isolate, we would like to first state the visible judgments, then
+give the hidden implementation.
 
-To allow this sort of development, IVY constructs the proof order
-based on dependencies rather than the textual order within the file.
-The rules for dependencies are:
-
-- A property or definition referencing symbol *s* depends on the definition of *s*,
-- The properties in an isolate depend on any properties and definitions referenced in its `with` clause,
-- A property depends on any textually preceeding properties within the same isolate, and
-- A judgment depends on any property explicitly named in its proof.
-
-For these purposes, a property whose proof requires *s* to be fresh
-counts as a definition of *s*. For example, `property ... named s`
-counts as a definition of *s*.
-
-A proof that can't be ordered because of a dependency cycle is invalid.
+To achieve this, we can use a *specification* section. The
+declarations in this section are admitted logically *after* the other
+declarations in the section.
 
 As an example, we can rewrite the above proof development so that the
 visible properties of the isolates occur textually at the beginning:
@@ -699,48 +732,24 @@ visible properties of the isolates occur textually at the beginning:
 
     isolate extra = {
  
-        property [prop] f(f(X)) > X
+        specification {
+            property [prop] f(f(X)) > X
+        }
 
 	isolate t_theory = {
 
-	    property [expanding] f(X) > X
-	    property [transitivity] X:t < Y & Y < Z -> X < Z	
+            specification {
+	        property [expanding] f(X) > X
+	        property [transitivity] X:t < Y & Y < Z -> X < Z
+            }
 
-	    object impl = {
+	    implementation {
 		interpret t -> int
 		definition f(X) = X + 1
 	    }
-
 	}
     }
 
-IVy still requires that the first use of a symbol be its `type` or
-`function` declaration.
-
-Note that according to the above rules, a definition cannot depend on
-property unless the property is explicitly named in its proof. Suppose,
-for example, we have this definitional schema:
-
-    schema genrec[t] = {
-        type q
-	function pred(X:t) : q
-        function step(X:q,Y:t) : q
-        function fun(X:t) : q
-        property [descending] pred(X) < X
-	#--------------------------------
-        definition fun(X:t) = 0 if X <= 0 else step(fun(pred(X),X))
-    }
-
-This allows us to recur on any value less than *X* rather than just *X*-1.
-However, to admit this, we must prove the the function `pred` is descending.	
-We can use this schema as follows:
-
-    property [myprop] X-2 < X
-
-    definition mysum(X:t) = 0 if X <= 0 else (X + sum(X-2))
-    proof
-       apply genrec[t] with descending = myprop
-
 
 
 

ivy/ivy_compiler.py

@@ -656,7 +656,6 @@ def compile_defn(df):
                     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):
@@ -874,7 +873,6 @@ 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))

ivy/ivy_parser.py

@@ -313,13 +313,32 @@ def addlabel(lf,pref):
     res.lineno = lf.lineno
     return res
 
-def p_top_axiom_labeledfmla(p):
-    'top : top opttemporal AXIOM labeledfmla'
-    p[0] = check_non_temporal(p[1])
-    lf = addlabel(p[4],'axiom')
-    d = AxiomDecl(addtemporal(lf) if p[2] else check_non_temporal(lf))
-    d.lineno = get_lineno(p,3)
-    p[0].declare(d)
+if iu.get_numeric_version() <= [1,6]:
+    def p_top_axiom_labeledfmla(p):
+        'top : top opttemporal AXIOM labeledfmla'
+        p[0] = check_non_temporal(p[1])
+        lf = addlabel(p[4],'axiom')
+        d = AxiomDecl(addtemporal(lf) if p[2] else check_non_temporal(lf))
+        d.lineno = get_lineno(p,3)
+        p[0].declare(d)
+else:
+    def p_gprop_fmla(p):
+        'gprop : fmla'
+        p[0] = p[1]
+
+    def p_gprop_schdefnrhs(p):
+        'gprop : schdefnrhs'
+        p[0] = p[1]
+
+    def p_top_axiom_optlabel_gprop(p):
+        'top : top opttemporal AXIOM optlabel gprop'
+        p[0] = check_non_temporal(p[1])
+        lf = LabeledFormula(p[4],p[5])
+        lf.lineno = get_lineno(p,3)
+        lf = addlabel(p[4],'axiom')
+        d = AxiomDecl(addtemporal(lf) if p[2] else check_non_temporal(lf))
+        d.lineno = get_lineno(p,3)
+        p[0].declare(d)
 
 def p_optskolem(p):
     'optskolem : '
@@ -873,7 +892,6 @@ else:
         '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:

ivy/ivy_proof.py

@@ -163,7 +163,7 @@ class ProofChecker(object):
         schema, prob, pmatch = self.setup_matching(decl,proof)
 #        prem = make_goal(proof.lineno,fresh_label(goal_prems(decl)),[],schema)
         prem  = apply_match_goal(pmatch,schema,apply_match_alt)
-        return [goal_add_prem(decls[0],prem)] + decls[1:]
+        return [goal_add_prem(decls[0],prem,proof.lineno)] + decls[1:]
 
     def match_schema(self,decl,proof):
         """ attempt to match a definition or property decl to a schema
@@ -185,18 +185,7 @@ class ProofChecker(object):
             schema = apply_match_goal(pmatch,schema,apply_match_alt)
             schema = apply_match_goal(fomatch,schema,apply_match)
             schema = apply_match_goal(somatch,schema,apply_match_alt)
-            return goal_subgoals(schema,decl)
-            
-            # subgoals = []
-            # for x in goal_prems(schema):
-            #     if isinstance(x,ia.LabeledFormula) :
-            #         g = apply_match_goal(pmatch,x,apply_match_alt)
-            #         iu.dbg('pmatch')
-            #         iu.dbg('g')
-            #         g = apply_match_goal(fomatch,g,apply_match)
-            #         g = apply_match_goal(somatch,g,apply_match_alt)
-            #         subgoals.append(g)
-            # return [s for s in subgoals if not trivial_goal(s)]
+            return goal_subgoals(schema,decl,proof.lineno)
         return None
 
 
@@ -225,14 +214,14 @@ def clone_goal(goal,prems,conc):
 
 # Substitute a goal g2 for the conclusion of goal g1. The result has the label of g2.
 
-def goal_subst(g1,g2):
+def goal_subst(g1,g2,lineno):
     check_name_clash(g1,g2)
-    return make_goal(g2.lineno, g2.label, goal_prems(g1) + goal_prems(g2), goal_conc(g2))
+    return make_goal(lineno, g2.label, goal_prems(g1) + goal_prems(g2), goal_conc(g2))
 
 # Substitute a sequence of subgoals in to the conclusion of the first goal
 
-def goals_subst(goals,subgoals):
-    return [goal_subst(goals[0],g) for g in subgoals] + goals[1:]
+def goals_subst(goals,subgoals,lineno):
+    return [goal_subst(goals[0],g,lineno) for g in subgoals] + goals[1:]
 
 # Add a formula or schema as a premise to a goal. Make up a fresh name for it.
 
@@ -244,8 +233,8 @@ def fresh_label(goals):
     
 # Add a premise to a goal
 
-def goal_add_prem(goal,prem):
-    return make_goal(goal.lineno,goal.label,goal_prems(goal) + [prem], goal_conc(goal))
+def goal_add_prem(goal,prem,lineno):
+    return make_goal(lineno,goal.label,goal_prems(goal) + [prem], goal_conc(goal))
     
 # Get the symbols and types defined in the premises of a goal
 
@@ -310,10 +299,10 @@ def check_premises_provided(g1,g2):
 # Turn the propositional premises of a goal into a list of subgoals. The
 # symbols and types in the goal must be provided by the environment.
 
-def goal_subgoals(schema,goal):
+def goal_subgoals(schema,goal,lineno):
     check_concs_match(schema,goal)
     check_premises_provided(schema,goal)
-    subgoals = [goal_subst(goal,x) for x in goal_prems(schema) if isinstance(x,ia.LabeledFormula)]
+    subgoals = [goal_subst(goal,x,lineno) for x in goal_prem_goals(schema)]
     return [s for s in subgoals if not trivial_goal(s)]
 
 # Get the free vocabulary of a goal, including sorts, symbols and variables
@@ -586,19 +575,12 @@ def rename_problem(match,prob):
 def avoid_capture_problem(prob,schema,match):
     """ Rename a match problem to avoid capture when applying a
     match"""
-    show_match(match)
-    iu.dbg('schema')
     matchvars = list(x for x in match_rhs_vars(match) if x not in match)
-    iu.dbg('matchvars')
     freevocab = goal_free(schema)
     rn = iu.UniqueRenamer(used=[v.name for v in freevocab if il.is_variable(v)])
     cmatch = dict((v,v.rename(rn(v.name))) for v in matchvars if v in freevocab)
-    show_match(cmatch)
-    iu.dbg('prob')
     rename_problem(cmatch,prob)
-    iu.dbg('prob')
     schema = apply_match_goal(cmatch,schema,apply_match)
-    iu.dbg('schema')
     return prob,schema
 
 def trivial_goal(goal):
@@ -661,8 +643,6 @@ def apply_match_alt(match,fmla,env = None):
 
     """
     freevars = list(match_rhs_vars(match))
-    iu.dbg('freevars')
-    iu.dbg('fmla')
     fmla = il.alpha_avoid(fmla,freevars)
     return apply_match_alt_rec(match,fmla,env if env is not None else set())
 

ivy/ivy_solver.py

@@ -42,6 +42,7 @@ def set_macro_finder(truth):
     z3.set_param('smt.macro_finder',truth)
     
 opt_incremental = iu.BooleanParameter("incremental",True)
+opt_show_vcs = iu.BooleanParameter("show_vcs",False)
 
 #z3.set_param('smt.mbqi.trace',True)
 opt_macro_finder = iu.BooleanParameter("macro_finder",True)
@@ -1002,14 +1003,16 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con
 
     """
 
-    print "definitions:"
-    for df in clauses.defs:
-        print df
-        print
-    print "fmlas:"
-    for fmla in clauses.fmlas:
-        print ivy_logic.close_formula(fmla)
-        print
+    if opt_show_vcs.get():
+        print ''
+        print "definitions:"
+        for df in clauses.defs:
+            print df
+            print
+        print "axioms:"
+        for fmla in clauses.fmlas:
+            print ivy_logic.close_formula(fmla)
+            print
 
     s = z3.Solver()
     s.add(clauses_to_z3(clauses))
@@ -1030,14 +1033,16 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con
                         s.add(clauses_to_z3(fmla))
                 fc.start()
                 if fc.assume():
-                    print 'assume: {}'.format(fc.cond())
+                    if opt_show_vcs.get():
+                        print 'assume: {}'.format(fc.cond())
                     s.add(clauses_to_z3(fc.cond()))
                     assumes.append(fc.cond())
                 else:
                     if opt_incremental.get():
                         s.push()
                     foo = fc.cond()
-                    print 'goal: {}'.format(foo)
+                    if opt_show_vcs.get():
+                        print 'assert: {}'.format(foo)
                     s.add(clauses_to_z3(foo))
                     res = decide(s)
                     if res != z3.unsat:

ivy/ivy_theory.py

@@ -151,7 +151,8 @@ def map_fmla(fmla,strat_map):
     if il.is_variable(fmla):
         if fmla not in strat_map:
             res = UFNode()
-            res.variables.add(fmla)
+            if fmla in universally_quantified_variables:
+                res.variables.add(fmla)
             strat_map[fmla] = res
         return strat_map[fmla]
     nodes = [map_fmla(f,strat_map) for f in fmla.args]
@@ -183,6 +184,7 @@ def create_strat_map(assumes,asserts,macros):
     symbols_over_universals = il.symbols_over_universals(all_fmlas)
     universally_quantified_variables = il.universal_variables(all_fmlas)
 
+#    print 'symbols_over_universals : {}'.format([str(v) for v in symbols_over_universals])
 #    print 'universally_quantified_variables : {}'.format([str(v) for v in universally_quantified_variables])
     
     strat_map = defaultdict(UFNode)
@@ -289,8 +291,10 @@ def get_assumes_and_asserts(preconds_only):
     for ldf in im.module.definitions:
         if not isinstance(ldf.formula,il.DefinitionSchema):
             if ldf.formula.defines() not in ilu.symbols_ast(ldf.formula.rhs()):
+#                print 'macro : {}'.format(ldf.formula)
                 macros.append((ldf.formula.to_constraint(),ldf))
             else: # can't treat recursive definition as macro
+#                print 'axiom : {}'.format(ldf.formula)
                 assumes.append((ldf.formula.to_constraint(),ldf))
 
     for ldf in im.module.labeled_axioms:
@@ -300,7 +304,7 @@ def get_assumes_and_asserts(preconds_only):
 
     for ldf in im.module.labeled_props:
         if not ldf.temporal:
-#            print 'prop : {}'.format(ldf.formula)
+#            print 'prop : {}{} {}'.format(ldf.lineno,ldf.label,ldf.formula)
             asserts.append((ldf.formula,ldf))
 
     for ldf in im.module.labeled_conjs:

test/ind1.ivy

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