Changeset 1489 for src/Clight/casts.ma

Timestamp:

Nov 4, 2011, 12:39:56 PM (9 years ago)

Author:

campbell

Message:

Fix up a couple of lemmas affected by the change to add_with_carries.

File:

• src/Clight/casts.ma (modified) (3 diffs)

src/Clight/casts.ma

@@ -41 +41 @@
 // qed.
 
+(* add_with_carries was changed to make it whd nicely in some places, but we
+   want to undo that for some lemmas. *)
+lemma bool_eta : ∀A:Type[0].∀b. ∀P:bool → A. if b then P true else P false = P b.
+#A * // qed.
+
 lemma add_with_carries_extend : ∀n,hx,hy,x,y,c.
   (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c
@@ -49 +54 @@
 <add_with_carries_unfold
 cases (add_with_carries n x y c)
-//
+#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //
 qed.
 
@@ -166 +171 @@
   <add_with_carries_unfold
   cases (add_with_carries n x y c)
+  #lb #cs whd in ⊢ (??%%) >bool_eta
   //
 | *: skip