From f28fa68497352ffb57ab2846da4cc1c1aeaf1968 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 12 Aug 2015 22:44:50 -0700
Subject: 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.

---
 Test/vstte2012/Tree.dfy | 32 +++++++++++++++-----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

(limited to 'Test/vstte2012')

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?
 {
 }
-- 
cgit v1.2.3