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, 4 insertions, 4 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);

   }

 }