[961] | 1 | include "common/Values.ma". |
---|
[824] | 2 | |
---|
| 3 | definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝ |
---|
[2032] | 4 | λm,n,x. \snd (vsplit … x). |
---|
[824] | 5 | |
---|
[2032] | 6 | lemma vsplit_O_n : ∀A,n,x. vsplit A O n x = 〈[[ ]], x〉. |
---|
[961] | 7 | #A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ] |
---|
[824] | 8 | qed. |
---|
| 9 | |
---|
| 10 | lemma truncate_eq : ∀n,x. truncate 0 n x = x. |
---|
[2032] | 11 | #n #x normalize >vsplit_O_n @refl |
---|
[824] | 12 | qed. |
---|
| 13 | |
---|
| 14 | lemma hdtl : ∀A,n. ∀x:Vector A (S n). x = (head' … x):::(tail … x). |
---|
| 15 | #A #n #x |
---|
| 16 | @(match x return λn. |
---|
| 17 | match n return λn.Vector A n → Prop with |
---|
| 18 | [ O ⇒ λ_.True |
---|
| 19 | | S m ⇒ λx:Vector A (S m). x = (head' A m x):::(tail A m x) ] |
---|
| 20 | with [ VEmpty ⇒ I | VCons p h t ⇒ ? ]) |
---|
| 21 | @refl |
---|
| 22 | qed. |
---|
| 23 | |
---|
| 24 | lemma vempty : ∀A. ∀x:Vector A O. x = [[ ]]. |
---|
| 25 | #A #x |
---|
| 26 | @(match x return λn. |
---|
| 27 | match n return λn.Vector A n → Prop with |
---|
| 28 | [ O ⇒ λx.x = [[ ]] |
---|
| 29 | | _ ⇒ λ_.True ] |
---|
| 30 | with [ VEmpty ⇒ ? | VCons _ _ _ ⇒ I ]) |
---|
| 31 | @refl |
---|
| 32 | qed. |
---|
| 33 | |
---|
| 34 | lemma fold_right2_i_unfold : ∀A,B,C,n,hx,hy,f,a,x,y. |
---|
| 35 | fold_right2_i A B C f a ? (hx:::x) (hy:::y) = |
---|
| 36 | f ? hx hy (fold_right2_i A B C f a n x y). |
---|
| 37 | // qed. |
---|
| 38 | |
---|
| 39 | lemma add_with_carries_unfold : ∀n,x,y,c. |
---|
| 40 | add_with_carries n x y c = fold_right2_i ????? n x y. |
---|
| 41 | // qed. |
---|
| 42 | |
---|
[1489] | 43 | (* add_with_carries was changed to make it whd nicely in some places, but we |
---|
| 44 | want to undo that for some lemmas. *) |
---|
| 45 | lemma bool_eta : ∀A:Type[0].∀b. ∀P:bool → A. if b then P true else P false = P b. |
---|
| 46 | #A * // qed. |
---|
| 47 | |
---|
[824] | 48 | lemma add_with_carries_extend : ∀n,hx,hy,x,y,c. |
---|
| 49 | (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c |
---|
| 50 | in 〈tail ?? rs, tail ?? cs〉) = add_with_carries n x y c. |
---|
| 51 | #n #hx #hy #x #y #c |
---|
| 52 | >add_with_carries_unfold |
---|
| 53 | > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y) |
---|
| 54 | <add_with_carries_unfold |
---|
| 55 | cases (add_with_carries n x y c) |
---|
[1516] | 56 | #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta // |
---|
[824] | 57 | qed. |
---|
| 58 | |
---|
| 59 | lemma tail_plus_1 : ∀n,hx,hy,x,y. |
---|
| 60 | tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y. |
---|
| 61 | #n #hx #hy #x #y |
---|
[1516] | 62 | whd in ⊢ (??(???%)%); |
---|
[824] | 63 | <(add_with_carries_extend n hx hy x y false) |
---|
| 64 | cases (add_with_carries (S n) (hx:::x) (hy:::y) false) |
---|
| 65 | // |
---|
| 66 | qed. |
---|
| 67 | |
---|
[2032] | 68 | lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v. |
---|
[824] | 69 | #A #m cases m |
---|
| 70 | [ #n cases n |
---|
| 71 | [ #v >(vempty … v) @refl |
---|
| 72 | | #n' #v >(hdtl … v) // |
---|
| 73 | ] |
---|
| 74 | | #m' #n #v >(hdtl … v) // |
---|
| 75 | ] qed. |
---|
| 76 | |
---|
[2032] | 77 | lemma vsplit_left : ∀A,m,n,h,t. |
---|
| 78 | vsplit A (S m) n (h:::t) = (let 〈l,r〉 ≝ vsplit A m n t in 〈h:::l,r〉). |
---|
| 79 | #A #m #n #h #t normalize >vsplit_eq' @refl |
---|
[824] | 80 | qed. |
---|
| 81 | |
---|
| 82 | lemma truncate_head : ∀m,n,h,t. |
---|
| 83 | truncate (S m) n (h:::t) = truncate m n t. |
---|
[2032] | 84 | #m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) // |
---|
[824] | 85 | qed. |
---|
| 86 | |
---|
| 87 | lemma truncate_tail : ∀m,n,v. |
---|
| 88 | truncate (S m) n v = truncate m n (tail … v). |
---|
[961] | 89 | #m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl |
---|
[824] | 90 | qed. |
---|
| 91 | |
---|
| 92 | lemma truncate_add_with_carries : ∀m,n,x,y,c. |
---|
| 93 | (let 〈rs,cs〉 ≝ add_with_carries … x y c in 〈truncate m n rs, truncate m n cs〉) = |
---|
| 94 | add_with_carries … (truncate … x) (truncate … y) c. |
---|
| 95 | #m elim m |
---|
| 96 | [ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs |
---|
[1516] | 97 | whd in ⊢ (??%?); >truncate_eq >truncate_eq @refl |
---|
[824] | 98 | | #m' #IH #n #x #y #c |
---|
| 99 | >(hdtl … x) >(hdtl … y) |
---|
| 100 | >truncate_head >truncate_head <IH |
---|
| 101 | <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y)) |
---|
[1516] | 102 | cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%); |
---|
[824] | 103 | <truncate_tail <truncate_tail @refl |
---|
| 104 | ] qed. |
---|
| 105 | |
---|
| 106 | lemma truncate_plus : ∀m,n,x,y. |
---|
| 107 | truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y). |
---|
[1516] | 108 | #m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries |
---|
[824] | 109 | cases (add_with_carries ????) // |
---|
| 110 | qed. |
---|
| 111 | |
---|
| 112 | lemma truncate_pad : ∀m,n,x. |
---|
| 113 | truncate m n (pad … x) = x. |
---|
| 114 | #m0 elim m0 |
---|
| 115 | [ #n #x >truncate_eq // |
---|
[1516] | 116 | | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH |
---|
[824] | 117 | ] qed. |
---|
| 118 | |
---|
| 119 | theorem zero_plus_reduce : ∀m,n,x,y. |
---|
| 120 | truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y. |
---|
[1516] | 121 | #m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%); |
---|
[824] | 122 | @truncate_plus |
---|
| 123 | qed. |
---|
| 124 | |
---|
| 125 | definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝ |
---|
| 126 | λm,n,v. pad_vector ? (sign_bit ? v) ?? v. |
---|
[961] | 127 | |
---|
[824] | 128 | lemma truncate_sign : ∀m,n,x. |
---|
| 129 | truncate m n (sign … x) = x. |
---|
| 130 | #m0 elim m0 |
---|
| 131 | [ #n #x >truncate_eq // |
---|
[1516] | 132 | | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH |
---|
[824] | 133 | ] qed. |
---|
| 134 | |
---|
| 135 | theorem sign_plus_reduce : ∀m,n,x,y. |
---|
| 136 | truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y. |
---|
[1516] | 137 | #m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%); |
---|
[824] | 138 | @truncate_plus |
---|
| 139 | qed. |
---|
| 140 | |
---|
| 141 | lemma sign_zero : ∀n,x. |
---|
| 142 | sign n O x = x. |
---|
| 143 | #n #x @refl qed. |
---|
| 144 | |
---|
| 145 | lemma sign_vcons : ∀m,n,x. |
---|
| 146 | sign m (S n) x = (sign_bit ? x):::(sign m n x). |
---|
| 147 | #m #n #x @refl |
---|
| 148 | qed. |
---|
| 149 | |
---|
| 150 | lemma sign_vcons_hd : ∀m,n,h,t. |
---|
| 151 | sign (S m) (S n) (h:::t) = h:::(sign (S m) n (h:::t)). |
---|
| 152 | // qed. |
---|
| 153 | |
---|
| 154 | lemma zero_vcons : ∀m. |
---|
| 155 | zero (S m) = false:::(zero m). |
---|
| 156 | // qed. |
---|
| 157 | |
---|
| 158 | lemma zero_sign : ∀m,n. |
---|
| 159 | sign m n (zero ?) = zero ?. |
---|
| 160 | #m #n elim n |
---|
| 161 | [ // |
---|
| 162 | | #n' #IH >sign_vcons >IH elim m // |
---|
| 163 | ] qed. |
---|
| 164 | |
---|
| 165 | lemma add_with_carries_vcons : ∀n,hx,hy,x,y,c. |
---|
| 166 | add_with_carries (S n) (hx:::x) (hy:::y) c |
---|
| 167 | = (let 〈rs,cs〉 ≝ add_with_carries n x y c in 〈?:::rs, ?:::cs〉). |
---|
| 168 | [ #n #hx #hy #x #y #c |
---|
| 169 | >add_with_carries_unfold |
---|
| 170 | > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y) |
---|
| 171 | <add_with_carries_unfold |
---|
| 172 | cases (add_with_carries n x y c) |
---|
[1516] | 173 | #lb #cs whd in ⊢ (??%%); >bool_eta |
---|
[824] | 174 | // |
---|
| 175 | | *: skip |
---|
| 176 | ] |
---|
| 177 | qed. |
---|
| 178 | |
---|
| 179 | lemma sign_bitflip : ∀m,n,x. |
---|
| 180 | negation_bv ? (sign (S m) n x) = sign (S m) n (negation_bv ? x). |
---|
| 181 | #m #n #x @(vector_inv_n … x) #h #t elim n |
---|
| 182 | [ @refl |
---|
[1516] | 183 | | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl |
---|
[824] | 184 | ] qed. |
---|
| 185 | |
---|
| 186 | lemma truncate_negation_bv : ∀m,n,x. |
---|
| 187 | truncate m n (negation_bv ? x) = negation_bv ? (truncate m n x). |
---|
| 188 | #m #n elim m |
---|
| 189 | [ #x >truncate_eq >truncate_eq @refl |
---|
| 190 | | #m' #IH #x @(vector_inv_n … x) #h #t >truncate_tail >truncate_tail |
---|
| 191 | >(IH t) @refl |
---|
| 192 | ] qed. |
---|
| 193 | |
---|
| 194 | lemma truncate_zero : ∀m,n. |
---|
| 195 | truncate m n (zero ?) = zero ?. |
---|
| 196 | #m #n elim m |
---|
| 197 | [ >truncate_eq @refl |
---|
| 198 | | #m' #IH >truncate_tail >zero_vcons <IH @refl |
---|
| 199 | ] qed. |
---|
| 200 | |
---|
| 201 | lemma zero_negate_reduce : ∀m,n,x. |
---|
| 202 | truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x. |
---|
[1516] | 203 | #m #n #x whd in ⊢ (??(???%)%); |
---|
[824] | 204 | lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true) |
---|
| 205 | cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true) |
---|
[1516] | 206 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
[824] | 207 | >truncate_negation_bv |
---|
| 208 | >truncate_pad >truncate_zero cases (add_with_carries ????) |
---|
| 209 | #rs' #cs' #E destruct // |
---|
| 210 | qed. |
---|
| 211 | |
---|
| 212 | lemma sign_negate_reduce : ∀m,n,x. |
---|
| 213 | truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x. |
---|
[1516] | 214 | #m #n #x whd in ⊢ (??(???%)%); |
---|
[824] | 215 | >sign_bitflip <(zero_sign (S n) m) |
---|
| 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 | cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true) |
---|
[1516] | 218 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
[824] | 219 | >truncate_sign >truncate_sign cases (add_with_carries ????) |
---|
| 220 | #rs' #cs' #E destruct // |
---|
| 221 | qed. |
---|
| 222 | |
---|
| 223 | theorem zero_subtract_reduce : ∀m,n,x,y. |
---|
| 224 | truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y. |
---|
| 225 | #m #n #x #y |
---|
[1516] | 226 | whd in ⊢ (??(???%)%); |
---|
[824] | 227 | lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false) |
---|
| 228 | cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false) |
---|
[1516] | 229 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
[824] | 230 | >zero_negate_reduce >truncate_pad |
---|
| 231 | cases (add_with_carries ????) |
---|
| 232 | #rs' #cs' #E destruct @refl |
---|
| 233 | qed. |
---|
| 234 | |
---|
| 235 | theorem sign_subtract_reduce : ∀m,n,x,y. |
---|
| 236 | truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y. |
---|
| 237 | #m #n #x #y |
---|
[1516] | 238 | whd in ⊢ (??(???%)%); |
---|
[824] | 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 | cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false) |
---|
[1516] | 241 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
[824] | 242 | >sign_negate_reduce >truncate_sign |
---|
| 243 | cases (add_with_carries ????) |
---|
| 244 | #rs' #cs' #E destruct @refl |
---|
| 245 | qed. |
---|