diff options
| author |  leino <unknown> | 2015-05-07 08:55:44 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-07 08:55:44 -0700 |
| commit | cafbf508ea7aa6f337140293105060393ccb11f5 (patch) | |
| tree | 5885eeda1ea285e3b043da8ffa8d7633d0a6fc0d /Test/dafny0/InductivePredicates.dfy | |
| parent | f98a30f1ad7c441d8ef9e6e5740752723a43413a (diff) | |
Added "inductive lemma" methods
Diffstat (limited to 'Test/dafny0/InductivePredicates.dfy')
| -rw-r--r-- | Test/dafny0/InductivePredicates.dfy | 32 |
1 files changed, 32 insertions, 0 deletions
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)
{
|