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.

3 files changed, 48 insertions, 68 deletions

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 24c8e94e..6e67de26 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -35,7 +35,7 @@ lemma Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma could ha
 {

   if k != 0 {

     Lemma_InTail(s.head, u);

-    Lemma_TailSubStreamK(s.tail, u, k-1);

+    //Lemma_TailSubStreamK(s.tail, u, k-1);

   }

 }

 lemma Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)

@@ -193,10 +193,10 @@ lemma FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)
 }

 

 lemma FS_Pong<T>(s: Stream<T>, h: PredicateHandle, x: T, k: nat)

-  requires AlwaysAnother(s, h) && In(x, s) && P(x, h);

-  requires Tail(s, k).head == x;

-  ensures In(x, Filter(s, h));

-  decreases k;

+  requires AlwaysAnother(s, h) && In(x, s) && P(x, h)

+  requires Tail(s, k).head == x

+  ensures In(x, Filter(s, h))

+  decreases k

 {

   var fs := Filter(s, h);

   if s.head == x {

@@ -205,14 +205,14 @@ lemma FS_Pong<T>(s: Stream<T>, h: PredicateHandle, x: T, k: nat)
     assert fs == Cons(s.head, Filter(s.tail, h));  // reminder of where we are

     calc {

       true;

-    ==  { FS_Pong(s.tail, h, x, k-1); }

+    //==  { FS_Pong(s.tail, h, x, k-1); }

       In(x, Filter(s.tail, h));

     ==> { assert fs.head != x;  Lemma_InTail(x, fs); }

       In(x, fs);

     }

   } else {

-    assert fs == Filter(s.tail, h);  // reminder of where we are

-    FS_Pong(s.tail, h, x, k-1);

+    //assert fs == Filter(s.tail, h);  // reminder of where we are

+    //FS_Pong(s.tail, h, x, k-1);

   }

 }

 

diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 7ea038be..6bd06965 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -7,25 +7,25 @@ abstract module TotalOrder {
   // Three properties of total orders.  Here, they are given as unproved

   // lemmas, that is, as axioms.

   lemma Antisymmetry(a: T, b: T)

-    requires Leq(a, b) && Leq(b, a);

-    ensures a == b;

+    requires Leq(a, b) && Leq(b, a)

+    ensures a == b

   lemma Transitivity(a: T, b: T, c: T)

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

-    ensures Leq(a, c);

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

+    ensures Leq(a, c)

   lemma Totality(a: T, b: T)

-    ensures Leq(a, b) || Leq(b, a);

+    ensures Leq(a, b) || Leq(b, a)

 }

 

 abstract module Sort {

   import O as TotalOrder  // let O denote some module that has the members of TotalOrder

 

   predicate Sorted(a: array<O.T>, low: int, high: int)

-    requires a != null && 0 <= low <= high <= a.Length;

-    reads a;

+    requires a != null && 0 <= low <= high <= a.Length

+    reads a

     // The body of the predicate is hidden outside the module, but the postcondition is

     // "exported" (that is, visible, known) outside the module.  Here, we choose the

     // export the following property:

-    ensures Sorted(a, low, high) ==> forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j]);

+    ensures Sorted(a, low, high) ==> forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j])

   {

     forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j])

   }

@@ -33,18 +33,18 @@ abstract module Sort {
   // In the insertion sort routine below, it's more convenient to keep track of only that

   // neighboring elements of the array are sorted...

   predicate NeighborSorted(a: array<O.T>, low: int, high: int)

-    requires a != null && 0 <= low <= high <= a.Length;

-    reads a;

+    requires a != null && 0 <= low <= high <= a.Length

+    reads a

   {

     forall i :: low < i < high ==> O.Leq(a[i-1], a[i])

   }

   // ...but we show that property to imply all pairs to be sorted.  The proof of this

   // lemma uses the transitivity property.

   lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)

-    requires a != null && 0 <= low <= high <= a.Length;

-    requires NeighborSorted(a, low, high);

-    ensures Sorted(a, low, high);

-    decreases high - low;

+    requires a != null && 0 <= low <= high <= a.Length

+    requires NeighborSorted(a, low, high)

+    ensures Sorted(a, low, high)

+    decreases high - low

   {

     if low != high {

       NeighborSorted_implies_Sorted(a, low+1, high);

@@ -57,25 +57,25 @@ abstract module Sort {
 

   // Standard insertion sort method

   method InsertionSort(a: array<O.T>)

-    requires a != null;

-    modifies a;

-    ensures Sorted(a, 0, a.Length);

-    ensures multiset(a[..]) == old(multiset(a[..]));

+    requires a != null

+    modifies a

+    ensures Sorted(a, 0, a.Length)

+    ensures multiset(a[..]) == old(multiset(a[..]))

   {

     if a.Length == 0 { return; }

     var i := 1;

     while i < a.Length

-      invariant 0 < i <= a.Length;

-      invariant NeighborSorted(a, 0, i);

-      invariant multiset(a[..]) == old(multiset(a[..]));

+      invariant 0 < i <= a.Length

+      invariant NeighborSorted(a, 0, i)

+      invariant multiset(a[..]) == old(multiset(a[..]))

     {

       var j := i;

       while 0 < j && !O.Leq(a[j-1], a[j])

-        invariant 0 <= j <= i;

-        invariant NeighborSorted(a, 0, j);

-        invariant NeighborSorted(a, j, i+1);

-        invariant 0 < j < i ==> O.Leq(a[j-1], a[j+1]);

-        invariant multiset(a[..]) == old(multiset(a[..]));

+        invariant 0 <= j <= i

+        invariant NeighborSorted(a, 0, j)

+        invariant NeighborSorted(a, j, i+1)

+        invariant 0 < j < i ==> O.Leq(a[j-1], a[j+1])

+        invariant multiset(a[..]) == old(multiset(a[..]))

       {

         // The proof of correctness uses the totality property here.

         // It implies that if two elements are not previously in

@@ -97,7 +97,7 @@ module IntOrder refines TotalOrder {
   datatype T = Int(i: int)

   // Define the ordering on these integers

   predicate method Leq ...

-    ensures Leq(a, b) ==> a.i <= b.i;

+    ensures Leq(a, b) ==> a.i <= b.i

   {

     a.i <= b.i

   }

@@ -156,7 +156,7 @@ module intOrder refines TotalOrder {
   type T = int

   // Define the ordering on these integers

   predicate method Leq ...

-    ensures Leq(a, b) ==> a <= b;

+    ensures Leq(a, b) ==> a <= b

   {

     a <= b

   }

diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy
index 516a9e4e..85f73bc3 100644
--- a/Test/dafny3/InfiniteTrees.dfy
+++ b/Test/dafny3/InfiniteTrees.dfy
@@ -286,7 +286,7 @@ lemma Theorem1_Lemma(t: Tree, n: nat, p: Stream<int>)
         LowerThan(ch, n);

       ==>  // def. LowerThan

         LowerThan(ch.head.children, n-1);

-      ==>  { Theorem1_Lemma(ch.head, n-1, tail); }

+      ==>  //{ Theorem1_Lemma(ch.head, n-1, tail); }

         !IsNeverEndingStream(tail);

       ==>  // def. IsNeverEndingStream

         !IsNeverEndingStream(p);

@@ -374,30 +374,30 @@ lemma Proposition3b()
   }

 }

 lemma Proposition3b_Lemma(t: Tree, h: nat, p: Stream<int>)

-  requires LowerThan(t.children, h) && ValidPath(t, p);

-  ensures !IsNeverEndingStream(p);

-  decreases h;

+  requires LowerThan(t.children, h) && ValidPath(t, p)

+  ensures !IsNeverEndingStream(p)

+  decreases h

 {

   match p {

     case Nil =>

     case Cons(index, tail) =>

       // From the definition of ValidPath(t, p), we get the following:

       var ch := Tail(t.children, index);

-      assert ch.Cons? && ValidPath(ch.head, tail);

+      // assert ch.Cons? && ValidPath(ch.head, tail);

       // From the definition of LowerThan(t.children, h), we get the following:

       match t.children {

         case Nil =>

           ValidPath_Lemma(p);

           assert false;  // absurd case

         case Cons(_, _) =>

-          assert 1 <= h;

+          // assert 1 <= h;

           LowerThan_Lemma(t.children, index, h);

-          assert LowerThan(ch, h);

+          // assert LowerThan(ch, h);

       }

       // Putting these together, by ch.Cons? and the definition of LowerThan(ch, h), we get:

-      assert LowerThan(ch.head.children, h-1);

+      // assert LowerThan(ch.head.children, h-1);

       // And now we can invoke the induction hypothesis:

-      Proposition3b_Lemma(ch.head, h-1, tail);

+      // Proposition3b_Lemma(ch.head, h-1, tail);

   }

 }

 

@@ -627,30 +627,10 @@ colemma Path_Lemma2'(p: Stream<int>)
   }

 }

 colemma Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)

-  requires IsNeverEndingStream(p) && p.tail == tail;

-  ensures InfinitePath'(S2N'(n, tail));

+  requires IsNeverEndingStream(p) && p.tail == tail

+  ensures InfinitePath'(S2N'(n, tail))

 {

-  if n <= 0 {

-    calc {

-      InfinitePath'#[_k](S2N'(n, tail));

-      // def. S2N'

-      InfinitePath'#[_k](Zero(S2N(tail)));

-      // def. InfinitePath'

-      InfinitePath#[_k-1](S2N(tail));

-      { Path_Lemma2'(tail); }

-      true;

-    }

-  } else {

-    calc {

-      InfinitePath'#[_k](S2N'(n, tail));

-      // def. S2N'

-      InfinitePath'#[_k](Succ(S2N'(n-1, tail)));

-      // def. InfinitePath'

-      InfinitePath'#[_k-1](S2N'(n-1, tail));

-      { Path_Lemma2''(p, n-1, tail); }

-      true;

-    }

-  }

+  Path_Lemma2'(tail);

 }

 lemma Path_Lemma3(r: CoOption<Number>)

   ensures InfinitePath(r) ==> IsNeverEndingStream(N2S(r));