source: src/Clight/frontend_misc.ma @ 2588

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

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

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