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, 6 insertions, 7 deletions

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;

   }