diff options
| author |  leino <unknown> | 2015-05-07 09:42:21 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-07 09:42:21 -0700 |
| commit | 9e999ccbf8581acf181ff00a529de96e12c690d5 (patch) | |
| tree | 0b9bd5d56a2f7a41dc520274d8d110bee997f5b1 /Test/dafny0/InductivePredicates.dfy | |
| parent | cafbf508ea7aa6f337140293105060393ccb11f5 (diff) | |
Additional test case for inductive predicates
Diffstat (limited to 'Test/dafny0/InductivePredicates.dfy')
| -rw-r--r-- | Test/dafny0/InductivePredicates.dfy | 83 |
1 files changed, 76 insertions, 7 deletions
diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy index 5f1184f1..424118e7 100644 --- a/Test/dafny0/InductivePredicates.dfy +++ b/Test/dafny0/InductivePredicates.dfy @@ -3,13 +3,6 @@ datatype natinf = N(n: nat) | Inf
-function S(x: natinf): natinf
-{
- match x
- case N(n) => N(n+1)
- case Inf => Inf
-}
-
inductive predicate Even(x: natinf)
{
(x.N? && x.n == 0) ||
@@ -104,3 +97,79 @@ lemma OneMore(x: natinf) returns (y: natinf) {
y := N(x.n + 2);
}
+
+// ----------------------- Here's another version of Even, using the S function
+
+module Alt {
+ datatype natinf = N(n: nat) | Inf
+
+ function S(x: natinf): natinf
+ {
+ match x
+ case N(n) => N(n+1)
+ case Inf => Inf
+ }
+
+ inductive predicate Even(x: natinf)
+ {
+ (x.N? && x.n == 0) ||
+ exists y :: x == S(S(y)) && Even(y)
+ }
+
+ inductive lemma MyLemma_NotSoNice(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+ {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case exists y :: x == S(S(y)) && Even#[_k-1](y) =>
+ var y :| x == S(S(y)) && Even#[_k-1](y);
+ MyLemma_NotSoNice(y);
+ assert x.n == y.n + 2;
+ }
+ }
+
+ inductive lemma MyLemma_NiceButNotFast(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+ {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case exists y :: x == S(S(y)) && Even(y) =>
+ var y :| x == S(S(y)) && Even(y);
+ MyLemma_NiceButNotFast(y);
+ assert x.n == y.n + 2;
+ }
+ }
+
+ lemma InfNotEven()
+ ensures !Even(Inf)
+ {
+ if Even(Inf) {
+ InfNotEven_Aux();
+ }
+ }
+
+ inductive lemma InfNotEven_Aux()
+ requires Even(Inf)
+ ensures false
+ {
+ var x := Inf;
+ if {
+ case x.N? && x.n == 0 =>
+ assert false; // this case is absurd
+ case exists y :: x == S(S(y)) && Even(y) =>
+ var y :| x == S(S(y)) && Even(y);
+ assert y == Inf;
+ InfNotEven_Aux();
+ }
+ }
+
+ lemma NextEven(x: natinf)
+ requires Even(x)
+ ensures Even(S(S(x)))
+ {
+ }
+}
|