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.

1 files changed, 15 insertions, 17 deletions

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index a346aac5..662024e4 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -22,9 +22,9 @@ datatype Result = Fail | Res(t: Tree, sOut: seq<int>)
 // The postconditions state properties that are needed

 // in the completeness proof.

 function toList(d: int, t: Tree): seq<int>

-  ensures toList(d, t) != [] && toList(d, t)[0] >= d;

-  ensures (toList(d, t)[0] == d) == (t == Leaf);

-  decreases t;

+  ensures toList(d, t) != [] && toList(d, t)[0] >= d

+  ensures (toList(d, t)[0] == d) == (t == Leaf)

+  decreases t

 {

   match t

   case Leaf => [d]

@@ -43,10 +43,10 @@ function toList(d: int, t: Tree): seq<int>
 function method build_rec(d: int, s: seq<int>): Result

   ensures build_rec(d, s).Res? ==>

             |build_rec(d, s).sOut| < |s| &&

-            build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..];

+            build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..]

   ensures build_rec(d, s).Res? ==>

-            toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|];

-  decreases |s|, (if s==[] then 0 else s[0]-d);

+            toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|]

+  decreases |s|, (if s==[] then 0 else s[0]-d)

 {

   if s==[] || s[0] < d then

     Fail

@@ -68,7 +68,7 @@ function method build_rec(d: int, s: seq<int>): Result
 // sequence yields exactly the input sequence.

 // Completeness is proved as a lemma, see below.

 function method build(s: seq<int>): Result

-  ensures build(s).Res? ==> toList(0,build(s).t) == s;

+  ensures build(s).Res? ==> toList(0,build(s).t) == s

 {

   var r := build_rec(0, s);

   if r.Res? && r.sOut == [] then r else Fail

@@ -86,16 +86,14 @@ function method build(s: seq<int>): Result
 // correctly (encoded by calls to this lemma).

 lemma lemma0(t: Tree, d: int, s: seq<int>)

   ensures build_rec(d, toList(d, t) + s).Res? &&

-          build_rec(d, toList(d, t) + s).sOut == s;

+          build_rec(d, toList(d, t) + s).sOut == s

 {

   match(t) {

   case Leaf =>

     assert toList(d, t) == [d];

   case Node(l, r) =>

     assert toList(d, t) + s == toList(d+1, l) + (toList(d+1, r) + s);

-

-    lemma0(l, d+1, toList(d+1, r) + s);  // apply the induction hypothesis

-    lemma0(r, d+1, s);  // apply the induction hypothesis

+    // the rest follows from (two invocations of) the (automatically applied) induction hypothesis

   }

 }

 

@@ -107,8 +105,8 @@ lemma lemma0(t: Tree, d: int, s: seq<int>)
 // the following two lemmas replace these arguments

 // by quantified variables.

 lemma lemma1(t: Tree, s:seq<int>)

-  requires s == toList(0, t) + [];

-  ensures  build(s).Res?;

+  requires s == toList(0, t) + []

+  ensures build(s).Res?

 {

   lemma0(t, 0, []);

 }

@@ -117,7 +115,7 @@ lemma lemma1(t: Tree, s:seq<int>)
 // This lemma introduces the existential quantifier in the completeness

 // property.

 lemma lemma2(s: seq<int>)

-  ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;

+  ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?

 {

   forall t | toList(0,t) == s {

     lemma1(t, s);

@@ -131,7 +129,7 @@ lemma lemma2(s: seq<int>)
 // The body of the method converts the argument of lemma2

 // into a universally quantified variable.

 lemma completeness()

-  ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);

+  ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?)

 {

   forall s {

     lemma2(s);

@@ -145,7 +143,7 @@ lemma completeness()
 // unfold the necessary definitions.

 method harness0()

   ensures build([1,3,3,2]).Res? &&

-          build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf));

+          build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf))

 {

 }

 

@@ -155,6 +153,6 @@ method harness0()
 // assertions are required by the verifier to

 // unfold the necessary definitions.

 method harness1()

-  ensures build([1,3,2,2]).Fail?;

+  ensures build([1,3,2,2]).Fail?

 {

 }