Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/lemmas (this fixes an item from the wishlist).

Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?).
Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1].

2 files changed, 103 insertions, 23 deletions

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index d990ae51..0dce8af9 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /rewriteFocalPredicates:1 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 codatatype Stream<T> = Cons(head: T, tail: Stream)

@@ -12,6 +12,7 @@ copredicate Pos(s: Stream<int>)
 {

   0 < s.head && Pos(s.tail)

 }

+predicate FullPos(s: Stream<int>) { Pos(s) }  // a way in the test file to sidestep focal-predicate rewrites

 

 colemma {:induction false} PosLemma0(n: int)

   requires 1 <= n;

@@ -26,7 +27,25 @@ colemma {:induction false} PosLemma1(n: int)
 {

   PosLemma1(n + 1);

   if (*) {

-    assert Pos(Upward(n + 1));  // error: cannot conclude this here, because we only have prefix predicates

+    assert FullPos(Upward(n + 1));  // error: cannot conclude this here, because we only have prefix predicates

+  }

+}

+

+colemma {:induction false} PosLemma2(n: int)

+  requires 1 <= n;

+  ensures Pos(Upward(n));

+{

+  PosLemma2(n + 1);

+  if (*) {

+    assert Pos(Upward(n + 1));  // Pos gets rewritten to Pos#[_k-1], which does hold

+  } else if (*) {

+    assert Pos#[_k-1](Upward(n + 1));  // explicitly saying Pos#[_k-1] also holds

+  } else if (*) {

+    assert Pos#[_k](Upward(n + 1));  // error: this is not known to hold for _k and n+1

+  } else if (*) {

+    assert Pos#[_k](Upward(n));  // but it does hold with Pos#[_k] and n (which is the postcondition of the prefix lemma)

+  } else if (*) {

+    assert Pos#[_k+1](Upward(n));  // error: this is too much to ask for

   }

 }

 

@@ -65,13 +84,29 @@ colemma {:induction false} AlwaysLemma_X1(s: Stream)
 {

   AlwaysLemma_X1(s);  // this is the right proof

 }

+predicate FullX(s: Stream) { X(s) }  // a way in the test file to sidestep focal-predicate rewrites

 

 colemma {:induction false} AlwaysLemma_X2(s: Stream)

   ensures X(s);

 {

   AlwaysLemma_X2(s);

   if (*) {

-    assert X(s);  // error: cannot conclude the full predicate here

+    assert FullX(s);  // error: cannot conclude the full predicate here

+  }

+}

+

+colemma {:induction false} AlwaysLemma_X3(s: Stream)

+  ensures X(s);

+{

+  AlwaysLemma_X3(s);

+  if (*) {

+    assert X(s);  // holds, because it gets rewritten to X#[_k-1]

+  } else if (*) {

+    assert X#[_k-1](s);  // explicitly saying X#[_k-1] also holds

+  } else if (*) {

+    assert X#[_k](s);  // in fact, X#[_k] holds, too (which is the postcondition of the prefix lemma)

+  } else if (*) {

+    assert X#[_k+1](s);  // as it turns out, this holds too, since the definition of X makes X#[_k+1] equal X#[_k]

   }

 }

 

@@ -79,6 +114,7 @@ copredicate Y(s: Stream)  // this is equivalent to always returning 'true'
 {

   Y(s.tail)

 }

+predicate FullY(s: Stream) { Y(s) }  // a way in the test file to sidestep focal-predicate rewrites

 

 colemma {:induction false} AlwaysLemma_Y0(s: Stream)

   ensures Y(s);  // prove that Y(s) really is always 'true'

@@ -97,7 +133,24 @@ colemma {:induction false} AlwaysLemma_Y2(s: Stream)
 {

   AlwaysLemma_Y2(s.tail);

   if (*) {

-    assert Y(s.tail);  // error: not provable here

+    assert FullY(s.tail);  // error: not provable here

+  }

+}

+

+colemma {:induction false} AlwaysLemma_Y3(s: Stream)

+  ensures Y(s);

+{

+  AlwaysLemma_Y3(s.tail);

+  if (*) {

+    assert Y(s.tail);  // this holds, because it's rewritten to Y#[_k-1]

+  } else if (*) {

+    assert Y#[_k-1](s.tail);

+  } else if (*) {

+    assert Y#[_k](s.tail);  // error: not known to hold for _k and s.tail

+  } else if (*) {

+    assert Y#[_k](s);  // this is also the postcondition of the prefix lemma

+  } else if (*) {

+    assert Y#[_k+1](s);  // error: this is too much to ask for

   }

 }

 

diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect
index 2a5a2b0b..c4f4c405 100644
--- a/Test/dafny0/CoinductiveProofs.dfy.expect
+++ b/Test/dafny0/CoinductiveProofs.dfy.expect
@@ -1,50 +1,77 @@
-CoinductiveProofs.dfy(29,11): Error: assertion violation

+CoinductiveProofs.dfy(30,11): Error: assertion violation

+CoinductiveProofs.dfy(15,36): Related location

 CoinductiveProofs.dfy(13,16): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

-CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(54,2): Related location

+CoinductiveProofs.dfy(44,11): Error: assertion violation

+CoinductiveProofs.dfy(13,16): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon16_Then

+CoinductiveProofs.dfy(48,11): Error: assertion violation

+CoinductiveProofs.dfy(13,16): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon18_Then

+CoinductiveProofs.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(77,10): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(73,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(74,11): Error: assertion violation

-CoinductiveProofs.dfy(54,2): Related location

+CoinductiveProofs.dfy(94,11): Error: assertion violation

+CoinductiveProofs.dfy(87,29): Related location

+CoinductiveProofs.dfy(73,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

-CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(80,2): Related location

+CoinductiveProofs.dfy(127,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(126,10): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(115,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(100,11): Error: assertion violation

-CoinductiveProofs.dfy(80,2): Related location

+CoinductiveProofs.dfy(136,11): Error: assertion violation

+CoinductiveProofs.dfy(117,29): Related location

+CoinductiveProofs.dfy(115,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

-CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(106,2): Related location

+CoinductiveProofs.dfy(149,11): Error: assertion violation

+CoinductiveProofs.dfy(115,2): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon16_Then

+CoinductiveProofs.dfy(153,11): Error: assertion violation

+CoinductiveProofs.dfy(115,2): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon18_Then

+CoinductiveProofs.dfy(164,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(163,10): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(159,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(203,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(202,21): Related location: This is the postcondition that might not hold.

 CoinductiveProofs.dfy(4,23): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(209,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(208,21): Related location: This is the postcondition that might not hold.

 CoinductiveProofs.dfy(4,23): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

 

-Dafny program verifier finished with 35 verified, 8 errors

+Dafny program verifier finished with 42 verified, 12 errors