1 | include "common/Values.ma". |
---|
2 | |
---|
3 | definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝ |
---|
4 | λm,n,x. \snd (vsplit … x). |
---|
5 | |
---|
6 | lemma vsplit_O_n : ∀A,n,x. vsplit A O n x = 〈[[ ]], x〉. |
---|
7 | #A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ] |
---|
8 | qed. |
---|
9 | |
---|
10 | lemma truncate_eq : ∀n,x. truncate 0 n x = x. |
---|
11 | #n #x normalize >vsplit_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 | (* 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 | |
---|
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) |
---|
56 | #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta // |
---|
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 |
---|
62 | whd in ⊢ (??(???%)%); |
---|
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 | |
---|
68 | lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v. |
---|
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 | |
---|
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 |
---|
80 | qed. |
---|
81 | |
---|
82 | lemma truncate_head : ∀m,n,h,t. |
---|
83 | truncate (S m) n (h:::t) = truncate m n t. |
---|
84 | #m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) // |
---|
85 | qed. |
---|
86 | |
---|
87 | lemma truncate_tail : ∀m,n,v. |
---|
88 | truncate (S m) n v = truncate m n (tail … v). |
---|
89 | #m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl |
---|
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 |
---|
97 | whd in ⊢ (??%?); >truncate_eq >truncate_eq @refl |
---|
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)) |
---|
102 | cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%); |
---|
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). |
---|
108 | #m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries |
---|
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 // |
---|
116 | | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH |
---|
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. |
---|
121 | #m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%); |
---|
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. |
---|
127 | |
---|
128 | lemma truncate_sign : ∀m,n,x. |
---|
129 | truncate m n (sign … x) = x. |
---|
130 | #m0 elim m0 |
---|
131 | [ #n #x >truncate_eq // |
---|
132 | | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH |
---|
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. |
---|
137 | #m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%); |
---|
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) |
---|
173 | #lb #cs whd in ⊢ (??%%); >bool_eta |
---|
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 |
---|
183 | | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl |
---|
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. |
---|
203 | #m #n #x whd in ⊢ (??(???%)%); |
---|
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) |
---|
206 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
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. |
---|
214 | #m #n #x whd in ⊢ (??(???%)%); |
---|
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) |
---|
218 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
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 |
---|
226 | whd in ⊢ (??(???%)%); |
---|
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) |
---|
229 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
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 |
---|
238 | whd in ⊢ (??(???%)%); |
---|
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) |
---|
241 | #rs #cs whd in ⊢ (??%? → ??(???%)?); |
---|
242 | >sign_negate_reduce >truncate_sign |
---|
243 | cases (add_with_carries ????) |
---|
244 | #rs' #cs' #E destruct @refl |
---|
245 | qed. |
---|