Dafny:

* Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction.
* For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited)
* In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)

1 files changed, 53 insertions, 0 deletions

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index f92e93e6..efd2f6f0 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -86,3 +86,56 @@ function G(d: Data): int
   case Lemon => G(d)

   case Kiwi(x) => 7

 }

+

+// -------- some things about induction ---------------------------------

+

+datatype Tree<T> {

+  Leaf(T);

+  Branch(Tree<T>, Tree<T>);

+}

+

+class DatatypeInduction<T> {

+  function LeafCount<G>(tree: Tree<G>): int

+  {

+    match tree

+    case Leaf(t) => 1

+    case Branch(left, right) => LeafCount(left) + LeafCount(right)

+  }

+

+  method Theorem0(tree: Tree<T>)

+    ensures 1 <= LeafCount(tree);

+  {

+    assert (forall t: Tree<T> {:induction} :: 1 <= LeafCount(t));

+  }

+

+  // also make sure it works for an instantiated generic datatype

+  method Theorem1(bt: Tree<bool>, it: Tree<int>)

+    ensures 1 <= LeafCount(bt);

+    ensures 1 <= LeafCount(it);

+  {

+    assert (forall t: Tree<bool> {:induction} :: 1 <= LeafCount(t));

+    assert (forall t: Tree<int> {:induction} :: 1 <= LeafCount(t));

+  }

+

+  method NotATheorem0(tree: Tree<T>)

+    ensures LeafCount(tree) % 2 == 1;

+  {

+    assert (forall t: Tree<T> {:induction} :: LeafCount(t) % 2 == 1);  // error: fails for Branch case

+  }

+

+  method NotATheorem1(tree: Tree<T>)

+    ensures 2 <= LeafCount(tree);

+  {

+    assert (forall t: Tree<T> {:induction} :: 2 <= LeafCount(t));  // error: fails for Leaf case

+  }

+

+  function Predicate(): bool

+  {

+    (forall t: Tree<T> {:induction} :: 2 <= LeafCount(t))

+  }

+

+  method NotATheorem2()

+  {

+    assert Predicate();  // error (this tests Related Location for induction via a predicate)

+  }

+}