From 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 2 Oct 2015 15:26:56 -0700 Subject: 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]. --- Test/dafny0/CoinductiveProofs.dfy | 61 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 57 insertions(+), 4 deletions(-) (limited to 'Test/dafny0/CoinductiveProofs.dfy') 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 = Cons(head: T, tail: Stream) @@ -12,6 +12,7 @@ copredicate Pos(s: Stream) { 0 < s.head && Pos(s.tail) } +predicate FullPos(s: Stream) { 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 } } -- cgit v1.2.3 From cfe05df94a5ccb6025c94bd21b09bfc1240de756 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 2 Oct 2015 18:56:13 -0700 Subject: Made /rewriteFocalPredicates:1 the default --- Source/Dafny/DafnyOptions.cs | 8 ++++---- Test/dafny0/CoinductiveProofs.dfy | 2 +- Test/dafny0/InductivePredicates.dfy | 6 +++--- Test/dafny3/Filter.dfy | 6 +++--- Test/dafny4/NipkowKlein-chapter7.dfy | 12 ++++++------ 5 files changed, 17 insertions(+), 17 deletions(-) (limited to 'Test/dafny0/CoinductiveProofs.dfy') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 2d8756d2..b61ba555 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny public bool CountVerificationErrors = true; public bool Optimize = false; public bool AutoTriggers = false; - public bool RewriteFocalPredicates = false; + public bool RewriteFocalPredicates = true; public bool PrintTooltips = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; @@ -379,9 +379,9 @@ namespace Microsoft.Dafny 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. /rewriteFocalPredicates: - 0 (default) - Don't rewrite predicates in the body of prefix lemmas. - 1 - In the body of prefix lemmas, rewrite any use of a focal predicate - P to P#[_k-1]. + 0 - Don't rewrite predicates in the body of prefix lemmas. + 1 (default) - In the body of prefix lemmas, rewrite any use of a focal predicate + P to P#[_k-1]. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy index 0dce8af9..c8bb45c7 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" /rewriteFocalPredicates:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" codatatype Stream = Cons(head: T, tail: Stream) diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy index 8d05af11..e9aa7604 100644 --- a/Test/dafny0/InductivePredicates.dfy +++ b/Test/dafny0/InductivePredicates.dfy @@ -58,7 +58,7 @@ inductive lemma {:induction false} IL_EvenBetter(x: natinf) if { case x.N? && x.n == 0 => // trivial - case x.N? && 2 <= x.n && Even(N(x.n - 2)) => + case x.N? && 2 <= x.n && Even(N(x.n - 2)) => // syntactic rewrite makes this like in IL IL_EvenBetter(N(x.n - 2)); } } @@ -142,7 +142,7 @@ module Alt { } } - inductive lemma {:induction false} MyLemma_NiceButNotFast(x: natinf) + inductive lemma {:induction false} MyLemma_Nicer(x: natinf) // same as MyLemma_NotSoNice but relying on syntactic rewrites requires Even(x) ensures x.N? && x.n % 2 == 0 { @@ -151,7 +151,7 @@ module Alt { // trivial case exists y :: x == S(S(y)) && Even(y) => var y :| x == S(S(y)) && Even(y); - MyLemma_NiceButNotFast(y); + MyLemma_Nicer(y); assert x.n == y.n + 2; } } diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index 6f541396..4f8b35ec 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -157,11 +157,11 @@ colemma Filter_IsSubStream(s: Stream, P: Predicate) calc { true; == { Filter_IsSubStream(s.tail, P); } // induction hypothesis - IsSubStream#[_k-1](Filter(s.tail, P), s.tail); + IsSubStream(Filter(s.tail, P), s.tail); == // { assert Filter(s.tail, h) == Filter(s, h).tail; } - IsSubStream#[_k-1](Filter(s, P).tail, s.tail); + IsSubStream(Filter(s, P).tail, s.tail); ==> { Lemma_TailSubStreamK(Filter(s, P).tail, s, _k-1); } - IsSubStream#[_k-1](Filter(s, P).tail, s); + IsSubStream(Filter(s, P).tail, s); } calc { In(Filter(s, P).head, s); diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy index aae94550..0c089895 100644 --- a/Test/dafny4/NipkowKlein-chapter7.dfy +++ b/Test/dafny4/NipkowKlein-chapter7.dfy @@ -162,8 +162,8 @@ inductive lemma SmallStep_is_deterministic(cs: (com, state), cs': (com, state), case Seq(c0, c1) => if c0 == SKIP { } else { - var c0' :| cs'.0 == Seq(c0', c1) && small_step#[_k-1](c0, cs.1, c0', cs'.1); - var c0'' :| cs''.0 == Seq(c0'', c1) && small_step#[_k-1](c0, cs.1, c0'', cs''.1); + var c0' :| cs'.0 == Seq(c0', c1) && small_step(c0, cs.1, c0', cs'.1); + var c0'' :| cs''.0 == Seq(c0'', c1) && small_step(c0, cs.1, c0'', cs''.1); SmallStep_is_deterministic((c0, cs.1), (c0', cs'.1), (c0'', cs''.1)); } case If(b, thn, els) => @@ -200,7 +200,7 @@ inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state) case Assign(x, a) => assert small_step_star(SKIP, t, SKIP, t); case Seq(c0, c1) => - var s' :| big_step#[_k-1](c0, s, s') && big_step#[_k-1](c1, s', t); + var s' :| big_step(c0, s, s') && big_step(c1, s', t); calc <== { small_step_star(c, s, SKIP, t); { star_transitive(Seq(c0, c1), s, Seq(SKIP, c1), s', SKIP, t); } @@ -226,7 +226,7 @@ inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state) true; } } else { - var s' :| big_step#[_k-1](body, s, s') && big_step#[_k-1](While(b, body), s', t); + var s' :| big_step(body, s, s') && big_step(While(b, body), s', t); calc <== { small_step_star(c, s, SKIP, t); { assert small_step(c, s, If(b, Seq(body, While(b, body)), SKIP), s); } @@ -253,7 +253,7 @@ inductive lemma lemma_7_13(c0: com, s0: state, c: com, t: state, c1: com) { if c0 == c && s0 == t { } else { - var c', s' :| small_step(c0, s0, c', s') && small_step_star#[_k-1](c', s', c, t); + var c', s' :| small_step(c0, s0, c', s') && small_step_star(c', s', c, t); lemma_7_13(c', s', c, t, c1); } } @@ -264,7 +264,7 @@ inductive lemma SmallStepStar_implies_BigStep(c: com, s: state, t: state) { if c == SKIP && s == t { } else { - var c', s' :| small_step(c, s, c', s') && small_step_star#[_k-1](c', s', SKIP, t); + var c', s' :| small_step(c, s, c', s') && small_step_star(c', s', SKIP, t); SmallStep_plus_BigStep(c, s, c', s', t); } } -- cgit v1.2.3