Added "inductive lemma" methods

4 files changed, 61 insertions, 11 deletions

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 850fa4c1..d1b04b1d 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -219,6 +219,19 @@ module InductivePredicateResolutionErrors {
       h < 0 && CoLetSuchThat(s.tail)  // error: recursive call to copredicate in body of let-such-that

   }

 

+  inductive predicate NegatedLetSuchThat(s: List<int>)

+  {

+    if s != Nil then true else

+      !var h :| h == s.head;

+      h < 0 && !NegatedLetSuchThat(s.tail)  // error: recursive call to inductive predicate in body of let-such-that

+  }

+  copredicate NegatedCoLetSuchThat(s: IList<int>)

+  {

+    if s != INil then true else

+      !var h :| h == s.head;

+      h < 0 && !NegatedCoLetSuchThat(s.tail)  // this is fine for a coinductive predicate

+  }

+

   inductive predicate CP(i: int)

   {

     CP(i) &&

diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect
index 0ab15059..4821a0e3 100644
--- a/Test/dafny0/Coinductive.dfy.expect
+++ b/Test/dafny0/Coinductive.dfy.expect
@@ -19,12 +19,13 @@ Coinductive.dfy(205,8): Error: an inductive predicate can be called recursively
 Coinductive.dfy(206,8): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

 Coinductive.dfy(206,21): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

 Coinductive.dfy(219,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(225,5): Error: an inductive predicate can be called recursively only in positive positions

-Coinductive.dfy(228,28): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(229,29): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(230,17): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(240,12): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(246,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(247,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(267,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates

-29 resolution/type errors detected in Coinductive.dfy

+Coinductive.dfy(226,16): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(238,5): Error: an inductive predicate can be called recursively only in positive positions

+Coinductive.dfy(241,28): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(242,29): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(243,17): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(253,12): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(259,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(260,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(280,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates

+30 resolution/type errors detected in Coinductive.dfy

diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy
index 9250fade..5f1184f1 100644
--- a/Test/dafny0/InductivePredicates.dfy
+++ b/Test/dafny0/InductivePredicates.dfy
@@ -39,6 +39,38 @@ lemma M'(k: nat, x: natinf)
   }

 }

 

+// Here is the same proof as in M / M', but packaged into a single "inductive lemma":

+inductive lemma IL(x: natinf)

+  requires Even(x)

+  ensures x.N? && x.n % 2 == 0

+{

+  if {

+    case x.N? && x.n == 0 =>

+      // trivial

+    case x.N? && 2 <= x.n && Even#[_k-1](N(x.n - 2)) =>

+      IL(N(x.n - 2));

+  }

+}

+

+inductive lemma IL_EvenBetter(x: natinf)

+  requires Even(x)

+  ensures x.N? && x.n % 2 == 0

+{

+  if {

+    case x.N? && x.n == 0 =>

+      // trivial

+    case x.N? && 2 <= x.n && Even(N(x.n - 2)) =>

+      IL_EvenBetter(N(x.n - 2));

+  }

+}

+

+inductive lemma IL_Bad(x: natinf)

+  requires Even(x)

+  ensures x.N? && x.n % 2 == 0

+{

+  assert false;  // error: one shouldn't be able to prove just anything

+}

+

 lemma InfNotEven()

   ensures !Even(Inf)

 {

diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect
index c0feb7dd..a57b7d70 100644
--- a/Test/dafny0/InductivePredicates.dfy.expect
+++ b/Test/dafny0/InductivePredicates.dfy.expect
@@ -1,5 +1,9 @@
-InductivePredicates.dfy(51,11): Error: assertion violation

+InductivePredicates.dfy(71,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+InductivePredicates.dfy(83,11): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 13 verified, 1 error

+Dafny program verifier finished with 18 verified, 2 errors