source: src/Clight/frontend_misc.ma @ 2896

Last change on this file since 2896 was 2822, checked in by garnier, 7 years ago

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File size: 109.8 KB
Line 
1(* Various small homeless results. *)
2
3include "Clight/TypeComparison.ma".
4include "Clight/Csem.ma".
5include "common/Pointers.ma".
6include "basics/jmeq.ma".
7include "basics/star.ma". (* well-founded relations *)
8include "common/IOMonad.ma".
9include "common/IO.ma".
10include "basics/lists/listb.ma".
11include "basics/lists/list.ma".
12
13
14(* --------------------------------------------------------------------------- *)
15(* [cthulhu] plays the same role as daemon. It should be droppable. *)
16(* --------------------------------------------------------------------------- *)
17
18axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)
19
20(* --------------------------------------------------------------------------- *)
21(* Misc. *)
22(* --------------------------------------------------------------------------- *)
23
24lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
25* normalize //
26qed.
27
28lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
29* normalize //
30qed.
31
32lemma type_eq_identity : ∀t. type_eq t t = true.
33#t normalize elim (type_eq_dec t t)
34[ 1: #Heq normalize //
35| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.
36
37lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
38#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
39[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
40| 2: #Hneq' normalize // ] qed.
41
42lemma typ_eq_dec : ∀t1,t2:typ. (t1=t2)⊎(t1≠t2).
43#t1 #t2
44cases t1 cases t2
45[ #sz #sg #sz' #sg' cases sz cases sz'
46  try //
47| #sz #sg %2 % #Habsurd destruct (Habsurd)
48| #sz #sg %2 % #Habsurd destruct (Habsurd)
49| %1 @refl ]
50qed.
51
52lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
53
54lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
55
56lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
57#A #B #a #b * #a' #b' #H destruct @refl
58qed.
59
60lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
61#A #B #a #b * #a' #b' #H destruct @refl
62qed.
63
64lemma bindIO_Error : ∀err,f. bindIO io_out io_in (val×trace) (trace×state) (Error … err) f = Wrong io_out io_in (trace×state) err.
65// qed.
66
67lemma bindIO_Value : ∀v,f. bindIO io_out io_in (val×trace) (trace×state) (Value … v) f = (f v).
68// qed.
69
70lemma bindIO_elim :
71         ∀A.
72         ∀P : (IO io_out io_in A) → Prop.
73         ∀e : res A. (*IO io_out io_in A.*)
74         ∀f.
75         (∀v. (e:IO io_out io_in A) = OK … v →  P (f v)) →
76         (∀err. (e:IO io_out io_in A) = Error … err →  P (Wrong ??? err)) →
77         P (bindIO io_out io_in ? A (e:IO io_out io_in A) f).
78#A #P * try /2/ qed.
79
80lemma opt_to_io_Value :
81  ∀A,B,C,err,x,res. opt_to_io A B C err x = return res → x = Some ? res.
82#A #B #C #err #x cases x normalize
83[ 1: #res #Habsurd destruct
84| 2: #c #res #Heq destruct @refl ]
85qed. 
86
87lemma some_inversion :
88  ∀A,B:Type[0].
89  ∀e:option A.
90  ∀res:B.
91  ∀f:A → option B.
92 match e with
93 [ None ⇒ None ?
94 | Some x ⇒ f x ] = Some ? res →
95 ∃x. e = Some ? x ∧ f x = Some ? res.
96 #A #B #e #res #f cases e normalize nodelta
97[ 1: #Habsurd destruct (Habsurd)
98| 2: #a #Heq %{a} @conj >Heq @refl ]
99qed.
100
101lemma res_inversion :
102  ∀A,B:Type[0].
103  ∀e:option A.
104  ∀errmsg.
105  ∀result:B.
106  ∀f:A → res B.
107 match e with
108 [ None ⇒ Error ? errmsg
109 | Some x ⇒ f x ] = OK ? result →
110 ∃x. e = Some ? x ∧ f x = OK ? result.
111 #A #B #e #errmsg #result #f cases e normalize nodelta
112[ 1: #Habsurd destruct (Habsurd)
113| 2: #a #Heq %{a} @conj >Heq @refl ]
114qed.
115
116lemma cons_inversion :
117  ∀A,B:Type[0].
118  ∀e:list A.
119  ∀res:B.
120  ∀f:A → list A → option B.
121 match e with
122 [ nil ⇒ None ?
123 | cons hd tl ⇒ f hd tl ] = Some ? res →
124 ∃hd,tl. e = hd::tl ∧ f hd tl = Some ? res.
125#A #B #e #res #f cases e normalize nodelta
126[ 1: #Habsurd destruct (Habsurd)
127| 2: #hd #tl #Heq %{hd} %{tl} @conj >Heq @refl ]
128qed.
129
130lemma if_opt_inversion :
131  ∀A:Type[0].
132  ∀x.
133  ∀y:A.
134  ∀e:bool.
135 (if e then
136    x
137  else
138    None ?) = Some ? y →
139 e = true ∧ x = Some ? y.
140#A #x #y * normalize
141#H destruct @conj @refl
142qed.
143
144lemma opt_to_res_inversion :
145  ∀A:Type[0]. ∀errmsg. ∀opt. ∀val. opt_to_res A errmsg opt = OK ? val →
146  opt = Some ? val.
147#A #errmsg *
148[ 1: #val normalize #Habsurd destruct
149| 2: #res #val normalize #Heq destruct @refl ]
150qed.
151
152lemma andb_inversion :
153  ∀a,b : bool. andb a b = true → a = true ∧ b = true.
154* * normalize /2 by conj, refl/ qed. 
155
156lemma identifier_eq_i_i : ∀tag,i. ∃pf. identifier_eq tag i i = inl … pf.
157#tag #i cases (identifier_eq ? i i)
158[ 1: #H %{H} @refl
159| 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ]
160qed.
161
162lemma intsize_eq_inversion :
163  ∀sz,sz'.
164  ∀A:Type[0].
165  ∀ok,not_ok.
166  intsize_eq_elim' sz sz' (λsz,sz'. res A)
167                          (OK ? ok)
168                          (Error ? not_ok) = (OK ? ok) →
169  sz = sz'.
170* * try // normalize
171#A #ok #not_ok #Habsurd destruct
172qed.
173
174lemma intsize_eq_elim_dec :
175  ∀sz1,sz2.
176  ∀P: ∀sz1,sz2. Type[0].
177  ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨
178  ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2).
179* * #P normalize
180try /3 by or_introl, conj, refl/
181%2 @conj try //
182% #H destruct
183qed.
184
185lemma typ_eq_elim :
186  ∀t1,t2.
187  ∀(P: (t1=t2)+(t1≠t2) → Prop).
188  (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
189#t1 #t2 #P #Hl #Hr
190@(match typ_eq t1 t2
191  with
192  [ inl H ⇒ Hl H
193  | inr H ⇒ Hr H ])
194qed.
195
196
197lemma eq_nat_dec_true : ∀n. eq_nat_dec n n = inl ?? (refl ? n).
198#n elim n try //
199#n' #Hind whd in ⊢ (??%?); >Hind @refl
200qed.
201
202lemma type_eq_dec_true : ∀ty. type_eq_dec ty ty = inl ?? (refl ? ty).
203#ty cases (type_eq_dec ty ty) #H
204destruct (H) try @refl @False_ind cases H #J @J @refl qed.
205
206lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
207*
208[ * * normalize @refl
209| @refl ]
210qed.
211
212lemma intsize_eq_elim_inversion :
213  ∀A:Type[0].
214  ∀sz1,sz2.
215  ∀elt1,f,errmsg,res. 
216  intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res →
217  ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
218#A * * #elt1 #f #errmsg #res normalize #H destruct (H)
219%{(refl ??)} normalize nodelta >H @refl
220qed.
221
222lemma inttyp_eq_elim_true' :
223  ∀sz,sg,P,p1,p2.
224  inttyp_eq_elim' sz sz sg sg P p1 p2 = p1.
225* * #P #p1 #p2 normalize try @refl
226qed.
227
228
229(* --------------------------------------------------------------------------- *)
230(* Useful facts on various boolean operations. *)
231(* --------------------------------------------------------------------------- *)
232 
233lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
234lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
235lemma andb_comm : ∀x,y. andb x y = andb y x. // qed.
236lemma notb_true : notb true = false. // qed.
237lemma notb_false : notb false = true. % #H destruct qed.
238lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
239
240(* --------------------------------------------------------------------------- *)
241(* Useful facts on Z. *)
242(* --------------------------------------------------------------------------- *)
243
244lemma Zltb_to_Zleb_true : ∀a,b. Zltb a b = true → Zleb a b = true.
245#a #b #Hltb lapply (Zltb_true_to_Zlt … Hltb) #Hlt @Zle_to_Zleb_true
246/3 by Zlt_to_Zle, transitive_Zle/ qed.
247
248lemma Zle_to_Zle_to_eq : ∀a,b. Zle a b → Zle b a → a = b.
249#a #b elim b
250[ 1: elim a // #a' normalize [ 1: @False_ind | 2: #_ @False_ind ] ]
251#b' elim a normalize
252[ 1: #_ @False_ind
253| 2: #a' #H1 #H2 >(le_to_le_to_eq … H1 H2) @refl
254| 3: #a' #_ @False_ind
255| 4: @False_ind
256| 5: #a' @False_ind
257| 6: #a' #H2 #H1 >(le_to_le_to_eq … H1 H2) @refl
258] qed.
259
260lemma Zleb_true_to_Zleb_true_to_eq : ∀a,b. (Zleb a b = true) → (Zleb b a = true) → a = b.
261#a #b #H1 #H2
262/3 by Zle_to_Zle_to_eq, Zleb_true_to_Zle/
263qed.
264
265lemma Zltb_dec : ∀a,b. (Zltb a b = true) ∨ (Zltb a b = false ∧ Zleb b a = true).
266#a #b
267lapply (Z_compare_to_Prop … a b)
268cases a
269[ 1: | 2,3: #a' ]
270cases b
271whd in match (Z_compare OZ OZ); normalize nodelta
272[ 2,3,5,6,8,9: #b' ]
273whd in match (Zleb ? ?);
274try /3 by or_introl, or_intror, conj, I, refl/
275whd in match (Zltb ??);
276whd in match (Zleb ??); #_
277[ 1: cases (decidable_le (succ a') b')
278     [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption
279     | 2:  #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2  @conj try @le_to_leb_true
280           /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ]
281| 2: cases (decidable_le (succ b') a')
282     [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption
283     | 2:  #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2  @conj try @le_to_leb_true
284           /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ]
285] qed.
286
287lemma Zleb_unsigned_OZ : ∀bv. Zleb OZ (Z_of_unsigned_bitvector 16 bv) = true.
288#bv elim bv try // #n' * #tl normalize /2/ qed.
289
290lemma Zltb_unsigned_OZ : ∀bv. Zltb (Z_of_unsigned_bitvector 16 bv) OZ = false.
291#bv elim bv try // #n' * #tl normalize /2/ qed.
292
293lemma Z_of_unsigned_not_neg : ∀bv.
294  (Z_of_unsigned_bitvector 16 bv = OZ) ∨ (∃p. Z_of_unsigned_bitvector 16 bv = pos p).
295#bv elim bv
296[ 1: normalize %1 @refl
297| 2: #n #hd #tl #Hind cases hd
298     [ 1: normalize %2 /2 by ex_intro/
299     | 2: cases Hind normalize [ 1: #H %1 @H | 2: * #p #H >H %2 %{p} @refl ]
300     ]
301] qed.
302
303lemma free_not_in_bounds : ∀x. if Zleb (pos one) x
304                                then Zltb x OZ 
305                                else false = false.
306#x lapply (Zltb_to_Zleb_true x OZ)
307elim (Zltb_dec … x OZ)
308[ 1: #Hlt >Hlt #H lapply (H (refl ??)) elim x
309     [ 2,3: #x' ] normalize in ⊢ (% → ?);
310     [ 1: #Habsurd destruct (Habsurd)
311     | 2,3: #_ @refl ]
312| 2: * #Hlt #Hle #_ >Hlt cases (Zleb (pos one) x) @refl ]
313qed.
314
315lemma free_not_valid : ∀x. if Zleb (pos one) x
316                            then Zltb x OZ 
317                            else false = false.
318#x
319cut (Zle (pos one) x ∧ Zlt x OZ → False)
320[ * #H1 #H2 lapply (transitive_Zle … (monotonic_Zle_Zsucc … H1) (Zlt_to_Zle … H2)) #H @H ] #Hguard
321cut (Zleb (pos one) x = true ∧ Zltb x OZ = true → False)
322[ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ @Zltb_true_to_Zlt assumption ]
323cases (Zleb (pos one) x) cases (Zltb x OZ)
324/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
325qed.
326
327(* follows from (0 ≤ a < b → mod a b = a) *)
328axiom Z_of_unsigned_bitvector_of_small_Z :
329  ∀z. OZ ≤ z → z < Z_two_power_nat 16 → Z_of_unsigned_bitvector 16 (bitvector_of_Z 16 z) = z.
330
331theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p.
332#n #m #p #Hle #Hlt /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle, transitive_Zle/
333qed.
334
335(* --------------------------------------------------------------------------- *)
336(* Useful facts on blocks. *)
337(* --------------------------------------------------------------------------- *)
338
339lemma eq_block_to_refl : ∀b1,b2. eq_block b1 b2 = true → b1 = b2.
340#b1 #b2 @(eq_block_elim … b1 b2)
341[ //
342| #_ #Habsurd destruct ] qed.
343
344lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
345#b1 #b2 #Hneq
346@(eq_block_elim … b1 b2)
347[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
348| 2: #_ @refl ] qed.
349
350lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false.
351#b1 #b2 #Hneq
352@(eq_block_elim … b1 b2)
353[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
354| 2: #_ @refl ] qed.
355
356definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_block ?.
357* (*#r1*) #id1 * (*#r2*) #id2 @(eqZb_elim … id1 id2)
358[ 1: #Heq >Heq (* cases r1 cases r2 * normalize *)
359     >eqZb_z_z normalize try // @conj #H destruct (H)
360     try @refl @eqZb_z_z
361| 2: #Hneq (* cases r1 cases r2 *) normalize
362     >(eqZb_false … Hneq) normalize @conj
363     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
364] qed.
365
366(* --------------------------------------------------------------------------- *)
367(* General results on lists. *)
368(* --------------------------------------------------------------------------- *)
369
370let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
371match l with
372[ nil ⇒ false
373| cons hd tl ⇒
374  let 〈id, ty〉 ≝ hd in
375  match identifier_eq SymbolTag i id with
376  [ inl Hid_eq ⇒ true
377  | inr Hid_neq ⇒ mem_assoc_env i tl 
378  ]
379].
380
381(* If mem succeeds in finding an element, then the list can be partitioned around this element. *)
382lemma list_mem_split : ∀A. ∀l : list A. ∀x : A. mem … x l → ∃l1,l2. l = l1 @ [x] @ l2.
383#A #l elim l
384[ 1: normalize #x @False_ind
385| 2: #hd #tl #Hind #x whd in ⊢ (% → ?); *
386     [ 1: #Heq %{(nil ?)} %{tl} destruct @refl
387     | 2: #Hmem lapply (Hind … Hmem) * #l1 * #l2 #Heq_tl >Heq_tl
388          %{(hd :: l1)} %{l2} @refl
389     ]
390] qed.
391
392lemma cons_to_append : ∀A. ∀hd : A. ∀l : list A. hd :: l = [hd] @ l. #A #hd #l @refl qed.
393
394lemma fold_append :
395  ∀A,B:Type[0]. ∀l1, l2 : list A. ∀f:A → B → B. ∀seed. foldr ?? f seed (l1 @ l2) = foldr ?? f (foldr ?? f seed l2) l1.
396#A #B #l1 elim l1 //
397#hd #tl #Hind #l2 #f #seed normalize >Hind @refl
398qed.
399
400lemma filter_append : ∀A:Type[0]. ∀l1,l2 : list A. ∀f. filter ? f (l1 @ l2) = (filter ? f l1) @ (filter ? f l2).
401#A #l1 elim l1 //
402#hd #tl #Hind #l2 #f
403>cons_to_append >associative_append
404normalize cases (f hd) normalize
405<Hind @refl
406qed.
407
408lemma filter_cons_unfold : ∀A:Type[0]. ∀f. ∀hd,tl.
409  filter ? f (hd :: tl) =
410  if f hd then
411    (hd :: filter A f tl)
412  else
413    (filter A f tl).
414#A #f #hd #tl elim tl // qed.
415
416
417lemma filter_elt_empty : ∀A:DeqSet. ∀elt,l. filter (carr A) (λx.¬(x==elt)) l = [ ] → All (carr A) (λx. x = elt) l.
418#A #elt #l elim l
419[ 1: //
420| 2: #hd #tl #Hind >filter_cons_unfold
421     lapply (eqb_true A hd elt)
422     cases (hd==elt) normalize nodelta
423     [ 2: #_ #Habsurd destruct
424     | 1: * #H1 #H2 #Heq lapply (Hind Heq) #Hall whd @conj //
425          @H1 @refl
426     ]
427] qed.
428
429lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed.
430
431alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
432
433lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2).
434#A #elt #l1 elim l1
435[ 1: #l2 normalize @conj [ 1: #H %2 @H | 2: * [ 1: @False_ind | 2: #H @H ] ]
436| 2: #hd #tl #Hind #l2 @conj
437     [ 1: whd in match (meml ???); *
438          [ 1: #Heq >Heq %1 normalize %1 @refl
439          | 2: #H1 lapply (Hind l2) * #HA #HB normalize
440               elim (HA H1)
441               [ 1: #H %1 %2 assumption | 2: #H %2 assumption ]
442          ]
443     | 2: normalize *
444          [ 1: * /2 by or_introl, or_intror/
445               #H %2 elim (Hind l2) #_ #H' @H' %1 @H
446          | 2: #H %2 elim (Hind l2) #_ #H' @H' %2 @H ]
447     ]
448] qed.
449
450lemma mem_append_forward : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) → (mem … elt l1) ∨ (mem … elt l2).
451#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #H' #_ @H' @H qed.
452
453lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) .
454#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed.
455
456(* "Observational" equivalence on list implies concrete equivalence. Useful to
457 * prove equality from some reasoning on indexings. Needs a particular induction
458 * principle. *)
459 
460let rec double_list_ind
461  (A : Type[0])
462  (P : list A → list A → Prop)
463  (base_nil  : P [ ] [ ])
464  (base_l1   : ∀hd1,l1. P (hd1::l1) [ ])
465  (base_l2   : ∀hd2,l2. P [ ] (hd2::l2))
466  (ind  : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2))
467  (l1, l2 : list A) on l1 ≝
468match l1 with
469[ nil ⇒
470  match l2 with
471  [ nil ⇒ base_nil
472  | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ]
473| cons hd1 tl1 ⇒ 
474  match l2 with
475  [ nil ⇒ base_l1 hd1 tl1
476  | cons hd2 tl2 ⇒
477    ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2)
478  ]
479]. 
480
481lemma nth_eq_tl :
482  ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2.
483  (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) →
484  (∀i. nth_opt A i l1 = nth_opt A i l2).
485#A #l1 #l2 @(double_list_ind … l1 l2)
486[ 1: #hd1 #hd2 #_ #i elim i try /2/
487| 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
488| 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
489| 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2
490     #Hind
491     @(λi. Hind (S i))
492] qed.     
493
494
495lemma nth_eq_to_eq :
496  ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2.
497#A #l1 elim l1
498[ 1: #l2 #H lapply (H 0) normalize
499     cases l2
500     [ 1: //
501     | 2: #hd2 #tl2 normalize #Habsurd destruct ]
502| 2: #hd1 #tl1 #Hind *
503     [ 1: #H lapply (H 0) normalize #Habsurd destruct
504     | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq)
505          >(Hind tl2) try @refl @(nth_eq_tl … H)
506     ]
507] qed.
508
509(* --------------------------------------------------------------------------- *)
510(* General results on vectors. *)
511(* --------------------------------------------------------------------------- *)
512
513(* copied from AssemblyProof, TODO get rid of the redundant stuff. *)
514lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
515 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
516 #n #hd #tl #abs @⊥ destruct (abs)
517qed.
518
519lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
520 ∃hd.∃tl.v ≃ VCons A n hd tl.
521 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
522 [ #abs @⊥ destruct (abs)
523 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
524qed.
525
526lemma vector_append_zero:
527  ∀A,m.
528  ∀v: Vector A m.
529  ∀q: Vector A 0.
530    v = q@@v.
531  #A #m #v #q
532  >(Vector_O A q) %
533qed.
534
535corollary prod_vector_zero_eq_left:
536  ∀A, n.
537  ∀q: Vector A O.
538  ∀r: Vector A n.
539    〈q, r〉 = 〈[[ ]], r〉.
540  #A #n #q #r
541  generalize in match (Vector_O A q …);
542  #hyp
543  >hyp in ⊢ (??%?);
544  %
545qed.
546 
547lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
548# A #m #n elim m
549[ 1: normalize #v
550  elim (Vector_Sn ?? v) #hd * #tl #Eq
551  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
552  >Eq normalize //
553| 2: #n' #Hind #v
554  elim (Vector_Sn ?? v) #hd * #tl #Eq
555  elim (Hind tl)
556  #tl1 * #tl2 #Eq_tl
557  @(ex_intro … (hd ::: tl1))
558  @(ex_intro … tl2) 
559  destruct normalize //
560] qed.
561
562lemma vsplit_zero:
563  ∀A,m.
564  ∀v: Vector A m.
565    〈[[]], v〉 = vsplit A 0 m v.
566  #A #m #v
567  elim v
568  [ %
569  | #n #hd #tl #ih
570    normalize in ⊢ (???%); %
571  ]
572qed.
573
574lemma vsplit_zero2:
575  ∀A,m.
576  ∀v: Vector A m.
577    〈[[]], v〉 = vsplit' A 0 m v.
578  #A #m #v
579  elim v
580  [ %
581  | #n #hd #tl #ih
582    normalize in ⊢ (???%); %
583  ]
584qed.
585
586lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
587# A #m #n elim m
588[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
589| 2: #n' #Hind #v
590  elim (Vector_Sn ?? v) #hd * #tl #Eq
591  elim (Hind tl)
592  #tl1 * #tl2 #Eq_tl
593  @(ex_intro … (hd ::: tl1))
594  @(ex_intro … tl2) 
595  destruct normalize //
596] qed.
597
598(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
599 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
600axiom vsplit_succ:
601  ∀A, m, n.
602  ∀l: Vector A m.
603  ∀r: Vector A n.
604  ∀v: Vector A (m + n).
605  ∀hd.
606    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
607
608axiom vsplit_succ2:
609  ∀A, m, n.
610  ∀l: Vector A m.
611  ∀r: Vector A n.
612  ∀v: Vector A (m + n).
613  ∀hd.
614    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
615     
616lemma vsplit_prod2:
617  ∀A,m,n.
618  ∀p: Vector A (m + n).
619  ∀v: Vector A m.
620  ∀q: Vector A n.
621    p = v@@q → 〈v, q〉 = vsplit' A m n p.
622  #A #m
623  elim m
624  [ #n #p #v #q #hyp
625    >hyp <(vector_append_zero A n q v)
626    >(prod_vector_zero_eq_left A …)
627    @vsplit_zero2
628  | #r #ih #n #p #v #q #hyp
629    >hyp
630    cases (Vector_Sn A r v)
631    #hd #exists
632    cases exists
633    #tl #jmeq >jmeq
634    @vsplit_succ2 [1: % |2: @ih % ]
635  ]
636qed.
637
638lemma vsplit_prod:
639  ∀A,m,n.
640  ∀p: Vector A (m + n).
641  ∀v: Vector A m.
642  ∀q: Vector A n.
643    p = v@@q → 〈v, q〉 = vsplit A m n p.
644  #A #m
645  elim m
646  [ #n #p #v #q #hyp
647    >hyp <(vector_append_zero A n q v)
648    >(prod_vector_zero_eq_left A …)
649    @vsplit_zero
650  | #r #ih #n #p #v #q #hyp
651    >hyp
652    cases (Vector_Sn A r v)
653    #hd #exists
654    cases exists
655    #tl #jmeq >jmeq
656    @vsplit_succ [1: % |2: @ih % ]
657  ]
658qed.
659
660(* --------------------------------------------------------------------------- *)
661(* Some more stuff on bitvectors. *)
662(* --------------------------------------------------------------------------- *)
663
664axiom commutative_multiplication :
665  ∀n. ∀v1,v2:BitVector n.
666  multiplication ? v1 v2 = multiplication ? v2 v1.
667
668lemma commutative_short_multiplication :
669  ∀n. ∀v1,v2:BitVector n.
670  short_multiplication ? v1 v2 = short_multiplication ? v2 v1.
671#n #v1 #v2 whd in ⊢ (??%%); >commutative_multiplication @refl
672qed.
673
674lemma sign_ext_same_size : ∀n,v. sign_ext n n v = v.
675#n #v whd in match (sign_ext ???); >nat_compare_eq @refl
676qed.
677
678lemma zero_ext_same_size : ∀n,v. zero_ext n n v = v.
679#n #v whd in match (zero_ext ???); >nat_compare_eq @refl
680qed.
681
682axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2.
683
684axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2.
685
686(* notice that we restrict source and target sizes to be ≠ 0 *)
687axiom zero_ext_one : ∀sz1,sz2. zero_ext (bitsize_of_intsize sz1) (bitsize_of_intsize sz2) (repr sz1 1) = (repr sz2 1).
688
689axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?).
690
691axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
692
693(* dividing zero by something eq zero, not the other way around ofc. *)
694axiom division_u_zero : ∀sz.∀v:BitVector ?. division_u sz (bv_zero ?) v = Some ? (bv_zero ?).
695
696
697(* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *)
698
699
700(* --------------------------------------------------------------------------- *)
701(* Generic properties of equivalence relations *)
702(* --------------------------------------------------------------------------- *)
703
704lemma triangle_diagram :
705  ∀acctype : Type[0].
706  ∀eqrel : acctype → acctype → Prop.
707  ∀refl_eqrel  : reflexive ? eqrel.
708  ∀trans_eqrel : transitive ? eqrel.
709  ∀sym_eqrel   : symmetric ? eqrel.
710  ∀a,b,c. eqrel a b → eqrel a c → eqrel b c.
711#acctype #eqrel #R #T #S #a #b #c
712#H1 #H2 @(T … (S … H1) H2)
713qed.
714
715lemma cotriangle_diagram :
716  ∀acctype : Type[0].
717  ∀eqrel : acctype → acctype → Prop.
718  ∀refl_eqrel  : reflexive ? eqrel.
719  ∀trans_eqrel : transitive ? eqrel.
720  ∀sym_eqrel   : symmetric ? eqrel.
721  ∀a,b,c. eqrel b a → eqrel c a → eqrel b c.
722#acctype #eqrel #R #T #S #a #b #c
723#H1 #H2 @S @(T … H2 (S … H1))
724qed.
725
726(* --------------------------------------------------------------------------- *)
727(* Quick and dirty implementation of finite sets relying on lists. The
728 * implementation is split in two: an abstract equivalence defined using inclusion
729 * of lists, and a concrete one where equivalence is defined as the closure of
730 * duplication, contraction and transposition of elements. We rely on the latter
731 * to prove stuff on folds over sets.  *)
732(* --------------------------------------------------------------------------- *)
733
734definition lset ≝ λA:Type[0]. list A.
735
736(* The empty set. *)
737definition empty_lset ≝ λA:Type[0]. nil A.
738
739(* Standard operations. *)
740definition lset_union ≝ λA:Type[0].λl1,l2 : lset A. l1 @ l2.
741
742definition lset_remove ≝ λA:DeqSet.λl:lset (carr A).λelt:carr A. (filter … (λx.¬x==elt) l).
743
744definition lset_difference ≝ λA:DeqSet.λl1,l2:lset (carr A). (filter … (λx.¬ (memb ? x l2)) l1).
745
746(* Standard predicates on sets *)
747definition lset_in ≝ λA:Type[0].λx : A. λl : lset A. mem … x l.
748
749definition lset_disjoint ≝ λA:Type[0].λl1, l2 : lset A.
750  ∀x,y. mem … x l1 → mem … y l2 → x ≠ y.
751 
752definition lset_inclusion ≝ λA:Type[0].λl1,l2.
753  All A (λx1. mem … x1 l2) l1.
754
755(* Definition of abstract set equivalence. *)
756definition lset_eq ≝ λA:Type[0].λl1,l2.
757  lset_inclusion A l1 l2 ∧
758  lset_inclusion A l2 l1.
759
760(* Properties of inclusion. *) 
761lemma reflexive_lset_inclusion : ∀A. ∀l. lset_inclusion A l l.
762#A #l elim l try //
763#hd #tl #Hind whd @conj
764[ 1: %1 @refl
765| 2: whd in Hind; @(All_mp … Hind)
766     #a #H whd %2 @H
767] qed.
768
769lemma transitive_lset_inclusion : ∀A. ∀l1,l2,l3. lset_inclusion A l1 l2 → lset_inclusion A l2 l3 → lset_inclusion A l1 l3 .
770#A #l1 #l2 #l3
771#Hincl1 #Hincl2 @(All_mp … Hincl1)
772whd in Hincl2;
773#a elim l2 in Hincl2;
774[ 1: normalize #_ @False_ind
775| 2: #hd #tl #Hind whd in ⊢ (% → ?);
776     * #Hmem #Hincl_tl whd in ⊢ (% → ?);
777     * [ 1: #Heq destruct @Hmem
778       | 2: #Hmem_tl @Hind assumption ]
779] qed.
780
781lemma cons_preserves_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A l1 (x::l2).
782#A #l1 #l2 #Hincl #x @(All_mp … Hincl) #a #Hmem whd %2 @Hmem qed.
783
784lemma cons_monotonic_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A (x::l1) (x::l2).
785#A #l1 #l2 #Hincl #x whd @conj
786[ 1: /2 by or_introl/
787| 2: @(All_mp … Hincl) #a #Hmem whd %2 @Hmem ] qed.
788
789lemma lset_inclusion_concat : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A l1 (l3 @ l2).
790#A #l1 #l2 #Hincl #l3 elim l3
791try /2 by cons_preserves_inclusion/
792qed.
793
794lemma lset_inclusion_concat_monotonic : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A (l3 @ l1) (l3 @ l2).
795#A #l1 #l2 #Hincl #l3 elim l3
796try @Hincl #hd #tl #Hind @cons_monotonic_inclusion @Hind
797qed.
798 
799(* lset_eq is an equivalence relation. *)
800lemma reflexive_lset_eq : ∀A. ∀l. lset_eq A l l. /2 by conj/ qed.
801
802lemma transitive_lset_eq : ∀A. ∀l1,l2,l3. lset_eq A l1 l2 → lset_eq A l2 l3 → lset_eq A l1 l3.
803#A #l1 #l2 #l3 * #Hincl1 #Hincl2 * #Hincl3 #Hincl4
804@conj @(transitive_lset_inclusion ??l2) assumption
805qed.
806
807lemma symmetric_lset_eq : ∀A. ∀l1,l2. lset_eq A l1 l2 → lset_eq A l2 l1.
808#A #l1 #l2 * #Hincl1 #Hincl2 @conj assumption
809qed.
810
811(* Properties of inclusion vs union and equality. *)
812lemma lset_union_inclusion : ∀A:Type[0]. ∀a,b,c. 
813  lset_inclusion A a c → lset_inclusion ? b c → lset_inclusion ? (lset_union ? a b) c.
814#A #a #b #c #H1 #H2 whd whd in match (lset_union ???);
815@All_append assumption qed.
816
817lemma lset_inclusion_union : ∀A:Type[0]. ∀a,b,c. 
818  lset_inclusion A a b ∨ lset_inclusion A a c → lset_inclusion ? a (lset_union ? b c).
819#A #a #b #c *
820[ 1: @All_mp #elt #Hmem @mem_append_backwards %1 @Hmem
821| 2: @All_mp #elt #Hmem @mem_append_backwards %2 @Hmem
822] qed.
823
824lemma lset_inclusion_eq : ∀A : Type[0]. ∀a,b,c : lset A.
825  lset_eq ? a b → lset_inclusion ? b c → lset_inclusion ? a c.
826#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H1 H3)
827qed.
828
829lemma lset_inclusion_eq2 : ∀A : Type[0]. ∀a,b,c : lset A.
830  lset_eq ? b c → lset_inclusion ? a b → lset_inclusion ? a c.
831#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H3 H1)
832qed.
833
834(* Properties of lset_eq and mem *)
835lemma lset_eq_mem :
836  ∀A:Type[0].
837  ∀s1,s2 : lset A.
838  lset_eq ? s1 s2 →
839  ∀b.mem ? b s1 → mem ? b s2.
840#A #s1 #s2 * #Hincl12 #_ #b
841whd in Hincl12; elim s1 in Hincl12;
842[ 1: normalize #_ *
843| 2: #hd #tl #Hind whd in ⊢ (% → % → ?); * #Hmem' #Hall * #Heq
844     [ 1: destruct (Heq) assumption
845     | 2: @Hind assumption ]
846] qed.
847
848lemma lset_eq_memb :
849  ∀A : DeqSet.
850  ∀s1,s2 : lset (carr A).
851  lset_eq ? s1 s2 →
852  ∀b.memb ? b s1 = true → memb ? b s2 = true.
853#A #s1 #s2 #Heq #b
854lapply (memb_to_mem A s1 b) #H1 #H2
855lapply (H1 H2) #Hmem lapply (lset_eq_mem … Heq ? Hmem) @mem_to_memb
856qed.
857
858lemma lset_eq_memb_eq :
859  ∀A : DeqSet.
860  ∀s1,s2 : lset (carr A).
861  lset_eq ? s1 s2 →
862  ∀b.memb ? b s1 = memb ? b s2.
863#A #s1 #s2 #Hlset_eq #b
864lapply (lset_eq_memb … Hlset_eq b)
865lapply (lset_eq_memb … (symmetric_lset_eq … Hlset_eq) b) 
866cases (b∈s1)
867[ 1: #_ #H lapply (H (refl ??)) #Hmem >H @refl
868| 2: cases (b∈s2) // #H lapply (H (refl ??)) #Habsurd destruct
869] qed.
870
871lemma lset_eq_filter_eq :
872  ∀A : DeqSet.
873  ∀s1,s2 : lset (carr A).
874  lset_eq ? s1 s2 → 
875  ∀l.
876     (filter ? (λwb.¬wb∈s1) l) =
877     (filter ? (λwb.¬wb∈s2) l).
878#A #s1 #s2 #Heq #l elim l
879[ 1: @refl
880| 2: #hd #tl #Hind >filter_cons_unfold >filter_cons_unfold
881      >(lset_eq_memb_eq … Heq) cases (hd∈s2)
882      normalize in match (notb ?); normalize nodelta
883      try @Hind >Hind @refl
884] qed.
885
886lemma cons_monotonic_eq : ∀A. ∀l1,l2 : lset A. lset_eq A l1 l2 → ∀x. lset_eq A (x::l1) (x::l2).
887#A #l1 #l2 #Heq #x cases Heq #Hincl1 #Hincl2
888@conj
889[ 1: @cons_monotonic_inclusion
890| 2: @cons_monotonic_inclusion ]
891assumption
892qed.
893
894(* Properties of difference and remove *)
895lemma lset_difference_unfold :
896  ∀A : DeqSet.
897  ∀s1, s2 : lset (carr A).
898  ∀hd. lset_difference A (hd :: s1) s2 =
899    if hd∈s2 then
900      lset_difference A s1 s2
901    else
902      hd :: (lset_difference A s1 s2).
903#A #s1 #s2 #hd normalize
904cases (hd∈s2) @refl
905qed.
906
907lemma lset_difference_unfold2 :
908  ∀A : DeqSet.
909  ∀s1, s2 : lset (carr A).
910  ∀hd. lset_difference A s1 (hd :: s2) =
911       lset_difference A (lset_remove ? s1 hd) s2.
912#A #s1
913elim s1
914[ 1: //
915| 2: #hd1 #tl1 #Hind #s2 #hd
916     whd in match (lset_remove ???);
917     whd in match (lset_difference A ??);
918     whd in match (memb ???);
919     lapply (eqb_true … hd1 hd)
920     cases (hd1==hd) normalize nodelta
921     [ 1: * #H #_ lapply (H (refl ??)) -H #H
922           @Hind
923     | 2: * #_ #Hguard >lset_difference_unfold
924          cases (hd1∈s2) normalize in match (notb ?); normalize nodelta
925          <Hind @refl ]
926] qed.         
927
928lemma lset_difference_disjoint :
929 ∀A : DeqSet.
930 ∀s1,s2 : lset (carr A).
931  lset_disjoint A s1 (lset_difference A s2 s1).
932#A #s1 elim s1
933[ 1: #s2 normalize #x #y *
934| 2: #hd1 #tl1 #Hind #s2 >lset_difference_unfold2 #x #y
935     whd in ⊢ (% → ?); *
936     [ 2: @Hind
937     | 1: #Heq >Heq elim s2
938          [ 1: normalize *
939          | 2: #hd2 #tl2 #Hind2 whd in match (lset_remove ???);
940               lapply (eqb_true … hd2 hd1)
941               cases (hd2 == hd1) normalize in match (notb ?); normalize nodelta * #H1 #H2
942               [ 1: @Hind2
943               | 2: >lset_difference_unfold cases (hd2 ∈ tl1) normalize nodelta try @Hind2
944                     whd in ⊢ (% → ?); *
945                     [ 1: #Hyhd2 destruct % #Heq lapply (H2 … (sym_eq … Heq)) #Habsurd destruct
946                     | 2: @Hind2 ]
947               ]
948          ]
949    ]
950] qed.
951
952
953lemma lset_remove_split : ∀A : DeqSet. ∀l1,l2 : lset A. ∀elt. lset_remove A (l1 @ l2) elt = (lset_remove … l1 elt) @ (lset_remove … l2 elt).
954#A #l1 #l2 #elt /2 by filter_append/ qed.
955
956lemma lset_inclusion_remove :
957  ∀A : DeqSet.
958  ∀s1, s2 : lset A.
959  lset_inclusion ? s1 s2 →
960  ∀elt. lset_inclusion ? (lset_remove ? s1 elt) (lset_remove ? s2 elt).
961#A #s1 elim s1
962[ 1: normalize //
963| 2: #hd1 #tl1 #Hind1 #s2 * #Hmem #Hincl
964     elim (list_mem_split ??? Hmem) #s2A * #s2B #Hs2_eq destruct #elt
965     whd in match (lset_remove ???);
966     @(match (hd1 == elt)
967       return λx. (hd1 == elt = x) → ?
968       with
969       [ true ⇒ λH. ?
970       | false ⇒ λH. ? ] (refl ? (hd1 == elt))) normalize in match (notb ?);
971     normalize nodelta
972     [ 1:  @Hind1 @Hincl
973     | 2: whd @conj
974          [ 2: @(Hind1 … Hincl)
975          | 1: >lset_remove_split >lset_remove_split
976               normalize in match (lset_remove A [hd1] elt);
977               >H normalize nodelta @mem_append_backwards %2
978               @mem_append_backwards %1 normalize %1 @refl ]
979     ]
980] qed.
981
982lemma lset_difference_lset_eq :
983  ∀A : DeqSet. ∀a,b,c.
984   lset_eq A b c →
985   lset_eq A (lset_difference A a b) (lset_difference A a c).
986#A #a #b #c #Heq
987whd in match (lset_difference ???) in ⊢ (??%%);   
988elim a
989[ 1: normalize @conj @I
990| 2: #hda #tla #Hind whd in match (foldr ?????) in ⊢ (??%%);
991     >(lset_eq_memb_eq … Heq hda) cases (hda∈c)
992     normalize in match (notb ?); normalize nodelta
993     try @Hind @cons_monotonic_eq @Hind
994] qed.
995
996lemma lset_difference_lset_remove_commute :
997  ∀A:DeqSet.
998  ∀elt,s1,s2.
999  (lset_difference A (lset_remove ? s1 elt) s2) =
1000  (lset_remove A (lset_difference ? s1 s2) elt).
1001#A #elt #s1 #s2
1002elim s1 try //
1003#hd #tl #Hind
1004>lset_difference_unfold
1005whd in match (lset_remove ???);
1006@(match (hd==elt) return λx. (hd==elt) = x → ?
1007  with
1008  [ true ⇒ λHhd. ?
1009  | false ⇒ λHhd. ?
1010  ] (refl ? (hd==elt)))
1011@(match (hd∈s2) return λx. (hd∈s2) = x → ?
1012  with
1013  [ true ⇒ λHmem. ?
1014  | false ⇒ λHmem. ?
1015  ] (refl ? (hd∈s2)))
1016>notb_true >notb_false normalize nodelta try //
1017try @Hind
1018[ 1:  whd in match (lset_remove ???) in ⊢ (???%); >Hhd
1019     elim (eqb_true ? elt elt) #_ #H >(H (refl ??))
1020     normalize in match (notb ?); normalize nodelta @Hind
1021| 2: >lset_difference_unfold >Hmem @Hind
1022| 3: whd in match (lset_remove ???) in ⊢ (???%);
1023     >lset_difference_unfold >Hhd >Hmem
1024     normalize in match (notb ?);
1025     normalize nodelta >Hind @refl
1026] qed.
1027
1028(* Inversion lemma on emptyness *)
1029lemma lset_eq_empty_inv : ∀A. ∀l. lset_eq A l [ ] → l = [ ].
1030#A #l elim l //
1031#hd' #tl' normalize #Hind * * @False_ind
1032qed.
1033
1034(* Inversion lemma on singletons *)
1035lemma lset_eq_singleton_inv : ∀A,hd,l. lset_eq A [hd] (hd::l) → All ? (λx.x=hd) l.
1036#A #hd #l
1037* #Hincl1 whd in ⊢ (% → ?); * #_ @All_mp
1038normalize #a * [ 1: #H @H | 2: @False_ind ]
1039qed.
1040
1041(* Permutation of two elements on top of the list is ok. *)
1042lemma lset_eq_permute : ∀A,l,x1,x2. lset_eq A (x1 :: x2 :: l) (x2 :: x1 :: l).
1043#A #l #x1 #x2 @conj normalize
1044[ 1: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
1045| 2: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
1046] qed.
1047
1048(* "contraction" of an element. *)
1049lemma lset_eq_contract : ∀A,l,x. lset_eq A (x :: x :: l) (x :: l).
1050#A #l #x @conj
1051[ 1: /5 by or_introl, conj, transitive_lset_inclusion/
1052| 2: /5 by cons_preserves_inclusion, cons_monotonic_inclusion/ ]
1053qed.
1054
1055(* We don't need more than one instance of each element. *)
1056lemma lset_eq_filter : ∀A:DeqSet.∀tl.∀hd.
1057  lset_eq A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
1058#A #tl elim tl
1059[ 1: #hd normalize /4 by or_introl, conj, I/
1060| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
1061     lapply (eqb_true A hd' hd) cases (hd'==hd)
1062     [ 2: #_ normalize in match (notb ?); normalize nodelta
1063          lapply (cons_monotonic_eq … (Hind hd) hd') #H
1064          lapply (lset_eq_permute ? tl' hd' hd) #H'
1065          @(transitive_lset_eq ? ? (hd'::hd::tl') ? … H')
1066          @(transitive_lset_eq ? ?? (hd'::hd::tl') … H)
1067          @lset_eq_permute
1068     | 1: * #Heq #_ >(Heq (refl ??)) normalize in match (notb ?); normalize nodelta
1069          lapply (Hind hd) #H
1070          @(transitive_lset_eq ? ? (hd::tl') (hd::hd::tl') H)
1071          @conj
1072          [ 1: whd @conj /2 by or_introl/ @cons_preserves_inclusion @cons_preserves_inclusion
1073               @reflexive_lset_inclusion
1074          | 2: whd @conj /2 by or_introl/ ]
1075     ]
1076] qed.
1077
1078lemma lset_inclusion_filter_self :
1079  ∀A:DeqSet.∀l,pred.
1080    lset_inclusion A (filter ? pred l) l.
1081#A #l #pred elim l
1082[ 1: normalize @I
1083| 2: #hd #tl #Hind whd in match (filter ???);
1084     cases (pred hd) normalize nodelta
1085     [ 1: @cons_monotonic_inclusion @Hind
1086     | 2: @cons_preserves_inclusion @Hind ]
1087] qed.   
1088
1089lemma lset_inclusion_filter_monotonic :
1090  ∀A:DeqSet.∀l1,l2. lset_inclusion (carr A) l1 l2 →
1091  ∀elt. lset_inclusion A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
1092#A #l1 elim l1
1093[ 1: #l2 normalize //
1094| 2: #hd1 #tl1 #Hind #l2 whd in ⊢ (% → ?); * #Hmem1 #Htl1_incl #elt
1095     whd >filter_cons_unfold
1096     lapply (eqb_true A hd1 elt) cases (hd1==elt)
1097     [ 1: * #H1 #_ lapply (H1 (refl ??)) #H1_eq >H1_eq in Hmem1; #Hmem
1098          normalize in match (notb ?); normalize nodelta @Hind assumption
1099     | 2: * #_ #Hneq normalize in match (notb ?); normalize nodelta
1100          whd @conj
1101          [ 1: elim l2 in Hmem1; try //
1102               #hd2 #tl2 #Hincl whd in ⊢ (% → ?); *
1103               [ 1: #Heq >Heq in Hneq; normalize
1104                    lapply (eqb_true A hd2 elt) cases (hd2==elt)
1105                    [ 1: * #H #_ #H2 lapply (H2 (H (refl ??))) #Habsurd destruct (Habsurd)
1106                    | 2: #_ normalize nodelta #_ /2 by or_introl/ ]
1107               | 2: #H lapply (Hincl H) #Hok
1108                    normalize cases (hd2==elt) normalize nodelta
1109                    [ 1: @Hok
1110                    | 2: %2 @Hok ] ]
1111          | 2: @Hind assumption ] ] ]
1112qed.
1113
1114(* removing an element of two equivalent sets conserves equivalence. *)
1115lemma lset_eq_filter_monotonic :
1116  ∀A:DeqSet.∀l1,l2. lset_eq (carr A) l1 l2 →
1117  ∀elt. lset_eq A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
1118#A #l1 #l2 * #Hincl1 #Hincl2 #elt @conj
1119/2 by lset_inclusion_filter_monotonic/
1120qed.
1121
1122(* ---------------- Concrete implementation of sets --------------------- *)
1123
1124(* We can give an explicit characterization of equivalent sets: they are permutations with repetitions, i,e.
1125   a composition of transpositions and duplications. We restrict ourselves to DeqSets. *)
1126inductive iso_step_lset (A : DeqSet) : lset A → lset A → Prop ≝
1127| lset_transpose : ∀a,x,b,y,c. iso_step_lset A (a @ [x] @ b @ [y] @ c) (a @ [y] @ b @ [x] @ c)
1128| lset_weaken : ∀a,x,b. iso_step_lset A (a @ [x] @ b) (a @ [x] @ [x] @ b)
1129| lset_contract : ∀a,x,b. iso_step_lset A (a @ [x] @ [x] @ b) (a @ [x] @ b).
1130
1131(* The equivalence is the reflexive, transitive and symmetric closure of iso_step_lset *)
1132inductive lset_eq_concrete (A : DeqSet) : lset A → lset A → Prop ≝
1133| lset_trans : ∀a,b,c. iso_step_lset A a b → lset_eq_concrete A b c → lset_eq_concrete A a c
1134| lset_refl  : ∀a. lset_eq_concrete A a a.
1135
1136(* lset_eq_concrete is symmetric and transitive *)
1137lemma transitive_lset_eq_concrete : ∀A,l1,l2,l3. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l3 → lset_eq_concrete A l1 l3.
1138#A #l1 #l2 #l3 #Hequiv
1139elim Hequiv //
1140#a #b #c #Hstep #Hequiv #Hind #Hcl3 lapply (Hind Hcl3) #Hbl3
1141@(lset_trans ???? Hstep Hbl3)
1142qed.
1143
1144lemma symmetric_step : ∀A,l1,l2. iso_step_lset A l1 l2 → iso_step_lset A l2 l1.
1145#A #l1 #l2 * /2/ qed.
1146
1147lemma symmetric_lset_eq_concrete : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l1.
1148#A #l1 #l2 #H elim H //
1149#a #b #c #Hab #Hbc #Hcb
1150@(transitive_lset_eq_concrete ???? Hcb ?)
1151@(lset_trans … (symmetric_step ??? Hab) (lset_refl …))
1152qed.
1153 
1154(* lset_eq_concrete is conserved by cons. *)
1155lemma equivalent_step_cons : ∀A,l1,l2. iso_step_lset A l1 l2 → ∀x. iso_step_lset A (x :: l1) (x :: l2).
1156#A #l1 #l2 * // qed. (* That // was impressive. *)
1157
1158lemma lset_eq_concrete_cons : ∀A,l1,l2. lset_eq_concrete A l1 l2 → ∀x. lset_eq_concrete A (x :: l1) (x :: l2).
1159#A #l1 #l2 #Hequiv elim Hequiv try //
1160#a #b #c #Hab #Hbc #Hind #x %1{(equivalent_step_cons ??? Hab x) (Hind x)}
1161qed.
1162
1163lemma absurd_list_eq_append : ∀A.∀x.∀l1,l2:list A. [ ] = l1 @ [x] @ l2 → False.
1164#A #x #l1 #l2 elim l1 normalize
1165[ 1: #Habsurd destruct
1166| 2: #hd #tl #_ #Habsurd destruct
1167] qed.
1168
1169(* Inversion lemma for emptyness, step case *)
1170lemma equivalent_iso_step_empty_inv : ∀A,l. iso_step_lset A l [] → l = [ ].
1171#A #l elim l //
1172#hd #tl #Hind #H inversion H
1173[ 1: #a #x #b #y #c #_ #Habsurd
1174      @(False_ind … (absurd_list_eq_append ? y … Habsurd))
1175| 2: #a #x #b #_ #Habsurd
1176      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
1177| 3: #a #x #b #_ #Habsurd
1178      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
1179] qed.
1180
1181(* Same thing for non-emptyness *)
1182lemma equivalent_iso_step_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → iso_step_lset A l1 l2 → l2 ≠ [ ].
1183#A #l1 elim l1
1184[ 1: #l2 * #H @(False_ind … (H (refl ??)))
1185| 2: #hd #tl #H #l2 #_ #Hstep % #Hl2 >Hl2 in Hstep; #Hstep
1186     lapply (equivalent_iso_step_empty_inv … Hstep) #Habsurd destruct
1187] qed.
1188
1189lemma lset_eq_concrete_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → lset_eq_concrete A l1 l2 → l2 ≠ [ ].
1190#A #l1 #l2 #Hl1 #H lapply Hl1 elim H
1191[ 2: #a #H @H
1192| 1: #a #b #c #Hab #Hbc #H #Ha lapply (equivalent_iso_step_cons_inv … Ha Hab) #Hb @H @Hb
1193] qed.
1194
1195lemma lset_eq_concrete_empty_inv : ∀A,l1,l2. l1 = [ ] → lset_eq_concrete A l1 l2 → l2 = [ ].
1196#A #l1 #l2 #Hl1 #H lapply Hl1 elim H //
1197#a #b #c #Hab #Hbc #Hbc_eq #Ha >Ha in Hab; #H_b lapply (equivalent_iso_step_empty_inv … ?? (symmetric_step … H_b))
1198#Hb @Hbc_eq @Hb
1199qed.
1200
1201(* Square equivalence diagram *)
1202lemma square_lset_eq_concrete :
1203  ∀A. ∀a,b,a',b'. lset_eq_concrete A a b → lset_eq_concrete A a a' → lset_eq_concrete A b b' → lset_eq_concrete A a' b'.
1204#A #a #b #a' #b' #H1 #H2 #H3
1205@(transitive_lset_eq_concrete ???? (symmetric_lset_eq_concrete … H2))
1206@(transitive_lset_eq_concrete ???? H1)
1207@H3
1208qed.
1209
1210(* Make the transposition of elements visible at top-level *)
1211lemma transpose_lset_eq_concrete :
1212  ∀A. ∀x,y,a,b,c,a',b',c'.
1213  lset_eq_concrete A (a @ [x] @ b @ [y] @ c) (a' @ [x] @ b' @ [y] @ c') →
1214  lset_eq_concrete A (a @ [y] @ b @ [x] @ c) (a' @ [y] @ b' @ [x] @ c').
1215#A #x #y #a #b #c #a' #b' #c
1216#H @(square_lset_eq_concrete ????? H) /2 by lset_trans, lset_refl, lset_transpose/
1217qed.
1218
1219lemma switch_lset_eq_concrete :
1220  ∀A. ∀a,b,c. lset_eq_concrete A (a@[b]@c) ([b]@a@c).
1221#A #a elim a //
1222#hda #tla #Hind #b #c lapply (Hind hda c) #H
1223lapply (lset_eq_concrete_cons … H b)
1224#H' normalize in H' ⊢ %; @symmetric_lset_eq_concrete
1225/3 by lset_transpose, lset_trans, symmetric_lset_eq_concrete/
1226qed.
1227
1228(* Folding a commutative and idempotent function on equivalent sets yields the same result. *)
1229lemma lset_eq_concrete_fold :
1230  ∀A : DeqSet.
1231  ∀acctype : Type[0].
1232  ∀l1,l2 : list (carr A).
1233  lset_eq_concrete A l1 l2 →
1234  ∀f:carr A → acctype → acctype.
1235  (∀x1,x2. ∀acc. f x1 (f x2 acc) = f x2 (f x1 acc)) →
1236  (∀x.∀acc. f x (f x acc) = f x acc) →
1237  ∀acc. foldr ?? f acc l1 = foldr ?? f acc l2.
1238#A #acctype #l1 #l2 #Heq #f #Hcomm #Hidem
1239elim Heq
1240try //
1241#a' #b' #c' #Hstep #Hbc #H #acc <H -H
1242elim Hstep
1243[ 1: #a #x #b #y #c
1244     >fold_append >fold_append >fold_append >fold_append
1245     >fold_append >fold_append >fold_append >fold_append
1246     normalize
1247     cut (f x (foldr A acctype f (f y (foldr A acctype f acc c)) b) =
1248          f y (foldr A acctype f (f x (foldr A acctype f acc c)) b)) [   
1249     elim c
1250     [ 1: normalize elim b
1251          [ 1: normalize >(Hcomm x y) @refl
1252          | 2: #hdb #tlb #Hind normalize
1253               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ]
1254     | 2: #hdc #tlc #Hind normalize elim b
1255          [ 1: normalize >(Hcomm x y) @refl
1256          | 2: #hdb #tlb #Hind normalize
1257               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] ]
1258     ]
1259     #Hind >Hind @refl
1260| 2: #a #x #b
1261     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
1262     normalize >Hidem @refl
1263| 3: #a #x #b
1264     >fold_append  >(fold_append ?? ([x]@[x])) >fold_append >fold_append
1265     normalize >Hidem @refl
1266] qed.
1267
1268(* Folding over equivalent sets yields equivalent results, for any equivalence. *)
1269lemma inj_to_fold_inj :
1270  ∀A,acctype : Type[0].
1271  ∀eqrel : acctype → acctype → Prop.
1272  ∀refl_eqrel  : reflexive ? eqrel.
1273  ∀trans_eqrel : transitive ? eqrel.
1274  ∀sym_eqrel   : symmetric ? eqrel.
1275  ∀f           : A → acctype → acctype.
1276  (∀x:A.∀acc1:acctype.∀acc2:acctype.eqrel acc1 acc2→eqrel (f x acc1) (f x acc2)) →
1277  ∀l : list A. ∀acc1, acc2 : acctype. eqrel acc1 acc2 → eqrel (foldr … f acc1 l) (foldr … f acc2 l).
1278#A #acctype #eqrel #R #T #S #f #Hinj #l elim l
1279//
1280#hd #tl #Hind #acc1 #acc2 #Heq normalize @Hinj @Hind @Heq
1281qed.
1282
1283(* We need to extend the above proof to arbitrary equivalence relation instead of
1284   just standard equality. *)
1285lemma lset_eq_concrete_fold_ext :
1286  ∀A : DeqSet.
1287  ∀acctype : Type[0].
1288  ∀eqrel : acctype → acctype → Prop.
1289  ∀refl_eqrel  : reflexive ? eqrel.
1290  ∀trans_eqrel : transitive ? eqrel.
1291  ∀sym_eqrel   : symmetric ? eqrel.
1292  ∀f:carr A → acctype → acctype.
1293  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1294  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1295  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1296  ∀l1,l2 : list (carr A).
1297  lset_eq_concrete A l1 l2 → 
1298  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1299#A #acctype #eqrel #R #T #S #f #Hinj #Hcomm #Hidem #l1 #l2 #Heq
1300elim Heq
1301try //
1302#a' #b' #c' #Hstep #Hbc #H inversion Hstep
1303[ 1: #a #x #b #y #c #HlA #HlB #_ #acc
1304     >HlB in H; #H @(T … ? (H acc))
1305     >fold_append >fold_append >fold_append >fold_append
1306     >fold_append >fold_append >fold_append >fold_append
1307     normalize
1308     cut (eqrel (f x (foldr ? acctype f (f y (foldr ? acctype f acc c)) b))
1309                (f y (foldr ? acctype f (f x (foldr ? acctype f acc c)) b)))
1310     [ 1:
1311     elim c
1312     [ 1: normalize elim b
1313          [ 1: normalize @(Hcomm x y)
1314          | 2: #hdb #tlb #Hind normalize
1315               lapply (Hinj hdb ?? Hind) #Hind'
1316               lapply (T … Hind' (Hcomm ???)) #Hind''
1317               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
1318     | 2: #hdc #tlc #Hind normalize elim b
1319          [ 1: normalize @(Hcomm x y)
1320          | 2: #hdb #tlb #Hind normalize
1321               lapply (Hinj hdb ?? Hind) #Hind'
1322               lapply (T … Hind' (Hcomm ???)) #Hind''
1323               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
1324     ] ]
1325     #Hind @(inj_to_fold_inj … eqrel R T S ? Hinj … Hind)
1326| 2: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
1327     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
1328     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @S @Hidem
1329| 3: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
1330     >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append
1331     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @Hidem
1332] qed.
1333
1334(* Prepare some well-founded induction principles on lists. The idea is to perform
1335   an induction on the sequence of filterees of a list : taking the first element,
1336   filtering it out of the tail, etc. We give such principles for pairs of lists
1337   and isolated lists.  *)
1338
1339(* The two lists [l1,l2] share at least the head of l1. *)
1340definition head_shared ≝ λA. λl1,l2 : list A.
1341match l1 with
1342[ nil ⇒ l2 = (nil ?)
1343| cons hd _ ⇒  mem … hd l2
1344].
1345
1346(* Relation on pairs of lists, as described above. *)
1347definition filtered_lists : ∀A:DeqSet. relation (list (carr A)×(list (carr A))) ≝
1348λA:DeqSet. λll1,ll2.
1349let 〈la1,lb1〉 ≝ ll1 in
1350let 〈la2,lb2〉 ≝ ll2 in
1351match la2 with
1352[ nil ⇒ False
1353| cons hda2 tla2 ⇒
1354    head_shared ? la2 lb2 ∧
1355    la1 = filter … (λx.¬(x==hda2)) tla2 ∧
1356    lb1 = filter … (λx.¬(x==hda2)) lb2
1357].
1358
1359(* Notice the absence of plural : this relation works on a simple list, not a pair. *)
1360definition filtered_list : ∀A:DeqSet. relation (list (carr A)) ≝
1361λA:DeqSet. λl1,l2.
1362match l2 with
1363[ nil ⇒ False
1364| cons hd2 tl2 ⇒
1365    l1 = filter … (λx.¬(x==hd2)) l2
1366].
1367
1368(* Relation on lists based on their lengths. We know this one is well-founded. *)
1369definition length_lt : ∀A:DeqSet. relation (list (carr A)) ≝
1370λA:DeqSet. λl1,l2. lt (length ? l1) (length ? l2).
1371
1372(* length_lt can be extended on pairs by just measuring the first component *)
1373definition length_fst_lt : ∀A:DeqSet. relation (list (carr A) × (list (carr A))) ≝
1374λA:DeqSet. λll1,ll2. lt (length ? (\fst ll1)) (length ? (\fst ll2)).
1375
1376lemma filter_length : ∀A. ∀l. ∀f. |filter A f l| ≤ |l|.
1377#A #l #f elim l //
1378#hd #tl #Hind whd in match (filter ???); cases (f hd) normalize nodelta
1379[ 1: /2 by le_S_S/
1380| 2: @le_S @Hind
1381] qed.
1382
1383(* The order on lists defined by their length is wf *)
1384lemma length_lt_wf : ∀A. ∀l. WF (list (carr A)) (length_lt A) l.
1385#A #l % elim l
1386[ 1: #a normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1387| 2: #hd #tl #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1388@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1389qed.
1390
1391(* Order on pairs of list by measuring the first proj *)
1392lemma length_fst_lt_wf : ∀A. ∀ll. WF ? (length_fst_lt A) ll.
1393#A * #l1 #l2 % elim l1
1394[ 1: * #a1 #a2 normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1395| 2: #hd1 #tl1 #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1396@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1397qed.
1398
1399lemma length_to_filtered_lists : ∀A. subR ? (filtered_lists A) (length_fst_lt A).
1400#A whd * #a1 #a2 * #b1 #b2 elim b1
1401[ 1: @False_ind
1402| 2: #hd1 #tl1 #Hind whd in ⊢ (% → ?); * * #Hmem #Ha1 #Ha2 whd
1403     >Ha1 whd in match (length ??) in ⊢ (??%); @le_S_S @filter_length
1404] qed.
1405
1406lemma length_to_filtered_list : ∀A. subR ? (filtered_list A) (length_lt A).
1407#A whd #a #b elim b
1408[ 1: @False_ind
1409| 2: #hd #tl #Hind whd in ⊢ (% → ?); whd in match (filter ???);
1410     lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?);
1411     normalize nodelta #Ha whd @le_S_S >Ha @filter_length ]
1412qed.
1413
1414(* Prove well-foundedness by embedding in lt *)
1415lemma filtered_lists_wf : ∀A. ∀ll. WF ? (filtered_lists A) ll.
1416#A #ll @(WF_antimonotonic … (length_to_filtered_lists A)) @length_fst_lt_wf
1417qed.
1418
1419lemma filtered_list_wf : ∀A. ∀l. WF ? (filtered_list A) l.
1420#A #l @(WF_antimonotonic … (length_to_filtered_list A)) @length_lt_wf
1421qed.
1422
1423definition Acc_elim : ∀A,R,x. WF A R x → (∀a. R a x → WF A R a) ≝
1424λA,R,x,acc.
1425match acc with
1426[ wf _ a0 ⇒ a0 ].
1427
1428(* Stolen from Coq. Warped to avoid prop-to-type restriction. *)
1429let rec WF_rect
1430  (A : Type[0])
1431  (R : A → A → Prop)
1432  (P : A → Type[0])
1433  (f : ∀ x : A.
1434       (∀ y : A. R y x → WF ? R y) →
1435       (∀ y : A. R y x → P y) → P x)
1436  (x : A)
1437  (a : WF A R x) on a : P x ≝
1438f x (Acc_elim … a) (λy:A. λRel:R y x. WF_rect A R P f y ((Acc_elim … a) y Rel)).
1439
1440lemma lset_eq_concrete_filter : ∀A:DeqSet.∀tl.∀hd.
1441  lset_eq_concrete A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
1442#A #tl elim tl
1443[ 1: #hd //
1444| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
1445     lapply (eqb_true A hd' hd)
1446     cases (hd'==hd)
1447     [ 2: #_ normalize in match (notb false); normalize nodelta
1448          >cons_to_append >(cons_to_append … hd')
1449          >cons_to_append in ⊢ (???%); >(cons_to_append … hd') in ⊢ (???%);
1450          @(transpose_lset_eq_concrete ? hd' hd [ ] [ ] (filter A (λy:A.¬y==hd) tl') [ ] [ ] tl')
1451          >nil_append >nil_append >nil_append >nil_append
1452          @lset_eq_concrete_cons >nil_append >nil_append
1453          @Hind
1454     | 1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta
1455          >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));
1456          @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))
1457          [ 1: @Hind
1458          | 2: %2
1459          | 3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]
1460     ]
1461] qed.
1462
1463
1464(* The "abstract", observational definition of set equivalence implies the concrete one. *)
1465
1466lemma lset_eq_to_lset_eq_concrete_aux :
1467  ∀A,ll.
1468    head_shared … (\fst ll) (\snd ll) →
1469    lset_eq (carr A) (\fst ll) (\snd ll) →
1470    lset_eq_concrete A (\fst ll) (\snd ll).
1471#A #ll @(WF_ind ????? (filtered_lists_wf A ll))
1472* *
1473[ 1: #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hb2 >Hb2 #_ %2
1474| 2: #hd1 #tl1 #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hmem
1475     lapply (list_mem_split ??? Hmem) * #l2A * #l2B #Hb2 #Heq
1476     destruct
1477     lapply (Hind_wf 〈filter … (λx.¬x==hd1) tl1,filter … (λx.¬x==hd1) (l2A@l2B)〉)
1478     cut (filtered_lists A 〈filter A (λx:A.¬x==hd1) tl1,filter A (λx:A.¬x==hd1) (l2A@l2B)〉 〈hd1::tl1,l2A@[hd1]@l2B〉)
1479     [ @conj try @conj try @refl whd
1480       [ 1: /2 by /
1481       | 2: >filter_append in ⊢ (???%); >filter_append in ⊢ (???%);
1482            whd in match (filter ?? [hd1]);
1483            elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1484            normalize nodelta <filter_append @refl ] ]
1485     #Hfiltered #Hind_aux lapply (Hind_aux Hfiltered) -Hind_aux
1486     cut (lset_eq A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1487     [ 1: lapply (lset_eq_filter_monotonic … Heq hd1)
1488          >filter_cons_unfold >filter_append >(filter_append … [hd1])
1489          whd in match (filter ?? [hd1]);
1490          elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1491          normalize nodelta <filter_append #Hsol @Hsol ]
1492     #Hset_eq
1493     cut (head_shared A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1494     [ 1: lapply Hset_eq cases (filter A (λx:A.¬x==hd1) tl1)
1495          [ 1: whd in ⊢ (% → ?); * #_ elim (filter A (λx:A.¬x==hd1) (l2A@l2B)) //
1496               #hd' #tl' normalize #Hind * @False_ind
1497          | 2: #hd' #tl' * #Hincl1 #Hincl2 whd elim Hincl1 #Hsol #_ @Hsol ] ]
1498     #Hshared #Hind_aux lapply (Hind_aux Hshared Hset_eq)
1499     #Hconcrete_set_eq
1500     >cons_to_append
1501     @(transitive_lset_eq_concrete ? ([hd1]@tl1) ([hd1]@l2A@l2B) (l2A@[hd1]@l2B))
1502     [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete ]
1503     lapply (lset_eq_concrete_cons … Hconcrete_set_eq hd1) #Hconcrete_cons_eq
1504     @(square_lset_eq_concrete … Hconcrete_cons_eq)
1505     [ 1: @(lset_eq_concrete_filter ? tl1 hd1)
1506     | 2: @(lset_eq_concrete_filter ? (l2A@l2B) hd1) ]
1507] qed.
1508
1509lemma lset_eq_to_lset_eq_concrete : ∀A,l1,l2. lset_eq (carr A) l1 l2 → lset_eq_concrete A l1 l2.
1510#A *
1511[ 1: #l2 #Heq >(lset_eq_empty_inv … (symmetric_lset_eq … Heq)) //
1512| 2: #hd1 #tl1 #l2 #Hincl lapply Hincl lapply (lset_eq_to_lset_eq_concrete_aux ? 〈hd1::tl1,l2〉) #H @H
1513     whd elim Hincl * //
1514] qed.
1515
1516
1517(* The concrete one implies the abstract one. *)
1518lemma lset_eq_concrete_to_lset_eq : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq A l1 l2.
1519#A #l1 #l2 #Hconcrete
1520elim Hconcrete try //
1521#a #b #c #Hstep #Heq_bc_concrete #Heq_bc
1522cut (lset_eq A a b)
1523[ 1: elim Hstep
1524     [ 1: #a' elim a'
1525          [ 2: #hda #tla #Hind #x #b' #y #c' >cons_to_append
1526               >(associative_append ? [hda] tla ?)
1527               >(associative_append ? [hda] tla ?)
1528               @cons_monotonic_eq >nil_append >nil_append @Hind
1529          | 1: #x #b' #y #c' >nil_append >nil_append
1530               elim b' try //
1531               #hdb #tlc #Hind >append_cons >append_cons in ⊢ (???%);
1532               >associative_append >associative_append
1533               lapply (cons_monotonic_eq … Hind hdb) #Hind'               
1534               @(transitive_lset_eq ? ([x]@[hdb]@tlc@[y]@c') ([hdb]@[x]@tlc@[y]@c'))
1535               /2 by transitive_lset_eq/ ]
1536     | 2: #a' elim a'
1537          [ 2: #hda #tla #Hind #x #b' >cons_to_append
1538               >(associative_append ? [hda] tla ?)
1539               >(associative_append ? [hda] tla ?)
1540               @cons_monotonic_eq >nil_append >nil_append @Hind
1541          | 1: #x #b' >nil_append >nil_append @conj normalize
1542               [ 1: @conj [ 1: %1 @refl ] elim b'
1543                    [ 1: @I
1544                    | 2: #hdb #tlb #Hind normalize @conj
1545                         [ 1: %2 %2 %1 @refl
1546                         | 2: @(All_mp … Hind) #a0 *
1547                              [ 1: #Heq %1 @Heq
1548                              | 2: * /2 by or_introl, or_intror/ ] ] ]
1549                    #H %2 %2 %2 @H
1550               | 2: @conj try @conj try /2 by or_introl, or_intror/ elim b'
1551                    [ 1: @I
1552                    | 2: #hdb #tlb #Hind normalize @conj
1553                         [ 1: %2 %1 @refl
1554                         | 2: @(All_mp … Hind) #a0 *
1555                              [ 1: #Heq %1 @Heq
1556                              | 2: #H %2 %2 @H ] ] ] ] ]
1557     | 3: #a #x #b elim a try @lset_eq_contract
1558          #hda #tla #Hind @cons_monotonic_eq @Hind ] ]
1559#Heq_ab @(transitive_lset_eq … Heq_ab Heq_bc)
1560qed.
1561
1562lemma lset_eq_fold :
1563  ∀A : DeqSet.
1564  ∀acctype : Type[0].
1565  ∀eqrel : acctype → acctype → Prop.
1566  ∀refl_eqrel  : reflexive ? eqrel.
1567  ∀trans_eqrel : transitive ? eqrel.
1568  ∀sym_eqrel   : symmetric ? eqrel.
1569  ∀f:carr A → acctype → acctype.
1570  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1571  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1572  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1573  ∀l1,l2 : list (carr A).
1574  lset_eq A l1 l2 → 
1575  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1576#A #acctype #eqrel #refl_eqrel #trans_eqrel #sym_eqrel #f #Hinj #Hsym #Hcontract #l1 #l2 #Heq #acc
1577lapply (lset_eq_to_lset_eq_concrete … Heq) #Heq_concrete
1578@(lset_eq_concrete_fold_ext A acctype eqrel refl_eqrel trans_eqrel sym_eqrel f Hinj Hsym Hcontract l1 l2 Heq_concrete acc)
1579qed.
1580
1581(* Additional lemmas on lsets *)
1582
1583lemma lset_difference_empty :
1584  ∀A : DeqSet.
1585  ∀s1. lset_difference A s1 [ ] = s1.
1586#A #s1 elim s1 try //
1587#hd #tl #Hind >lset_difference_unfold >Hind @refl
1588qed.
1589
1590lemma lset_not_mem_difference :
1591  ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3).
1592#A #s1 #s2 #s3 #Hincl #x #Hmem
1593lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
1594elim s1 in Hincl Hmem;
1595[ 1: #_ *
1596| 2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall *
1597     [ 2: #Hmem_x_tl @Hind assumption
1598     | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]
1599] qed.
1600
1601lemma lset_mem_inclusion_mem :
1602  ∀A,s1,s2,elt.
1603  mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2.
1604#A #s1 elim s1
1605[ 1: #s2 #elt *
1606| 2: #hd #tl #Hind #s2 #elt *
1607     [ 1: #Heq destruct * //
1608     | 2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl;
1609          [ 1: #_ *
1610          | 2: #hd' #tl' #Hind * #Hmem' #Hall *
1611               [ 1: #Heq destruct @Hmem'
1612               | 2: #Hmem'' @Hind assumption ] ] ] ]
1613qed.
1614
1615lemma lset_remove_inclusion :
1616  ∀A : DeqSet. ∀s,elt.
1617    lset_inclusion A (lset_remove ? s elt) s.
1618#A #s elim s try // qed.
1619
1620lemma lset_difference_remove_inclusion :
1621  ∀A : DeqSet. ∀s1,s2,elt.
1622    lset_inclusion A
1623      (lset_difference ? (lset_remove ? s1 elt) s2) 
1624      (lset_difference ? s1 s2).
1625#A #s elim s try // qed.
1626
1627lemma lset_difference_permute :
1628  ∀A : DeqSet. ∀s1,s2,s3.
1629    lset_difference A s1 (s2 @ s3) =
1630    lset_difference A s1 (s3 @ s2).
1631#A #s1 #s2 elim s2 try //
1632#hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute
1633>Hind elim s3 try //
1634#hd' #tl' #Hind' >cons_to_append >associative_append
1635>associative_append >(cons_to_append … hd tl)
1636>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
1637>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
1638<Hind' generalize in match (lset_difference ???); #foo
1639whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
1640whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
1641elim foo
1642[ 1: normalize @refl
1643| 2: #hd'' #tl'' #Hind normalize
1644      @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with
1645        [ true ⇒ λH. ?
1646        | false ⇒ λH. ?
1647        ] (refl ? (hd''==hd')))
1648      @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with
1649        [ true ⇒ λH'. ?
1650        | false ⇒ λH'. ?
1651        ] (refl ? (hd''==hd)))
1652      normalize nodelta
1653      try @Hind
1654[ 1: normalize >H normalize nodelta @Hind
1655| 2: normalize >H' normalize nodelta @Hind
1656| 3: normalize >H >H' normalize nodelta >Hind @refl
1657] qed.
1658
1659
1660
1661lemma lset_disjoint_dec :
1662  ∀A : DeqSet.
1663  ∀s1,elt,s2.
1664  mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1).
1665#A #s1 #elt #s2
1666@(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ?
1667  with
1668  [ false ⇒ λHA. ?
1669  | true ⇒ λHA. ? ] (refl ? (elt ∈ s1)))
1670[ 1: lapply (memb_to_mem … HA) #Hmem
1671     %1 @Hmem
1672| 2: %2 elim s1 in HA;
1673     [ 1: #_ whd %1 @refl
1674     | 2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?);
1675          >lset_difference_unfold
1676          >lset_difference_unfold2
1677          lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %);
1678          cases (elt==hd1) normalize nodelta
1679          [ 1: #_ #Habsurd destruct
1680          | 2: #HA #HB >HB normalize nodelta %1 @refl ] ] ]
1681qed.
1682
1683lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2.
1684  mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l.
1685#A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/
1686qed.
1687
1688lemma lset_inclusion_difference_aux :
1689  ∀A : DeqSet. ∀s1,s2.
1690  lset_inclusion A s1 s2 →
1691  (lset_eq A s2 (s1@lset_difference A s2 s1)).
1692#A #s1
1693@(WF_ind ????? (filtered_list_wf A s1))
1694*
1695[ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq
1696| 2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl
1697     lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?)
1698     [ 1: whd normalize
1699          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ]
1700     #Hind_wf     
1701     elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq
1702     >cons_to_append in ⊢ (???%); >associative_append
1703     >lset_difference_unfold2
1704     >nil_append
1705     >lset_remove_split >lset_remove_split
1706     normalize in match (lset_remove ? [hd1] hd1);
1707     >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
1708     >nil_append <lset_remove_split >lset_difference_lset_remove_commute
1709     lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?)
1710     [ 1: lapply (lset_inclusion_remove … Hincl hd1)
1711          >Heq @lset_inclusion_eq2
1712          >lset_remove_split >lset_remove_split >lset_remove_split
1713          normalize in match (lset_remove ? [hd1] hd1);
1714          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
1715          >nil_append @reflexive_lset_eq ]
1716     #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind
1717     @lset_eq_concrete_to_lset_eq
1718     lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc
1719     @(square_lset_eq_concrete ????? Hindc) -Hindc -Hind
1720     [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B))
1721          [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete
1722          | 1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ]
1723     | 2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …))
1724          elim (s2A@s2B)
1725          [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq
1726          | 2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold
1727               @(match (hd2∈filter A (λx:A.¬x==hd1) tl1)
1728                 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ?
1729                 with
1730                 [ false ⇒ λH. ?
1731                 | true ⇒ λH. ?
1732                 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta
1733               [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter))
1734                    normalize nodelta @Hind
1735               | 2: @(match (hd2∈tl1)
1736                      return λx. ((hd2∈tl1) = x) → ?
1737                      with
1738                      [ false ⇒ λH'. ?
1739                      | true ⇒ λH'. ?
1740                      ] (refl ? (hd2∈tl1))) normalize nodelta
1741                      [ 1: (* We have hd2 = hd1 *)
1742                            cut (hd2 = hd1)
1743                            [ elim tl1 in H H';
1744                              [ 1: normalize #_ #Habsurd destruct (Habsurd)
1745                              | 2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?);
1746                                    lapply (eqb_true ? hdtl1 hd1)
1747                                    cases (hdtl1==hd1) normalize nodelta
1748                                    [ 1: * #H >(H (refl ??)) #_
1749                                         lapply (eqb_true ? hd2 hd1)
1750                                         cases (hd2==hd1) normalize nodelta *
1751                                         [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl
1752                                         | 2: #_ #_ @Hind ]
1753                                    | 2: #_ normalize lapply (eqb_true ? hd2 hdtl1)
1754                                         cases (hd2 == hdtl1) normalize nodelta *
1755                                         [ 1: #_ #_ #Habsurd destruct (Habsurd)
1756                                         | 2: #_ #_ @Hind ] ] ] ]
1757                           #Heq_hd2hd1 destruct (Heq_hd2hd1)
1758                           @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind)
1759                           #Hind' @(square_lset_eq_concrete … Hind')
1760                           [ 2: @lset_refl
1761                           | 1: >cons_to_append >cons_to_append in ⊢ (???%);
1762                                @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
1763                                [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract
1764                                | 2: >(cons_to_append … hd1 (lset_difference ???))
1765                                     @lset_eq_concrete_cons >nil_append >nil_append
1766                                     @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ]
1767                        | 2: @(match hd2 == hd1
1768                               return λx. ((hd2 == hd1) = x) → ?
1769                               with
1770                               [ true ⇒ λH''. ?
1771                               | false ⇒ λH''. ?
1772                               ] (refl ? (hd2 == hd1)))
1773                             [ 1: whd in match (lset_remove ???) in ⊢ (???%);
1774                                  >H'' normalize nodelta >((proj1 … (eqb_true …)) H'')
1775                                  @(transitive_lset_eq … Hind)
1776                                  @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
1777                                  [ 2: @lset_eq_contract ]                                                                   
1778                                  @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons                                 
1779                                  @switch_lset_eq_concrete
1780                             | 2: whd in match (lset_remove ???) in ⊢ (???%);
1781                                  >H'' >notb_false normalize nodelta
1782                                  @lset_eq_concrete_to_lset_eq
1783                                  lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc
1784                                  lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' -Hindc
1785                                  @(square_lset_eq_concrete … Hindc')
1786                                  [ 1: @symmetric_lset_eq_concrete
1787                                       >cons_to_append >cons_to_append in ⊢ (???%);
1788                                       >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%);
1789                                       @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
1790                                  | 2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
1791                                  ]
1792                              ]
1793                        ]
1794                    ]
1795             ]
1796      ]
1797] qed.             
1798                                                       
1799lemma lset_inclusion_difference :
1800  ∀A : DeqSet.
1801  ∀s1,s2 : lset (carr A).
1802    lset_inclusion ? s1 s2 →
1803    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
1804          lset_disjoint ? s1 s2' ∧
1805          lset_eq ? s2' (lset_difference ? s2 s1).
1806#A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj
1807[ 1: @lset_inclusion_difference_aux @Hincl
1808| 2: /2 by lset_difference_disjoint/
1809| 3,4: @reflexive_lset_inclusion ]
1810qed.
1811
1812(* --------------------------------------------------------------------------- *)
1813(* Stuff on bitvectors, previously in memoryInjections.ma *)
1814(* --------------------------------------------------------------------------- *)
1815(* --------------------------------------------------------------------------- *)   
1816(* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
1817(* --------------------------------------------------------------------------- *)
1818 
1819lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
1820#n #bv whd in match (add_with_carries ????); elim bv //
1821#n #hd #tl #Hind whd in match (fold_right2_i ????????);
1822>Hind normalize
1823cases n in tl;
1824[ 1: #tl cases hd normalize @refl
1825| 2: #n' #tl cases hd normalize @refl ]
1826qed.
1827
1828lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
1829#n #bv whd in match (addition_n ???);
1830>add_with_carries_n_O //
1831qed.
1832
1833lemma replicate_Sn : ∀A,sz,elt.
1834  replicate A (S sz) elt = elt ::: (replicate A sz elt).
1835// qed.
1836
1837lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
1838
1839lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
1840#n #xa #a normalize @refl qed.
1841
1842(* useful facts on carry_of *)
1843lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
1844lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
1845lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
1846lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
1847lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
1848
1849
1850
1851definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
1852
1853lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
1854    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
1855    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
1856#n elim n
1857[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
1858     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
1859     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
1860     normalize #Heq destruct (Heq) @refl
1861| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
1862     destruct #Hind >add_with_carries_Sn >replicate_Sn
1863     whd in match (zero ?) in Hind; lapply Hind
1864     elim (add_with_carries (S (S n'))
1865            (false:::replicate bool (S n') false)
1866            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
1867            normalize >add_with_carries_Sn in Hind;
1868     elim (add_with_carries (S n') (replicate bool (S n') false)
1869                    (replicate bool (S n') false) true) #flags' #bits'
1870     normalize
1871     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
1872            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
1873     normalize #Heq destruct @refl
1874] qed.     
1875
1876lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
1877#n lapply (one_bv_Sn_aux n)
1878whd in match (one_bv ?) in ⊢ (? → (??%%));
1879elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
1880#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
1881qed.
1882
1883lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
1884    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
1885#n   
1886elim n
1887[ 1: #a >(BitVector_O … a) normalize @refl
1888| 2: #n' cases n'
1889     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
1890          >(BitVector_O … tl) normalize cases xa @refl
1891     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
1892          >one_bv_Sn >zero_Sn
1893          lapply (Hind tl)
1894          >add_with_carries_Sn >add_with_carries_Sn
1895          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
1896          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
1897          normalize nodelta @refl
1898] qed.         
1899
1900(* In order to use associativity on increment, we hide it under addition_n. *)
1901lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
1902#n
1903whd in match (increment ??) in ⊢ (∀_.??%?);
1904whd in match (addition_n ???) in ⊢ (∀_.???%);
1905#a lapply (increment_to_addition_n_aux n a)
1906#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
1907qed.
1908
1909(* Explicit formulation of addition *)
1910
1911(* Explicit formulation of the last carry bit *)
1912let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
1913match n return λx. BitVector x → BitVector x → bool with
1914[ O ⇒ λ_,_. init
1915| S x ⇒ λa',b'.
1916  let hd_a ≝ head' … a' in
1917  let hd_b ≝ head' … b' in
1918  let tl_a ≝ tail … a' in
1919  let tl_b ≝ tail … b' in
1920  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
1921] a b.
1922
1923lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
1924  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
1925#n #init #a #b @refl qed.
1926
1927lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
1928  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
1929
1930(* correction of [ith_carry] *)
1931lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
1932  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
1933  head' … flags_ab = ith_carry ? a b init.
1934#n elim n
1935[ 1: #init #a #b #res_ab #flags_ab
1936     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1937     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1938     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1939     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1940     destruct
1941     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
1942     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
1943     @refl
1944| 2: #n' #Hind #init #a #b #res_ab #flags_ab
1945     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1946     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1947     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1948     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1949     destruct
1950     lapply (Hind … init tl_a tl_b tl_res tl_flags)
1951     >add_with_carries_Sn >(ith_carry_Sn (S n'))
1952     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
1953     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
1954     normalize nodelta cases hd_flags_ab normalize nodelta
1955     whd in match (head' ? (S n') ?); #H1 #H2
1956     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
1957] qed.
1958
1959(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
1960definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
1961match n return λx. BitVector x → BitVector x → bool with
1962[ O ⇒ λ_,_. init
1963| S x ⇒ λa',b'.
1964  let hd_a ≝ head' … a' in
1965  let hd_b ≝ head' … b' in
1966  let tl_a ≝ tail … a' in
1967  let tl_b ≝ tail … b' in
1968  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
1969] a b.
1970
1971lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
1972  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
1973#n #a #b // qed.
1974
1975lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
1976  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
1977
1978(* correction of ith_bit *)
1979lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
1980  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
1981  head' … res_ab = ith_bit ? a b init.
1982#n
1983cases n
1984[ 1: #init #a #b #res_ab #flags_ab
1985     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1986     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1987     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1988     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1989     destruct
1990     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
1991     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
1992     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
1993| 2: #n' #init #a #b #res_ab #flags_ab
1994     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1995     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1996     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1997     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1998     destruct
1999     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
2000     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
2001     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
2002     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
2003     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
2004     <(H1 (refl ??)) @refl
2005] qed.
2006
2007(* Transform a function from bit-vectors to bits into a vector by folding *)
2008let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
2009match v with
2010[ VEmpty ⇒ VEmpty ?
2011| VCons sz elt tl ⇒
2012  let bit ≝ f ? v in
2013  bit ::: (bitvector_fold ? tl f)
2014].
2015
2016(* Two-arguments version *)
2017let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
2018match v1  with
2019[ VEmpty ⇒ λ_. VEmpty ?
2020| VCons sz elt tl ⇒ λv2'.
2021  let bit ≝ f ? v1 v2 in
2022  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
2023] v2.
2024
2025lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
2026  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
2027
2028(* These functions pack all the relevant information (including carries) directly. *)
2029definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
2030
2031lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
2032  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
2033 
2034lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
2035
2036(* Prove the equivalence of addition_n_direct with add_with_carries *)
2037lemma addition_n_direct_ok : ∀n,carry,v1,v2.
2038  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
2039#n elim n
2040[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
2041| 2: #n' #Hind #carry #v1 #v2
2042     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
2043     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
2044     lapply (Hind carry tl1 tl2)
2045     lapply (ith_bit_ok ? carry v1 v2)
2046     lapply (ith_carry_ok ? carry v1 v2)
2047     destruct
2048     #Hind >addition_n_direct_Sn
2049     >ith_bit_Sn >add_with_carries_Sn
2050     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
2051     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
2052            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
2053     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
2054     whd in match head'; normalize nodelta
2055     #H1 #H2 >H1 >H2 @refl
2056] qed.
2057
2058lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
2059  (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
2060#n #carry #v1 #v2 <addition_n_direct_ok
2061cases (add_with_carries ????) //
2062qed.
2063 
2064(* trivially lift associativity to our new setting *)     
2065lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
2066  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
2067  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
2068#n #carry1 #carry2 #v1 #v2 #v3
2069<addition_n_direct_ok <addition_n_direct_ok
2070<addition_n_direct_ok <addition_n_direct_ok
2071lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
2072elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
2073elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
2074#H @(sym_eq … H)
2075qed.
2076
2077lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
2078  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
2079#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
2080qed.
2081
2082definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
2083definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
2084
2085
2086(* fold andb on a bitvector. *)
2087let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
2088match b with
2089[ VEmpty ⇒ true
2090| VCons sz elt tl ⇒
2091  andb elt (andb_fold ? tl)
2092].
2093
2094lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
2095
2096lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
2097#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
2098qed.
2099
2100lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
2101  ith_carry … a (one_bv ?) false = andb_fold … a.
2102#n elim n
2103[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
2104     cases hd normalize @refl
2105| 2: #n' #Hind #a
2106     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
2107     lapply (Hind … tl) #Hind >one_bv_Sn
2108     >ith_carry_Sn whd in match (andb_fold ??);
2109     cases hd >Hind @refl
2110] qed.
2111
2112lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
2113  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
2114#n #a
2115elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
2116whd in match (head' ???);
2117-a cases n in tl;
2118[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
2119| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
2120     >ith_increment_carry >tail_Sn
2121     cases hd try //
2122] qed.
2123
2124(* Lemma used to prove involutivity of two-complement negation *)
2125lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
2126   (andb_fold (S n) (negation_bv (S n) v) =
2127    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
2128#n elim n
2129[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
2130| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2131     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
2132     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
2133     cases hd normalize nodelta
2134     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
2135     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
2136     >ith_increment_carry
2137     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
2138] qed.
2139   
2140(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
2141lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
2142#n elim n
2143[ 1: #v >(BitVector_O v) @refl
2144| 2: #n' cases n'
2145     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2146          >(BitVector_O … tl) normalize cases hd @refl
2147     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2148          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
2149          whd in match twocomp_neg_direct; normalize nodelta
2150          whd in match increment_direct; normalize nodelta
2151          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
2152          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
2153          generalize in match (addition_n_direct (S n'')
2154                                                   (negation_bv (S n'')
2155                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
2156                                                   (one_bv (S n'')) false); #tail
2157          >ith_increment_carry >ith_increment_carry
2158          cases hd normalize nodelta
2159          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
2160          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
2161          <twocomp_neg_involutive_aux
2162          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
2163      ]
2164] qed.
2165
2166lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
2167#n #a #b #va #vb #H destruct (H) @conj @refl qed.
2168
2169lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
2170
2171(* Injectivity of increment *)
2172lemma increment_inj : ∀n. ∀a,b : BitVector n.
2173  increment_direct ? a = increment_direct ? b →
2174  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
2175#n whd in match increment_direct; normalize nodelta elim n
2176[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
2177| 2: #n' cases n'
2178   [ 1: #_ #a #b
2179        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
2180        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
2181        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
2182        normalize #H @conj try //
2183   | 2: #n'' #Hind #a #b
2184        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
2185        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
2186        lapply (Hind … tl_a tl_b) -Hind #Hind
2187        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
2188        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
2189        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
2190        lapply (Hind Heq2) * #Heq3 #Heq4
2191        cut (hd_a = hd_b)
2192        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
2193             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
2194             @refl ]
2195        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
2196        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
2197] qed.
2198
2199(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
2200lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
2201  a = b → increment_direct ? a = increment_direct ? b. // qed.
2202
2203(* A more general result. *)
2204lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
2205  addition_n_direct ? x delta false = addition_n_direct ? y delta false →
2206  x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
2207#n elim n
2208[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
2209| 2: #n' #Hind #x #y #delta
2210     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
2211     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
2212     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
2213     >addition_n_direct_Sn >ith_bit_Sn
2214     >addition_n_direct_Sn >ith_bit_Sn
2215     >ith_carry_Sn >ith_carry_Sn
2216     lapply (Hind … tlx tly tld) -Hind #Hind #Heq
2217     elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
2218     lapply (Hind Heq_tl) -Hind * #HindA #HindB
2219     >HindA >HindB >HindB in Heq_hd; #Heq_hd
2220     cut (hdx = hdy)
2221     [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
2222          cases hdx cases hdy normalize #H try @H try @refl
2223          >H try @refl ]
2224     #Heq_hd >Heq_hd @conj @refl
2225] qed.
2226
2227(* We also need it the other way around. *)
2228lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
2229  x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
2230   addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
2231#n elim n
2232[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
2233| 2: #n' #Hind #x #y #delta
2234     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
2235     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
2236     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
2237     #Hneq
2238     cut (hdx ≠ hdy ∨ tlx ≠ tly)
2239     [ @(eq_bv_elim … tlx tly)
2240       [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
2241         #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
2242                                 #H @H @refl ]
2243         #H %1 @H
2244       | #H %2 @H ] ]
2245     -Hneq #Hneq
2246     >addition_n_direct_Sn >addition_n_direct_Sn
2247     >ith_bit_Sn >ith_bit_Sn cases Hneq
2248     [ 1: #Hneq_hd
2249          lapply (addition_n_direct_inj … tlx tly tld)         
2250          @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
2251          [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
2252               % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
2253               lapply Hneq_hd
2254               cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
2255               normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
2256               try @(absurd … Heq_hd Hneq_hd)
2257               elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
2258               try @refl try assumption try @(sym_eq … Heq_hd)
2259          | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
2260               elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
2261     | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
2262          % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
2263          elim Hind -Hind #HA #HB @HA @HB ]
2264] qed.
2265
2266lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
2267
2268lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
2269   ith_carry (S n) a (one_bv (S n)) false
2270   = ith_carry (S n) a (zero (S n)) true.
2271#n elim n
2272[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
2273| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
2274     lapply (Hind tl_a) #Hind
2275     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
2276] qed.
2277
2278lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
2279#n elim n //
2280#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
2281>ith_carry_Sn >(Hind tl) cases hd @refl.
2282qed.
2283
2284lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
2285  addition_n_direct ? v (zero ?) false = v.
2286#n elim n
2287[ 1: #v >(BitVector_O … v) normalize @refl
2288| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2289     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
2290     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
2291     >xorb_false @refl
2292] qed.
2293
2294lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
2295#n elim n
2296[ 1: #a >(BitVector_O … a) normalize @refl
2297| 2: #n' cases n'
2298     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
2299     | 2: #n'' #Hind #a
2300          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
2301          lapply (Hind tl_a) -Hind #Hind
2302          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
2303          >addition_n_direct_Sn >ith_bit_Sn
2304          >xorb_false >Hind @bitvector_cons_eq
2305          >increment_to_carry_aux @refl
2306     ]
2307] qed.
2308
2309lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
2310  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
2311#n #a #b >increment_to_carry_zero <associative_addition_n_direct
2312>neutral_addition_n_direct @refl
2313qed.
2314
2315lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
2316#n #v whd in match (increment ??);
2317>addition_n_direct_ok <increment_to_carry_zero @refl
2318qed.
2319
2320(* Prove -(a + b) = -a + -b *)
2321lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
2322  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
2323whd in match twocomp_neg_direct; normalize nodelta
2324lapply increment_inj_inv
2325whd in match increment_direct; normalize nodelta
2326#H #n #a #b
2327<associative_addition_n_direct @H
2328>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
2329>increment_to_carry
2330-H lapply b lapply a -b -a
2331cases n
2332[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
2333| 2: #n' #a #b
2334     cut (negation_bv ? (addition_n_direct ? a b false)
2335           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
2336          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
2337     [ -n lapply b lapply a elim n'
2338     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
2339          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
2340          cases hd_a cases hd_b normalize @conj @refl
2341     | 2: #n #Hind #a #b
2342          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
2343          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
2344          lapply (Hind tl_a tl_b) * #H1 #H2
2345          @conj
2346          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
2347               >carry_notb >H2 @refl
2348          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
2349               >negation_bv_Sn >negation_bv_Sn
2350               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
2351               >xorb_lneg >xorb_rneg >notb_notb
2352               <xorb_rneg >H2 @refl
2353          ]
2354      ] ]
2355      * #H1 #H2 @H1
2356] qed.
2357
2358lemma addition_n_direct_neg : ∀n. ∀a.
2359 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
2360 ∧ (ith_carry n a (negation_bv n a) false = false).
2361#n elim n
2362[ 1: #a >(BitVector_O … a) @conj @refl
2363| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
2364     lapply (Hind … tl) -Hind * #HA #HB
2365     @conj
2366     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
2367     | 1: >negation_bv_Sn >addition_n_direct_Sn
2368          >ith_bit_Sn >HB >xorb_false >HA
2369          @bitvector_cons_eq elim hd @refl
2370     ]
2371] qed.
2372
2373(* -a + a = 0 *)
2374lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
2375whd in match twocomp_neg_direct;
2376whd in match increment_direct;
2377normalize nodelta
2378#n #a <associative_addition_n_direct
2379elim (addition_n_direct_neg … a) #H #_ >H
2380-H -a
2381cases n try //
2382#n'
2383cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
2384       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
2385[ elim n'
2386     [ 1: @conj @refl
2387     | 2: #n' * #HA #HB @conj
2388          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
2389               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
2390          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
2391     ]
2392] * #H1 #H2 @H1
2393qed.
2394
2395(* Lift back the previous result to standard operations. *)
2396lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
2397#n #v whd in match twocomp_neg_direct; normalize nodelta
2398whd in match increment_direct; normalize nodelta
2399whd in match two_complement_negation; normalize nodelta
2400>increment_to_addition_n <addition_n_direct_ok
2401whd in match addition_n; normalize nodelta
2402elim (add_with_carries ????) #a #b @refl
2403qed.
2404
2405lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
2406  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
2407#n #a #b
2408lapply (twocomp_neg_plus ? a b)
2409>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
2410<addition_n_direct_ok <addition_n_direct_ok
2411whd in match addition_n; normalize nodelta
2412elim (add_with_carries n a b false) #bits #flags normalize nodelta
2413elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
2414normalize nodelta #H @H
2415qed.
2416
2417lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
2418#n #a lapply (bitvector_opp_direct ? a)
2419>twocomp_neg_direct_ok <addition_n_direct_ok
2420whd in match (addition_n ???);
2421elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
2422qed.
2423
2424lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
2425#n #a
2426lapply (neutral_addition_n_direct n a)
2427<addition_n_direct_ok
2428whd in match (addition_n ???);
2429elim (add_with_carries n a (zero n) false) #bits #flags #H @H
2430qed.
2431
2432lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
2433  addition_n ? x delta = addition_n ? y delta → x = y. 
2434#n #x #y #delta 
2435lapply (addition_n_direct_inj … x y delta)
2436<addition_n_direct_ok <addition_n_direct_ok
2437whd in match addition_n; normalize nodelta
2438elim (add_with_carries n x delta false) #bitsx #flagsx
2439elim (add_with_carries n y delta false) #bitsy #flagsy
2440normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
2441qed.
2442
2443lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
2444  x ≠ y → addition_n ? x delta ≠ addition_n ? y delta. 
2445#n #x #y #delta 
2446lapply (addition_n_direct_inj_inv … x y delta)
2447<addition_n_direct_ok <addition_n_direct_ok
2448whd in match addition_n; normalize nodelta
2449elim (add_with_carries n x delta false) #bitsx #flagsx
2450elim (add_with_carries n y delta false) #bitsy #flagsy
2451normalize #H1 #H2 @(H1 H2)
2452qed.
2453
2454(* --------------------------------------------------------------------------- *)
2455(* Inversion principles for binary operations *)
2456(* --------------------------------------------------------------------------- *)
2457
2458lemma sem_add_ip_inversion :
2459  ∀sz,sg,ty',optlen.
2460  ∀v1,v2,res.
2461  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
2462  ∃sz',i. v1 = Vint sz' i ∧
2463      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
2464       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
2465#tsz #tsg #ty' * [ | #n ]
2466*
2467[ | #sz' #i' | | #p'
2468| | #sz' #i' | | #p' ]
2469#v2 #res
2470whd in ⊢ ((??%?) → ?);
2471#H destruct
2472cases v2 in H;
2473[ | #sz2' #i2' | | #p2'
2474| | #sz2' #i2' | | #p2' ] normalize nodelta
2475#H destruct
2476[ 1,3:
2477  lapply H -H
2478  @(eq_bv_elim … i' (zero ?)) normalize nodelta
2479  #Hi #Heq destruct (Heq)
2480  %{sz'} %{(zero ?)} @conj destruct try @refl
2481  %2 @conj try @conj try @refl
2482| *: %{sz'} %{i'} @conj try @refl
2483  %1 %{p2'} @conj try @refl
2484] qed.
2485
2486(* symmetric of the upper one *)
2487lemma sem_add_pi_inversion :
2488  ∀sz,sg,ty',optlen.
2489  ∀v1,v2,res.
2490  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
2491  ∃sz',i. v2 = Vint sz' i ∧
2492      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
2493       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
2494#tsz #tsg #ty' * [ | #n ]
2495*
2496[ | #sz' #i' | | #p'
2497| | #sz' #i' | | #p' ]
2498#v2 #res
2499whd in ⊢ ((??%?) → ?);
2500#H destruct
2501cases v2 in H; normalize nodelta
2502[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
2503#H destruct
2504[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
2505  %{p'} @conj try @refl
2506| *: lapply H -H
2507  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
2508  #Hi #Heq destruct (Heq)
2509  %{sz2'} %{(zero ?)} @conj destruct try @refl
2510  %2 @conj try @conj try @refl
2511] qed.
2512
2513(* Know that addition on integers gives an integer. Notice that there is no correlation
2514   between the size in the types and the size of the integer values. *)
2515lemma sem_add_ii_inversion :
2516  ∀sz,sg.
2517  ∀v1,v2,res.
2518  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
2519  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2520              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
2521#sz #sg
2522*
2523[ | #sz' #i' | | #p' ]
2524#v2 #res
2525whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
2526cases sz cases sg normalize nodelta
2527#H destruct
2528cases v2 in H; normalize nodelta
2529#H1 destruct
2530#H2 destruct #Heq %{sz'} lapply Heq -Heq
2531cases sz' in i'; #i' 
2532whd in match (intsize_eq_elim ???????);
2533cases H1 in H2; #j' normalize nodelta
2534#Heq destruct (Heq)
2535%{i'} %{j'} @conj try @conj try @conj try @refl
2536qed.
2537
2538lemma sem_sub_pp_inversion :
2539  ∀ty1,ty2,n1,n2,target.
2540  ∀v1,v2,res.
2541  sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) target = Some ? res →
2542  ∃sz,sg.
2543    target = Tint sz sg ∧
2544    ((∃p1,p2,i. v1 =  Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧
2545             division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧
2546             res = Vint sz (zero_ext ?? i)) ∨
2547     (v1 =  Vnull ∧ v2 = Vnull ∧ res = Vint sz (zero ?))).
2548#ty1 #ty2 #n1 #n2 #target
2549cut (classify_sub (ptr_type ty1 n1) (ptr_type ty2 n2) =
2550     sub_case_pp n1 n2 ty1 ty2)
2551[ cases n1 cases n2     
2552  [ | #n1 | #n2 | #n2 #n1 ] try @refl ]
2553#Hclassify
2554*
2555[ | #sz #i | | #p ]
2556#v2 #res
2557whd in ⊢ ((??%?) → ?); normalize nodelta
2558#H1 destruct
2559lapply H1 -H1
2560>Hclassify normalize nodelta
2561[ 1,2: #H destruct ]
2562cases v2 normalize nodelta
2563[ | #sz' #i' | | #p'
2564| | #sz' #i' | | #p' ]
2565#H2 destruct
2566cases target in H2;
2567[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
2568| | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
2569normalize nodelta
2570#H destruct
2571[ 2,4,5,6,7,8,9:
2572  cases (eq_block (pblock p) (pblock p')) in H;
2573  normalize nodelta #H destruct
2574  cases (eqb (sizeof ty1) O) in H;
2575  normalize nodelta #H destruct ]
2576%{sz} %{sg} @conj try @refl
2577try /4 by or_introl, or_intror, conj, refl/
2578cases (if_opt_inversion ???? H)
2579#Hblocks_eq -H
2580@(eqb_elim … (sizeof ty1) 0) normalize nodelta
2581[ #Heq_sizeof #Habsurd destruct ]
2582#_ #Hdiv
2583%1 %{p} %{p'}
2584cases (division_u ???) in Hdiv; normalize nodelta
2585[ #Habsurd destruct ] #i #Heq destruct
2586%{i} try @conj try @conj try @conj try @conj try @refl
2587try @(eq_block_to_refl … Hblocks_eq)
2588qed.
2589
2590lemma sem_sub_pi_inversion :
2591  ∀sz,sg,ty',optlen,target.
2592  ∀v1,v2,res.
2593  sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) target = Some ? res →
2594  ∃sz',i. v2 = Vint sz' i ∧
2595      ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨
2596       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
2597#tsz #tsg #ty' * [ | #n ] #target
2598*
2599[ | #sz' #i' | | #p'
2600| | #sz' #i' | | #p' ]
2601#v2 #res
2602whd in ⊢ ((??%?) → ?);
2603#H destruct
2604cases v2 in H; normalize nodelta
2605[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
2606#H destruct
2607[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
2608  %{p'} @conj try @refl
2609| *: lapply H -H
2610  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
2611  #Hi #Heq destruct (Heq)
2612  %{sz2'} %{(zero ?)} @conj destruct try @refl
2613  %2 @conj try @conj try @refl
2614] qed.
2615
2616lemma sem_sub_ii_inversion :
2617  ∀sz,sg,ty.
2618  ∀v1,v2,res.
2619  sem_sub v1 (Tint sz sg) v2 (Tint sz sg) ty = Some ? res →
2620  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2621              res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2).
2622#sz #sg #ty *             
2623[ | #sz' #i' | | #p' ]
2624#v2 #res
2625whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
2626cases sz cases sg normalize nodelta
2627#H destruct
2628cases v2 in H; normalize nodelta
2629#H1 destruct
2630#H2 destruct #Heq %{sz'} lapply Heq -Heq
2631cases sz' in i'; #i' 
2632whd in match (intsize_eq_elim ???????);
2633cases H1 in H2; #j' normalize nodelta
2634#Heq destruct (Heq)
2635%{i'} %{j'} @conj try @conj try @conj try @refl
2636qed.
2637
2638
2639lemma sem_mul_inversion :
2640  ∀sz,sg.
2641  ∀v1,v2,res.
2642  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
2643  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2644              res = Vint sz' (short_multiplication ? i1 i2).
2645#sz #sg *
2646[ | #sz' #i' | | #p' ]
2647#v2 #res
2648whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
2649cases sz cases sg normalize nodelta
2650#H destruct
2651cases v2 in H; normalize nodelta
2652#H1 destruct
2653#H2 destruct #Heq %{sz'} lapply Heq -Heq
2654cases sz' in i'; #i' 
2655whd in match (intsize_eq_elim ???????);
2656cases H1 in H2; #j' normalize nodelta
2657#Heq destruct (Heq)
2658%{i'} %{j'} @conj try @conj try @conj try @refl
2659qed.
2660
2661
2662lemma sem_div_inversion_s :
2663  ∀sz.
2664  ∀v1,v2,res.
2665  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
2666  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2667              match division_s ? i1 i2 with
2668              [ Some q ⇒  res =  (Vint sz' q)
2669              | None ⇒ False ].
2670#sz *
2671[ | #sz' #i' | | #p' ]
2672#v2 #res
2673whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
2674>type_eq_dec_true normalize nodelta
2675#H destruct
2676cases v2 in H; normalize nodelta
2677[ | #sz2' #i2' | | #p2' ]
2678#Heq destruct
2679%{sz'}
2680lapply Heq -Heq
2681cases sz' in i'; #i' 
2682whd in match (intsize_eq_elim ???????);
2683cases sz2' in i2'; #i2' normalize nodelta
2684whd in match (option_map ????); #Hdiv destruct
2685%{i'} %{i2'} @conj try @conj try @conj try @refl
2686cases (division_s ???) in Hdiv;
2687[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
2688qed.
2689
2690lemma sem_div_inversion_u :
2691  ∀sz.
2692  ∀v1,v2,res.
2693  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
2694  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2695              match division_u ? i1 i2 with
2696              [ Some q ⇒  res =  (Vint sz' q)
2697              | None ⇒ False ].
2698#sz *
2699[ | #sz' #i' | | #p' ]
2700#v2 #res
2701whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
2702>type_eq_dec_true normalize nodelta
2703#H destruct
2704cases v2 in H; normalize nodelta
2705[ | #sz2' #i2' | | #p2' ]
2706#Heq destruct
2707%{sz'}
2708lapply Heq -Heq
2709cases sz' in i'; #i' 
2710whd in match (intsize_eq_elim ???????);
2711cases sz2' in i2'; #i2' normalize nodelta
2712whd in match (option_map ????); #Hdiv destruct
2713%{i'} %{i2'} @conj try @conj try @conj try @refl
2714cases (division_u ???) in Hdiv;
2715[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
2716qed.
2717
2718lemma sem_mod_inversion_s :
2719  ∀sz.
2720  ∀v1,v2,res.
2721  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
2722  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2723              match modulus_s ? i1 i2 with
2724              [ Some q ⇒  res =  (Vint sz' q)
2725              | None ⇒ False ].
2726#sz *
2727[ | #sz' #i' | | #p' ]
2728#v2 #res
2729whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
2730>type_eq_dec_true normalize nodelta
2731#H destruct
2732cases v2 in H; normalize nodelta
2733[ | #sz2' #i2' | | #p2' ]
2734#Heq destruct
2735%{sz'}
2736lapply Heq -Heq
2737cases sz' in i'; #i' 
2738whd in match (intsize_eq_elim ???????);
2739cases sz2' in i2'; #i2' normalize nodelta
2740whd in match (option_map ????); #Hdiv destruct
2741%{i'} %{i2'} @conj try @conj try @conj try @refl
2742cases (modulus_s ???) in Hdiv;
2743[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
2744qed.
2745
2746lemma sem_mod_inversion_u :
2747  ∀sz.
2748  ∀v1,v2,res.
2749  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
2750  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2751              match modulus_u ? i1 i2 with
2752              [ Some q ⇒  res =  (Vint sz' q)
2753              | None ⇒ False ].
2754#sz *
2755[ | #sz' #i' | | #p' ]
2756#v2 #res
2757whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
2758>type_eq_dec_true normalize nodelta
2759#H destruct
2760cases v2 in H; normalize nodelta
2761[ | #sz2' #i2' | | #p2' ]
2762#Heq destruct
2763%{sz'}
2764lapply Heq -Heq
2765cases sz' in i'; #i' 
2766whd in match (intsize_eq_elim ???????);
2767cases sz2' in i2'; #i2' normalize nodelta
2768whd in match (option_map ????); #Hdiv destruct
2769%{i'} %{i2'} @conj try @conj try @conj try @refl
2770cases (modulus_u ???) in Hdiv;
2771[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
2772qed.
2773
2774lemma sem_and_inversion :
2775  ∀v1,v2,res.
2776  sem_and v1 v2 = Some ? res →
2777  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2778              res = Vint sz' (conjunction_bv ? i1 i2).
2779*
2780[ | #sz' #i' | | #p' ]
2781#v2 #res
2782whd in ⊢ ((??%?) → ?);
2783#H destruct
2784cases v2 in H; normalize nodelta
2785[ | #sz2' #i2' | | #p2' ]
2786#Heq destruct
2787%{sz'}
2788lapply Heq -Heq
2789cases sz' in i'; #i' 
2790whd in match (intsize_eq_elim ???????);
2791cases sz2' in i2'; #i2' normalize nodelta
2792#H destruct
2793%{i'} %{i2'} @conj try @conj try @conj try @refl
2794qed.
2795
2796lemma sem_or_inversion :
2797  ∀v1,v2,res.
2798  sem_or v1 v2 = Some ? res →
2799  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2800              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
2801*
2802[ | #sz' #i' | | #p' ]
2803#v2 #res
2804whd in ⊢ ((??%?) → ?);
2805#H destruct
2806cases v2 in H; normalize nodelta
2807[ | #sz2' #i2' | | #p2' ]
2808#Heq destruct
2809%{sz'}
2810lapply Heq -Heq
2811cases sz' in i'; #i' 
2812whd in match (intsize_eq_elim ???????);
2813cases sz2' in i2'; #i2' normalize nodelta
2814#H destruct
2815%{i'} %{i2'} @conj try @conj try @conj try @refl
2816qed.
2817
2818lemma sem_xor_inversion :
2819  ∀v1,v2,res.
2820  sem_xor v1 v2 = Some ? res →
2821  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
2822              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
2823*
2824[ | #sz' #i' | | #p' ]
2825#v2 #res
2826whd in ⊢ ((??%?) → ?);
2827#H destruct
2828cases v2 in H; normalize nodelta
2829[ | #sz2' #i2' | | #p2' ]
2830#Heq destruct
2831%{sz'}
2832lapply Heq -Heq
2833cases sz' in i'; #i' 
2834whd in match (intsize_eq_elim ???????);
2835cases sz2' in i2'; #i2' normalize nodelta
2836#H destruct
2837%{i'} %{i2'} @conj try @conj try @conj try @refl
2838qed.
2839
2840lemma sem_shl_inversion :
2841  ∀v1,v2,res.
2842  sem_shl v1 v2 = Some ? res →
2843  ∃sz1,sz2,i1,i2.
2844              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
2845              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
2846                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
2847              lt_u (bitsize_of_intsize sz2) i2
2848                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
2849*
2850[ | #sz' #i' | | #p' ]
2851#v2 #res
2852whd in ⊢ ((??%?) → ?);
2853#H destruct
2854cases v2 in H; normalize nodelta
2855[ | #sz2' #i2' | | #p2' ]
2856#Heq destruct
2857%{sz'} %{sz2'}
2858lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
2859%{i'} %{i2'}
2860>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
2861qed.
2862
2863lemma sem_shr_inversion :
2864  ∀v1,v2,sz,sg,res.
2865  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
2866  ∃sz1,sz2,i1,i2.
2867              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
2868              lt_u (bitsize_of_intsize sz2) i2
2869                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
2870              match sg with
2871              [ Signed ⇒
2872                 res =
2873                   (Vint sz1
2874                    (shift_right bool (7+pred_size_intsize sz1*8)
2875                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
2876                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
2877              | Unsigned ⇒
2878                 res =
2879                   (Vint sz1
2880                    (shift_right bool (7+pred_size_intsize sz1*8)
2881                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
2882              ].
2883*
2884[ | #sz' #i' | | #p' ]
2885#v2 #sz * #res
2886whd in ⊢ ((??%?) → ?);
2887whd in match (classify_aop ??);
2888>type_eq_dec_true normalize nodelta
2889#H destruct
2890cases v2 in H; normalize nodelta
2891[ | #sz2' #i2' | | #p2'
2892| | #sz2' #i2' | | #p2' ]
2893#Heq destruct
2894%{sz'} %{sz2'}
2895lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
2896%{i'} %{i2'}
2897>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
2898qed.
2899
2900
2901
2902lemma sem_cmp_int_inversion :
2903  ∀v1,v2,sz,sg,op,m,res.
2904   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
2905   ∃sz,i1,i2. v1 = Vint sz i1 ∧
2906              v2 = Vint sz i2 ∧
2907    match sg with
2908    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
2909    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
2910    ].
2911#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
2912whd in ⊢ ((??%?) → ?);
2913whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
2914cases v1
2915[ | #sz #i | | #p ] normalize nodelta
2916#H destruct
2917cases v2 in H;
2918[ | #sz' #i' | | #p' ] normalize nodelta
2919#H destruct lapply H -H
2920cases sz in i; #i
2921cases sz' in i'; #i' cases sg normalize nodelta
2922whd in match (intsize_eq_elim ???????); #H destruct
2923[ 1,2: %{I8}
2924| 3,4: %{I16}
2925| 5,6: %{I32} ] 
2926%{i} %{i'} @conj try @conj try @refl
2927qed.
2928
2929
2930lemma sem_cmp_ptr_inversion :
2931  ∀v1,v2,ty',n,op,m,res.
2932   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
2933   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
2934                 valid_pointer m p1 = true ∧
2935                 valid_pointer m p2 = true ∧
2936                 (if eq_block (pblock p1) (pblock p2)
2937                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
2938                  else sem_cmp_mismatch op) = Some ? res) ∨
2939   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
2940   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
2941   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
2942* [ | #sz #i | | #p ] normalize nodelta
2943#v2 #ty' #n #op
2944* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
2945whd in match (classify_cmp ??); cases n normalize nodelta
2946[ 2,4,6,8: #array_len ]
2947whd in match (ptr_type ty' ?);
2948whd in match (if_type_eq ?????);
2949>type_eq_dec_true normalize nodelta
2950#H destruct
2951cases v2 in H; normalize nodelta
2952[ | #sz' #i' | | #p'
2953| | #sz' #i' | | #p'
2954| | #sz' #i' | | #p'
2955| | #sz' #i' | | #p' ]
2956#H destruct
2957try /6 by or_introl, or_intror, ex_intro, conj/
2958[ 1: %1 %1 %2 %{p} @conj try @conj //
2959| 3: %1 %1 %2 %{p} @conj try @conj //
2960| *: %1 %1 %1 %{p} %{p'}
2961     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
2962     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
2963     try @conj try @conj try @conj try @conj try @conj try @refl try @H
2964     destruct
2965] qed.
Note: See TracBrowser for help on using the repository browser.