[824] | 1 | include "common/Integers.ma". |
---|
| 2 | |
---|
| 3 | definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝ |
---|
| 4 | λm,n,x. \snd (split … x). |
---|
| 5 | |
---|
| 6 | lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉. |
---|
| 7 | #A #n #x elim x // |
---|
| 8 | qed. |
---|
| 9 | |
---|
| 10 | lemma truncate_eq : ∀n,x. truncate 0 n x = x. |
---|
| 11 | #n #x normalize >split_O_n @refl |
---|
| 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 | |
---|
| 43 | lemma add_with_carries_extend : ∀n,hx,hy,x,y,c. |
---|
| 44 | (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c |
---|
| 45 | in 〈tail ?? rs, tail ?? cs〉) = add_with_carries n x y c. |
---|
| 46 | #n #hx #hy #x #y #c |
---|
| 47 | >add_with_carries_unfold |
---|
| 48 | > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y) |
---|
| 49 | <add_with_carries_unfold |
---|
| 50 | cases (add_with_carries n x y c) |
---|
| 51 | // |
---|
| 52 | qed. |
---|
| 53 | |
---|
| 54 | lemma tail_plus_1 : ∀n,hx,hy,x,y. |
---|
| 55 | tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y. |
---|
| 56 | #n #hx #hy #x #y |
---|
| 57 | whd in ⊢ (??(???%)%) |
---|
| 58 | <(add_with_carries_extend n hx hy x y false) |
---|
| 59 | cases (add_with_carries (S n) (hx:::x) (hy:::y) false) |
---|
| 60 | // |
---|
| 61 | qed. |
---|
| 62 | |
---|
| 63 | lemma split_eq' : ∀A,m,n,v. split A m n v = split' A m n v. |
---|
| 64 | #A #m cases m |
---|
| 65 | [ #n cases n |
---|
| 66 | [ #v >(vempty … v) @refl |
---|
| 67 | | #n' #v >(hdtl … v) // |
---|
| 68 | ] |
---|
| 69 | | #m' #n #v >(hdtl … v) // |
---|
| 70 | ] qed. |
---|
| 71 | |
---|
| 72 | lemma split_left : ∀A,m,n,h,t. |
---|
| 73 | split A (S m) n (h:::t) = let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉. |
---|
| 74 | #A #m #n #h #t normalize >split_eq' @refl |
---|
| 75 | qed. |
---|
| 76 | |
---|
| 77 | lemma truncate_head : ∀m,n,h,t. |
---|
| 78 | truncate (S m) n (h:::t) = truncate m n t. |
---|
| 79 | #m #n #h #t normalize >split_eq' cases (split' bool m n t) // |
---|
| 80 | qed. |
---|
| 81 | |
---|
| 82 | lemma truncate_tail : ∀m,n,v. |
---|
| 83 | truncate (S m) n v = truncate m n (tail … v). |
---|
| 84 | // |
---|
| 85 | qed. |
---|
| 86 | |
---|
| 87 | lemma truncate_add_with_carries : ∀m,n,x,y,c. |
---|
| 88 | (let 〈rs,cs〉 ≝ add_with_carries … x y c in 〈truncate m n rs, truncate m n cs〉) = |
---|
| 89 | add_with_carries … (truncate … x) (truncate … y) c. |
---|
| 90 | #m elim m |
---|
| 91 | [ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs |
---|
| 92 | whd in ⊢ (??%?) >truncate_eq >truncate_eq @refl |
---|
| 93 | | #m' #IH #n #x #y #c |
---|
| 94 | >(hdtl … x) >(hdtl … y) |
---|
| 95 | >truncate_head >truncate_head <IH |
---|
| 96 | <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y)) |
---|
| 97 | cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%) |
---|
| 98 | <truncate_tail <truncate_tail @refl |
---|
| 99 | ] qed. |
---|
| 100 | |
---|
| 101 | lemma truncate_plus : ∀m,n,x,y. |
---|
| 102 | truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y). |
---|
| 103 | #m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries |
---|
| 104 | cases (add_with_carries ????) // |
---|
| 105 | qed. |
---|
| 106 | |
---|
| 107 | lemma truncate_pad : ∀m,n,x. |
---|
| 108 | truncate m n (pad … x) = x. |
---|
| 109 | #m0 elim m0 |
---|
| 110 | [ #n #x >truncate_eq // |
---|
| 111 | | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH |
---|
| 112 | ] qed. |
---|
| 113 | |
---|
| 114 | theorem zero_plus_reduce : ∀m,n,x,y. |
---|
| 115 | truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y. |
---|
| 116 | #m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%) |
---|
| 117 | @truncate_plus |
---|
| 118 | qed. |
---|
| 119 | |
---|
| 120 | definition sign_bit : ∀n. BitVector n → bool ≝ |
---|
| 121 | λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]. |
---|
| 122 | |
---|
| 123 | definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝ |
---|
| 124 | λm,n,v. pad_vector ? (sign_bit ? v) ?? v. |
---|
| 125 | |
---|
| 126 | lemma truncate_sign : ∀m,n,x. |
---|
| 127 | truncate m n (sign … x) = x. |
---|
| 128 | #m0 elim m0 |
---|
| 129 | [ #n #x >truncate_eq // |
---|
| 130 | | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH |
---|
| 131 | ] qed. |
---|
| 132 | |
---|
| 133 | theorem sign_plus_reduce : ∀m,n,x,y. |
---|
| 134 | truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y. |
---|
| 135 | #m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%) |
---|
| 136 | @truncate_plus |
---|
| 137 | qed. |
---|
| 138 | |
---|
| 139 | lemma sign_zero : ∀n,x. |
---|
| 140 | sign n O x = x. |
---|
| 141 | #n #x @refl qed. |
---|
| 142 | |
---|
| 143 | lemma sign_vcons : ∀m,n,x. |
---|
| 144 | sign m (S n) x = (sign_bit ? x):::(sign m n x). |
---|
| 145 | #m #n #x @refl |
---|
| 146 | qed. |
---|
| 147 | |
---|
| 148 | lemma sign_vcons_hd : ∀m,n,h,t. |
---|
| 149 | sign (S m) (S n) (h:::t) = h:::(sign (S m) n (h:::t)). |
---|
| 150 | // qed. |
---|
| 151 | |
---|
| 152 | lemma zero_vcons : ∀m. |
---|
| 153 | zero (S m) = false:::(zero m). |
---|
| 154 | // qed. |
---|
| 155 | |
---|
| 156 | lemma zero_sign : ∀m,n. |
---|
| 157 | sign m n (zero ?) = zero ?. |
---|
| 158 | #m #n elim n |
---|
| 159 | [ // |
---|
| 160 | | #n' #IH >sign_vcons >IH elim m // |
---|
| 161 | ] qed. |
---|
| 162 | |
---|
| 163 | lemma add_with_carries_vcons : ∀n,hx,hy,x,y,c. |
---|
| 164 | add_with_carries (S n) (hx:::x) (hy:::y) c |
---|
| 165 | = (let 〈rs,cs〉 ≝ add_with_carries n x y c in 〈?:::rs, ?:::cs〉). |
---|
| 166 | [ #n #hx #hy #x #y #c |
---|
| 167 | >add_with_carries_unfold |
---|
| 168 | > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y) |
---|
| 169 | <add_with_carries_unfold |
---|
| 170 | cases (add_with_carries n x y c) |
---|
| 171 | // |
---|
| 172 | | *: skip |
---|
| 173 | ] |
---|
| 174 | qed. |
---|
| 175 | |
---|
| 176 | lemma sign_bitflip : ∀m,n,x. |
---|
| 177 | negation_bv ? (sign (S m) n x) = sign (S m) n (negation_bv ? x). |
---|
| 178 | #m #n #x @(vector_inv_n … x) #h #t elim n |
---|
| 179 | [ @refl |
---|
| 180 | | #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl |
---|
| 181 | ] qed. |
---|
| 182 | |
---|
| 183 | lemma truncate_negation_bv : ∀m,n,x. |
---|
| 184 | truncate m n (negation_bv ? x) = negation_bv ? (truncate m n x). |
---|
| 185 | #m #n elim m |
---|
| 186 | [ #x >truncate_eq >truncate_eq @refl |
---|
| 187 | | #m' #IH #x @(vector_inv_n … x) #h #t >truncate_tail >truncate_tail |
---|
| 188 | >(IH t) @refl |
---|
| 189 | ] qed. |
---|
| 190 | |
---|
| 191 | lemma truncate_zero : ∀m,n. |
---|
| 192 | truncate m n (zero ?) = zero ?. |
---|
| 193 | #m #n elim m |
---|
| 194 | [ >truncate_eq @refl |
---|
| 195 | | #m' #IH >truncate_tail >zero_vcons <IH @refl |
---|
| 196 | ] qed. |
---|
| 197 | |
---|
| 198 | lemma zero_negate_reduce : ∀m,n,x. |
---|
| 199 | truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x. |
---|
| 200 | #m #n #x whd in ⊢ (??(???%)%) |
---|
| 201 | lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true) |
---|
| 202 | cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true) |
---|
| 203 | #rs #cs whd in ⊢ (??%? → ??(???%)?) |
---|
| 204 | >truncate_negation_bv |
---|
| 205 | >truncate_pad >truncate_zero cases (add_with_carries ????) |
---|
| 206 | #rs' #cs' #E destruct // |
---|
| 207 | qed. |
---|
| 208 | |
---|
| 209 | lemma sign_negate_reduce : ∀m,n,x. |
---|
| 210 | truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x. |
---|
| 211 | #m #n #x whd in ⊢ (??(???%)%) |
---|
| 212 | >sign_bitflip <(zero_sign (S n) m) |
---|
| 213 | 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) |
---|
| 214 | cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true) |
---|
| 215 | #rs #cs whd in ⊢ (??%? → ??(???%)?) |
---|
| 216 | >truncate_sign >truncate_sign cases (add_with_carries ????) |
---|
| 217 | #rs' #cs' #E destruct // |
---|
| 218 | qed. |
---|
| 219 | |
---|
| 220 | theorem zero_subtract_reduce : ∀m,n,x,y. |
---|
| 221 | truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y. |
---|
| 222 | #m #n #x #y |
---|
| 223 | whd in ⊢ (??(???%)%) |
---|
| 224 | lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false) |
---|
| 225 | cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false) |
---|
| 226 | #rs #cs whd in ⊢ (??%? → ??(???%)?) |
---|
| 227 | >zero_negate_reduce >truncate_pad |
---|
| 228 | cases (add_with_carries ????) |
---|
| 229 | #rs' #cs' #E destruct @refl |
---|
| 230 | qed. |
---|
| 231 | |
---|
| 232 | theorem sign_subtract_reduce : ∀m,n,x,y. |
---|
| 233 | truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y. |
---|
| 234 | #m #n #x #y |
---|
| 235 | whd in ⊢ (??(???%)%) |
---|
| 236 | 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) |
---|
| 237 | cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false) |
---|
| 238 | #rs #cs whd in ⊢ (??%? → ??(???%)?) |
---|
| 239 | >sign_negate_reduce >truncate_sign |
---|
| 240 | cases (add_with_carries ????) |
---|
| 241 | #rs' #cs' #E destruct @refl |
---|
| 242 | qed. |
---|