source: src/Clight/casts.ma @ 824

Last change on this file since 824 was 824, checked in by campbell, 9 years ago

Some work on showing that casts around integer operations can be removed.

File size: 7.5 KB
RevLine 
[824]1include "common/Integers.ma".
2
3definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
4λm,n,x. \snd (split … x).
5
6lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
7#A #n #x elim x //
8qed.
9
10lemma truncate_eq : ∀n,x. truncate 0 n x = x.
11#n #x normalize >split_O_n @refl
12qed.
13
14lemma 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
22qed.
23
24lemma 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
32qed.
33
34lemma 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
39lemma 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
43lemma 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
50cases (add_with_carries n x y c)
51//
52qed.
53
54lemma 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
57whd in ⊢ (??(???%)%)
58<(add_with_carries_extend n hx hy x y false)
59cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
60//
61qed.
62
63lemma 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
72lemma 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
75qed.
76
77lemma 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) //
80qed.
81
82lemma truncate_tail : ∀m,n,v.
83  truncate (S m) n v = truncate m n (tail … v).
84  //
85  qed.
86
87lemma 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
101lemma 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
104cases (add_with_carries ????) //
105qed.
106
107lemma 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
114theorem 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
118qed.
119
120definition sign_bit : ∀n. BitVector n → bool ≝
121λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
122
123definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
124λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
125
126lemma 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
133theorem 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
137qed.
138
139lemma sign_zero : ∀n,x.
140  sign n O x = x.
141#n #x @refl qed.
142
143lemma sign_vcons : ∀m,n,x.
144  sign m (S n) x = (sign_bit ? x):::(sign m n x).
145#m #n #x @refl
146qed.
147
148lemma 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
152lemma zero_vcons : ∀m.
153  zero (S m) = false:::(zero m).
154// qed.
155
156lemma 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
163lemma 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]
174qed.
175
176lemma 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
183lemma 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
191lemma 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
198lemma 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 ⊢ (??(???%)%)
201lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
202cases (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 //
207qed.
208
209lemma 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)
213lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
214cases (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 //
218qed.
219
220theorem 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
223whd in ⊢ (??(???%)%)
224lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
225cases (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
228cases (add_with_carries ????)
229#rs' #cs' #E destruct @refl
230qed.
231
232theorem 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
235whd in ⊢ (??(???%)%)
236lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
237cases (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
240cases (add_with_carries ????)
241#rs' #cs' #E destruct @refl
242qed.
Note: See TracBrowser for help on using the repository browser.