Changeset 1516 for src/Clight/casts.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/casts.ma
r1489 r1516 54 54 <add_with_carries_unfold 55 55 cases (add_with_carries n x y c) 56 #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //56 #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta // 57 57 qed. 58 58 … … 60 60 tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y. 61 61 #n #hx #hy #x #y 62 whd in ⊢ (??(???%)%) 62 whd in ⊢ (??(???%)%); 63 63 <(add_with_carries_extend n hx hy x y false) 64 64 cases (add_with_carries (S n) (hx:::x) (hy:::y) false) … … 95 95 #m elim m 96 96 [ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs 97 whd in ⊢ (??%?) >truncate_eq >truncate_eq @refl97 whd in ⊢ (??%?); >truncate_eq >truncate_eq @refl 98 98 | #m' #IH #n #x #y #c 99 99 >(hdtl … x) >(hdtl … y) 100 100 >truncate_head >truncate_head <IH 101 101 <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y)) 102 cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%) 102 cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%); 103 103 <truncate_tail <truncate_tail @refl 104 104 ] qed. … … 106 106 lemma truncate_plus : ∀m,n,x,y. 107 107 truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y). 108 #m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries108 #m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries 109 109 cases (add_with_carries ????) // 110 110 qed. … … 114 114 #m0 elim m0 115 115 [ #n #x >truncate_eq // 116 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH116 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH 117 117 ] qed. 118 118 119 119 theorem zero_plus_reduce : ∀m,n,x,y. 120 120 truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y. 121 #m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)121 #m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%); 122 122 @truncate_plus 123 123 qed. … … 130 130 #m0 elim m0 131 131 [ #n #x >truncate_eq // 132 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH132 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH 133 133 ] qed. 134 134 135 135 theorem sign_plus_reduce : ∀m,n,x,y. 136 136 truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y. 137 #m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)137 #m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%); 138 138 @truncate_plus 139 139 qed. … … 171 171 <add_with_carries_unfold 172 172 cases (add_with_carries n x y c) 173 #lb #cs whd in ⊢ (??%%) >bool_eta173 #lb #cs whd in ⊢ (??%%); >bool_eta 174 174 // 175 175 | *: skip … … 181 181 #m #n #x @(vector_inv_n … x) #h #t elim n 182 182 [ @refl 183 | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl183 | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl 184 184 ] qed. 185 185 … … 201 201 lemma zero_negate_reduce : ∀m,n,x. 202 202 truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x. 203 #m #n #x whd in ⊢ (??(???%)%) 203 #m #n #x whd in ⊢ (??(???%)%); 204 204 lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true) 205 205 cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true) 206 #rs #cs whd in ⊢ (??%? → ??(???%)?) 206 #rs #cs whd in ⊢ (??%? → ??(???%)?); 207 207 >truncate_negation_bv 208 208 >truncate_pad >truncate_zero cases (add_with_carries ????) … … 212 212 lemma sign_negate_reduce : ∀m,n,x. 213 213 truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x. 214 #m #n #x whd in ⊢ (??(???%)%) 214 #m #n #x whd in ⊢ (??(???%)%); 215 215 >sign_bitflip <(zero_sign (S n) m) 216 216 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) 217 217 cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true) 218 #rs #cs whd in ⊢ (??%? → ??(???%)?) 218 #rs #cs whd in ⊢ (??%? → ??(???%)?); 219 219 >truncate_sign >truncate_sign cases (add_with_carries ????) 220 220 #rs' #cs' #E destruct // … … 224 224 truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y. 225 225 #m #n #x #y 226 whd in ⊢ (??(???%)%) 226 whd in ⊢ (??(???%)%); 227 227 lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false) 228 228 cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false) 229 #rs #cs whd in ⊢ (??%? → ??(???%)?) 229 #rs #cs whd in ⊢ (??%? → ??(???%)?); 230 230 >zero_negate_reduce >truncate_pad 231 231 cases (add_with_carries ????) … … 236 236 truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y. 237 237 #m #n #x #y 238 whd in ⊢ (??(???%)%) 238 whd in ⊢ (??(???%)%); 239 239 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) 240 240 cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false) 241 #rs #cs whd in ⊢ (??%? → ??(???%)?) 241 #rs #cs whd in ⊢ (??%? → ??(???%)?); 242 242 >sign_negate_reduce >truncate_sign 243 243 cases (add_with_carries ????)
Note: See TracChangeset
for help on using the changeset viewer.