Changeset 1516 for src/Clight/casts.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (9 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

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

src/Clight/casts.ma

@@ -54 +54 @@
 <add_with_carries_unfold
 cases (add_with_carries n x y c)
-#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //
+#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta //
 qed.
 
@@ -60 +60 @@
   tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
 #n #hx #hy #x #y
-whd in ⊢ (??(???%)%)
+whd in ⊢ (??(???%)%);
 <(add_with_carries_extend n hx hy x y false)
 cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
@@ -95 +95 @@
 #m elim m
 [ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
-  whd in ⊢ (??%?) >truncate_eq >truncate_eq  @refl
+  whd in ⊢ (??%?); >truncate_eq >truncate_eq  @refl
 | #m' #IH #n #x #y #c
   >(hdtl … x) >(hdtl … y)
   >truncate_head >truncate_head <IH
   <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
-  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%)
+  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%);
   <truncate_tail <truncate_tail @refl
 ] qed.
@@ -106 +106 @@
 lemma truncate_plus : ∀m,n,x,y.
   truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
-#m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries 
+#m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries 
 cases (add_with_carries ????) //
 qed.
@@ -114 +114 @@
 #m0 elim m0
 [ #n #x >truncate_eq //
-| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
+| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
 ] qed.
 
 theorem zero_plus_reduce : ∀m,n,x,y. 
   truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
-#m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
+#m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%);
 @truncate_plus
 qed.
@@ -130 +130 @@
 #m0 elim m0
 [ #n #x >truncate_eq //
-| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
+| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
 ] qed.
 
 theorem sign_plus_reduce : ∀m,n,x,y. 
   truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
-#m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
+#m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%);
 @truncate_plus
 qed.
@@ -171 +171 @@
   <add_with_carries_unfold
   cases (add_with_carries n x y c)
-  #lb #cs whd in ⊢ (??%%) >bool_eta
+  #lb #cs whd in ⊢ (??%%); >bool_eta
   //
 | *: skip
@@ -181 +181 @@
 #m #n #x @(vector_inv_n … x) #h #t elim n
 [ @refl
-| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
+| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl
 ] qed.
 
@@ -201 +201 @@
 lemma zero_negate_reduce : ∀m,n,x.
   truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
-#m #n #x whd in ⊢ (??(???%)%)
+#m #n #x whd in ⊢ (??(???%)%);
 lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
 cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
-#rs #cs whd in ⊢ (??%? → ??(???%)?)
+#rs #cs whd in ⊢ (??%? → ??(???%)?);
 >truncate_negation_bv
 >truncate_pad >truncate_zero cases (add_with_carries ????)
@@ -212 +212 @@
 lemma sign_negate_reduce : ∀m,n,x.
   truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
-#m #n #x whd in ⊢ (??(???%)%)
+#m #n #x whd in ⊢ (??(???%)%);
 >sign_bitflip <(zero_sign (S n) m)
 lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
 cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
-#rs #cs whd in ⊢ (??%? → ??(???%)?)
+#rs #cs whd in ⊢ (??%? → ??(???%)?);
 >truncate_sign >truncate_sign cases (add_with_carries ????)
 #rs' #cs' #E destruct //
@@ -224 +224 @@
   truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
 #m #n #x #y
-whd in ⊢ (??(???%)%)
+whd in ⊢ (??(???%)%);
 lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
 cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
-#rs #cs whd in ⊢ (??%? → ??(???%)?)
+#rs #cs whd in ⊢ (??%? → ??(???%)?);
 >zero_negate_reduce >truncate_pad
 cases (add_with_carries ????)
@@ -236 +236 @@
   truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
 #m #n #x #y
-whd in ⊢ (??(???%)%)
+whd in ⊢ (??(???%)%);
 lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
 cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
-#rs #cs whd in ⊢ (??%? → ??(???%)?)
+#rs #cs whd in ⊢ (??%? → ??(???%)?);
 >sign_negate_reduce >truncate_sign
 cases (add_with_carries ????)