Change the induction heuristic for lemmas to also look in precondition for clues about which parameters to include.

As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.

5 files changed, 57 insertions, 92 deletions

diff --git a/Test/dafny4/ACL2-extractor.dfy b/Test/dafny4/ACL2-extractor.dfy
index 8fe98531..bd2c9d83 100644
--- a/Test/dafny4/ACL2-extractor.dfy
+++ b/Test/dafny4/ACL2-extractor.dfy
@@ -116,9 +116,9 @@ lemma RevLength(xs: List)
 // you can prove two lists equal by proving their elements equal

 

 lemma EqualElementsMakeEqualLists(xs: List, ys: List)

-  requires length(xs) == length(ys);

-  requires forall i :: 0 <= i < length(xs) ==> nth(i, xs) == nth(i, ys);

-  ensures xs == ys;

+  requires length(xs) == length(ys)

+  requires forall i :: 0 <= i < length(xs) ==> nth(i, xs) == nth(i, ys)

+  ensures xs == ys

 {

   match xs {

     case Nil =>

@@ -132,7 +132,7 @@ lemma EqualElementsMakeEqualLists(xs: List, ys: List)
           nth(i+1, xs) == nth(i+1, ys);

         }

       }

-      EqualElementsMakeEqualLists(xs.tail, ys.tail);

+      // EqualElementsMakeEqualLists(xs.tail, ys.tail);

   }

 }

 

diff --git a/Test/dafny4/KozenSilva.dfy b/Test/dafny4/KozenSilva.dfy
index af0cdc71..ef49b10f 100644
--- a/Test/dafny4/KozenSilva.dfy
+++ b/Test/dafny4/KozenSilva.dfy
@@ -25,8 +25,8 @@ copredicate LexLess(s: Stream<int>, t: Stream<int>)
 

 // A co-lemma is used to establish the truth of a co-predicate.

 colemma Theorem1_LexLess_Is_Transitive(s: Stream<int>, t: Stream<int>, u: Stream<int>)

-  requires LexLess(s, t) && LexLess(t, u);

-  ensures LexLess(s, u);

+  requires LexLess(s, t) && LexLess(t, u)

+  ensures LexLess(s, u)

 {

   // Here is the proof, which is actually a body of code.  It lends itself to a

   // simple, intuitive co-inductive reading.  For a theorem this simple, this simple

@@ -38,6 +38,14 @@ colemma Theorem1_LexLess_Is_Transitive(s: Stream<int>, t: Stream<int>, u: Stream
   }

 }

 

+// Actually, Dafny can do the proof of the previous lemma completely automatically.  Here it is:

+colemma Theorem1_LexLess_Is_Transitive_Automatic(s: Stream<int>, t: Stream<int>, u: Stream<int>)

+  requires LexLess(s, t) && LexLess(t, u)

+  ensures LexLess(s, u)

+{

+  // no manual proof needed, so the body of the co-lemma is empty

+}

+

 // The following predicate captures the (inductively defined) negation of (the

 // co-inductively defined) LexLess above.

 predicate NotLexLess(s: Stream<int>, t: Stream<int>)

@@ -51,7 +59,7 @@ predicate NotLexLess'(k: nat, s: Stream<int>, t: Stream<int>)
 }

 

 lemma EquivalenceTheorem(s: Stream<int>, t: Stream<int>)

-  ensures LexLess(s, t) <==> !NotLexLess(s, t);

+  ensures LexLess(s, t) <==> !NotLexLess(s, t)

 {

   if !NotLexLess(s, t) {

     EquivalenceTheorem0(s, t);

@@ -61,8 +69,8 @@ lemma EquivalenceTheorem(s: Stream<int>, t: Stream<int>)
   }

 }

 colemma EquivalenceTheorem0(s: Stream<int>, t: Stream<int>)

-  requires !NotLexLess(s, t);

-  ensures LexLess(s, t);

+  requires !NotLexLess(s, t)

+  ensures LexLess(s, t)

 {

   // Here, more needs to be said about the way Dafny handles co-lemmas.

   // The way a co-lemma establishes a co-predicate is to prove, by induction,

@@ -74,14 +82,14 @@ colemma EquivalenceTheorem0(s: Stream<int>, t: Stream<int>)
 // indicates a finite unrolling of a co-inductive predicate.  In particular,

 // LexLess#[k] refers to k unrollings of LexLess.

 lemma EquivalenceTheorem0_Lemma(k: nat, s: Stream<int>, t: Stream<int>)

-  requires !NotLexLess'(k, s, t);

-  ensures LexLess#[k](s, t);

+  requires !NotLexLess'(k, s, t)

+  ensures LexLess#[k](s, t)

 {

   // This simple inductive proof is done completely automatically by Dafny.

 }

 lemma EquivalenceTheorem1(s: Stream<int>, t: Stream<int>)

-  requires LexLess(s, t);

-  ensures !NotLexLess(s, t);

+  requires LexLess(s, t)

+  ensures !NotLexLess(s, t)

 {

   // The forall statement in Dafny is used, here, as universal introduction:

   // what EquivalenceTheorem1_Lemma establishes for one k, the forall

@@ -91,22 +99,22 @@ lemma EquivalenceTheorem1(s: Stream<int>, t: Stream<int>)
   }

 }

 lemma EquivalenceTheorem1_Lemma(k: nat, s: Stream<int>, t: Stream<int>)

-  requires LexLess(s, t);

-  ensures !NotLexLess'(k, s, t);

+  requires LexLess(s, t)

+  ensures !NotLexLess'(k, s, t)

 {

 }

 

 lemma Theorem1_Alt(s: Stream<int>, t: Stream<int>, u: Stream<int>)

-  requires NotLexLess(s, u);

-  ensures NotLexLess(s, t) || NotLexLess(t, u);

+  requires NotLexLess(s, u)

+  ensures NotLexLess(s, t) || NotLexLess(t, u)

 {

   forall k: nat | NotLexLess'(k, s, u) {

     Theorem1_Alt_Lemma(k, s, t, u);

   }

 }

 lemma Theorem1_Alt_Lemma(k: nat, s: Stream<int>, t: Stream<int>, u: Stream<int>)

-  requires NotLexLess'(k, s, u);

-  ensures NotLexLess'(k, s, t) || NotLexLess'(k, t, u);

+  requires NotLexLess'(k, s, u)

+  ensures NotLexLess'(k, s, t) || NotLexLess'(k, t, u)

 {

 }

 

@@ -116,8 +124,8 @@ function PointwiseAdd(s: Stream<int>, t: Stream<int>): Stream<int>
 }

 

 colemma Theorem2_Pointwise_Addition_Is_Monotone(s: Stream<int>, t: Stream<int>, u: Stream<int>, v: Stream<int>)

-  requires LexLess(s, t) && LexLess(u, v);

-  ensures LexLess(PointwiseAdd(s, u), PointwiseAdd(t, v));

+  requires LexLess(s, t) && LexLess(u, v)

+  ensures LexLess(PointwiseAdd(s, u), PointwiseAdd(t, v))

 {

   // The co-lemma will establish the co-inductive predicate by establishing

   // all finite unrollings thereof.  Each finite unrolling is proved by

@@ -148,15 +156,9 @@ copredicate Subtype(a: RecType, b: RecType)
 }

 

 colemma Theorem3_Subtype_Is_Transitive(a: RecType, b: RecType, c: RecType)

-  requires Subtype(a, b) && Subtype(b, c);

-  ensures Subtype(a, c);

-{

-  if a == Bottom || c == Top {

-    // done

-  } else {

-    Theorem3_Subtype_Is_Transitive(c.dom, b.dom, a.dom);

-    Theorem3_Subtype_Is_Transitive(a.ran, b.ran, c.ran);

-  }

+  requires Subtype(a, b) && Subtype(b, c)

+  ensures Subtype(a, c)

+{

 }

 

 // --------------------------------------------------------------------------

@@ -184,16 +186,16 @@ copredicate ValBelow(u: Val, v: Val)
 }

 

 colemma Theorem4a_ClEnvBelow_Is_Transitive(c: ClEnv, d: ClEnv, e: ClEnv)

-  requires ClEnvBelow(c, d) && ClEnvBelow(d, e);

-  ensures ClEnvBelow(c, e);

+  requires ClEnvBelow(c, d) && ClEnvBelow(d, e)

+  ensures ClEnvBelow(c, e)

 {

   forall y | y in c.m {

     Theorem4b_ValBelow_Is_Transitive#[_k-1](c.m[y], d.m[y], e.m[y]);

   }

 }

 colemma Theorem4b_ValBelow_Is_Transitive(u: Val, v: Val, w: Val)

-  requires ValBelow(u, v) && ValBelow(v, w);

-  ensures ValBelow(u, w);

+  requires ValBelow(u, v) && ValBelow(v, w)

+  ensures ValBelow(u, w)

 {

   if u.ValCl? {

     Theorem4a_ClEnvBelow_Is_Transitive(u.cl.env, v.cl.env, w.cl.env);

@@ -209,7 +211,7 @@ predicate IsCapsule(cap: Capsule)
 }

 

 function ClosureConversion(cap: Capsule): Cl

-  requires IsCapsule(cap);

+  requires IsCapsule(cap)

 {

   Closure(cap.e.abs, ClosureConvertedMap(cap.s))

   // In the Kozen and Silva paper, there are more conditions, having to do with free variables,

@@ -229,8 +231,8 @@ predicate CapsuleEnvironmentBelow(s: map<Var, ConstOrAbs>, t: map<Var, ConstOrAb
 }

 

 colemma Theorem5_ClosureConversion_Is_Monotone(s: map<Var, ConstOrAbs>, t: map<Var, ConstOrAbs>)

-  requires CapsuleEnvironmentBelow(s, t);

-  ensures ClEnvBelow(ClosureConvertedMap(s), ClosureConvertedMap(t));

+  requires CapsuleEnvironmentBelow(s, t)

+  ensures ClEnvBelow(ClosureConvertedMap(s), ClosureConvertedMap(t))

 {

 }

 

@@ -251,8 +253,8 @@ copredicate Bisim(s: Stream, t: Stream)
 }

 

 colemma Theorem6_Bisim_Is_Symmetric(s: Stream, t: Stream)

-  requires Bisim(s, t);

-  ensures Bisim(t, s);

+  requires Bisim(s, t)

+  ensures Bisim(t, s)

 {

   // proof is automatic

 }

@@ -270,8 +272,8 @@ function merge(s: Stream, t: Stream): Stream
 // In general, the termination argument needs to be supplied explicitly in terms

 // of a metric, rank, variant function, or whatever you want to call it--a

 // "decreases" clause in Dafny.  Dafny provides some help in making up "decreases"

-// clauses, and in this case it automatically adds "decreases 0;" to SplitLeft

-// and "decreases 1;" to SplitRight.  With these "decreases" clauses, the

+// clauses, and in this case it automatically adds "decreases 0" to SplitLeft

+// and "decreases 1" to SplitRight.  With these "decreases" clauses, the

 // termination check of SplitRight's call to SplitLeft will simply be "0 < 1",

 // which is trivial to check.

 function SplitLeft(s: Stream): Stream

@@ -284,7 +286,7 @@ function SplitRight(s: Stream): Stream
 }

 

 colemma Theorem7_Merge_Is_Left_Inverse_Of_Split_Bisim(s: Stream)

-  ensures Bisim(merge(SplitLeft(s), SplitRight(s)), s);

+  ensures Bisim(merge(SplitLeft(s), SplitRight(s)), s)

 {

   var LHS := merge(SplitLeft(s), SplitRight(s));

   // The construct that follows is a "calc" statement.  It gives a way to write an

@@ -318,7 +320,7 @@ colemma Theorem7_Merge_Is_Left_Inverse_Of_Split_Bisim(s: Stream)
 }

 

 colemma Theorem7_Merge_Is_Left_Inverse_Of_Split_Equal(s: Stream)

-  ensures merge(SplitLeft(s), SplitRight(s)) == s;

+  ensures merge(SplitLeft(s), SplitRight(s)) == s

 {

   // The proof of this co-lemma is actually done completely automatically (so the

   // body of this co-lemma can be empty).  However, just to show what the calculations

diff --git a/Test/dafny4/KozenSilva.dfy.expect b/Test/dafny4/KozenSilva.dfy.expect
index c6c90498..90432af3 100644
--- a/Test/dafny4/KozenSilva.dfy.expect
+++ b/Test/dafny4/KozenSilva.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 47 verified, 0 errors

+Dafny program verifier finished with 49 verified, 0 errors

diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy
index 7db31cbd..e694fc4b 100644
--- a/Test/dafny4/NipkowKlein-chapter7.dfy
+++ b/Test/dafny4/NipkowKlein-chapter7.dfy
@@ -112,13 +112,6 @@ inductive lemma lemma_7_6(b: bexp, c: com, c': com, s: state, t: state)
   requires big_step(While(b, c), s, t) && equiv_c(c, c')

   ensures big_step(While(b, c'), s, t)

 {

-  if !bval(b, s) {

-    // trivial

-  } else {

-    var s' :| big_step#[_k-1](c, s, s') && big_step#[_k-1](While(b, c), s', t);

-    lemma_7_6(b, c, c', s', t);  // induction hypothesis

-    assert big_step(While(b, c'), s', t);

-  }

 }

 

 // equiv_c is an equivalence relation

@@ -139,27 +132,7 @@ inductive lemma IMP_is_deterministic(c: com, s: state, t: state, t': state)
   requires big_step(c, s, t) && big_step(c, s, t')

   ensures t == t'

 {

-  match c

-  case SKIP =>

-    // trivial

-  case Assign(x, a) =>

-    // trivial

-  case Seq(c0, c1) =>

-    var s' :| big_step#[_k-1](c0, s, s') && big_step#[_k-1](c1, s', t);

-    var s'' :| big_step#[_k-1](c0, s, s'') && big_step#[_k-1](c1, s'', t');

-    IMP_is_deterministic(c0, s, s', s'');

-    IMP_is_deterministic(c1, s', t, t');

-  case If(b, thn, els) =>

-    IMP_is_deterministic(if bval(b, s) then thn else els, s, t, t');

-  case While(b, body) =>

-    if !bval(b, s) {

-      // trivial

-    } else {

-      var s' :| big_step#[_k-1](body, s, s') && big_step#[_k-1](While(b, body), s', t);

-      var s'' :| big_step#[_k-1](body, s, s'') && big_step#[_k-1](While(b, body), s'', t');

-      IMP_is_deterministic(body, s, s', s'');

-      IMP_is_deterministic(While(b, body), s', t, t');

-    }

+  // Dafny totally rocks!

 }

 

 // ----- Small-step semantics -----

@@ -214,12 +187,6 @@ inductive lemma star_transitive_aux(c0: com, s0: state, c1: com, s1: state, c2:
   requires small_step_star(c0, s0, c1, s1)

   ensures small_step_star(c1, s1, c2, s2) ==> small_step_star(c0, s0, c2, s2)

 {

-  if c0 == c1 && s0 == s1 {

-  } else {

-    var c', s' :|

-      small_step(c0, s0, c', s') && small_step_star#[_k-1](c', s', c1, s1);

-      star_transitive_aux(c', s', c1, s1, c2, s2);

-  }

 }

 

 // The big-step semantics can be simulated by some number of small steps

@@ -240,15 +207,14 @@ inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state)
       small_step_star(Seq(c0, c1), s, Seq(SKIP, c1), s') && small_step_star(Seq(SKIP, c1), s', SKIP, t);

       { lemma_7_13(c0, s, SKIP, s', c1); }

       small_step_star(c0, s, SKIP, s') && small_step_star(Seq(SKIP, c1), s', SKIP, t);

-      { BigStep_implies_SmallStepStar(c0, s, s'); }

+      //{ BigStep_implies_SmallStepStar(c0, s, s'); }

       small_step_star(Seq(SKIP, c1), s', SKIP, t);

       { assert small_step(Seq(SKIP, c1), s', c1, s'); }

       small_step_star(c1, s', SKIP, t);

-      { BigStep_implies_SmallStepStar(c1, s', t); }

+      //{ BigStep_implies_SmallStepStar(c1, s', t); }

       true;

     }

   case If(b, thn, els) =>

-    BigStep_implies_SmallStepStar(if bval(b, s) then thn else els, s, t);

   case While(b, body) =>

     if !bval(b, s) && s == t {

       calc <== {

@@ -271,11 +237,11 @@ inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state)
         small_step_star(Seq(body, While(b, body)), s, Seq(SKIP, While(b, body)), s') && small_step_star(Seq(SKIP, While(b, body)), s', SKIP, t);

         { lemma_7_13(body, s, SKIP, s', While(b, body)); }

         small_step_star(body, s, SKIP, s') && small_step_star(Seq(SKIP, While(b, body)), s', SKIP, t);

-        { BigStep_implies_SmallStepStar(body, s, s'); }

+        //{ BigStep_implies_SmallStepStar(body, s, s'); }

         small_step_star(Seq(SKIP, While(b, body)), s', SKIP, t);

         { assert small_step(Seq(SKIP, While(b, body)), s', While(b, body), s'); }

         small_step_star(While(b, body), s', SKIP, t);

-        { BigStep_implies_SmallStepStar(While(b, body), s', t); }

+        //{ BigStep_implies_SmallStepStar(While(b, body), s', t); }

         true;

       }

     }

@@ -299,7 +265,6 @@ inductive lemma SmallStepStar_implies_BigStep(c: com, s: state, t: state)
   if c == SKIP && s == t {

   } else {

     var c', s' :| small_step(c, s, c', s') && small_step_star#[_k-1](c', s', SKIP, t);

-    SmallStepStar_implies_BigStep(c', s', t);

     SmallStep_plus_BigStep(c, s, c', s', t);

   }

 }

@@ -316,7 +281,6 @@ inductive lemma SmallStep_plus_BigStep(c: com, s: state, c': com, s': state, t:
       var c0' :| c' == Seq(c0', c1) && small_step(c0, s, c0', s');

       if big_step(c', s', t) {

         var s'' :| big_step(c0', s', s'') && big_step(c1, s'', t);

-        SmallStep_plus_BigStep(c0, s, c0', s', s'');

       }

     }

   case If(b, thn, els) =>

diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index 3dba6325..0d6cffa1 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -234,17 +234,16 @@ lemma UniqueRepresentation(a: seq<int>, b: seq<int>, lowDigit: int, base: nat)
 }

 

 lemma ZeroIsUnique(a: seq<int>, lowDigit: int, base: nat)

-  requires 2 <= base && lowDigit <= 0 < lowDigit + base;

-  requires a == trim(a);

-  requires IsSkewNumber(a, lowDigit, base);

-  requires eval(a, base) == 0;

-  ensures a == [];

+  requires 2 <= base && lowDigit <= 0 < lowDigit + base

+  requires a == trim(a)

+  requires IsSkewNumber(a, lowDigit, base)

+  requires eval(a, base) == 0

+  ensures a == []

 {

   if a != [] {

-    assert eval(a, base) == a[0] + base * eval(a[1..], base);

     if eval(a[1..], base) == 0 {

       TrimProperty(a);

-      ZeroIsUnique(a[1..], lowDigit, base);

+      // ZeroIsUnique(a[1..], lowDigit, base);

     }

     assert false;

   }