From 6c4b0f1362ecea4c0fdc3e87ca9bc2de48158b82 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 28 Sep 2015 13:19:31 -0700
Subject: Improvements in proofs

---
 Test/dafny4/Leq.dfy | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny4/Leq.dfy b/Test/dafny4/Leq.dfy
index 046febcf..0491dd00 100644
--- a/Test/dafny4/Leq.dfy
+++ b/Test/dafny4/Leq.dfy
@@ -36,7 +36,6 @@ colemma NatCasesAux(a: Nat)
   ensures IsInfinity(a)
 {
   assert a != Num(0);
-  assert a != Z;
   if IsFinite(a.pred) {
     // going for a contradiction
     var m:nat :| a.pred == Num(m);
@@ -158,25 +157,18 @@ lemma CoLeq1'(a: Nat, b: Nat) returns (m: nat, n: nat)
   if !IsInfinity(b) {
     NatCases(b);
     n :| b == Num(n);
-    CoLeq1Aux(a, n);
-    m :| a == Num(m) && m <= n;
+    m := CoLeq1Aux(a, n);
   }
 }
 
-lemma CoLeq1Aux(a: Nat, n: nat)
+lemma CoLeq1Aux(a: Nat, n: nat) returns (m: nat)
   requires CoLeq(a, Num(n))
-  ensures exists m:nat :: a == Num(m) && m <= n
+  ensures a == Num(m) && m <= n
 {
-  var b := Num(n);
-  assert a == Z ||
-         (a.S? && b.S? && CoLeq(a.pred, b.pred));
   if a == Z {
-    assert a == Num(0);
+    m := 0;
   } else {
-    assert b.pred == Num(n-1);
-    assert a.S? && b.S? && CoLeq(a.pred, b.pred);
-    CoLeq1Aux(a.pred, n-1);
-    var m:nat :| a.pred == Num(m) && m <= n-1;
-    assert a == Num(m+1) && m+1 <= n-1+1;
+    m := CoLeq1Aux(a.pred, n-1);
+    m := m + 1;
   }
 }
-- 
cgit v1.2.3