source: src/Clight/frontend_misc.ma @ 2582

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

Some progress on CL to CM.

File size: 93.7 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
668axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2.
669
670axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2.
671
672axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?).
673
674axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
675
676(* dividing zero by something eq zero, not the other way around ofc. *)
677axiom division_u_zero : ∀sz.∀v:BitVector ?. division_u sz (bv_zero ?) v = Some ? (bv_zero ?).
678
679
680(* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *)
681
682
683(* --------------------------------------------------------------------------- *)
684(* Generic properties of equivalence relations *)
685(* --------------------------------------------------------------------------- *)
686
687lemma triangle_diagram :
688  ∀acctype : Type[0].
689  ∀eqrel : acctype → acctype → Prop.
690  ∀refl_eqrel  : reflexive ? eqrel.
691  ∀trans_eqrel : transitive ? eqrel.
692  ∀sym_eqrel   : symmetric ? eqrel.
693  ∀a,b,c. eqrel a b → eqrel a c → eqrel b c.
694#acctype #eqrel #R #T #S #a #b #c
695#H1 #H2 @(T … (S … H1) H2)
696qed.
697
698lemma cotriangle_diagram :
699  ∀acctype : Type[0].
700  ∀eqrel : acctype → acctype → Prop.
701  ∀refl_eqrel  : reflexive ? eqrel.
702  ∀trans_eqrel : transitive ? eqrel.
703  ∀sym_eqrel   : symmetric ? eqrel.
704  ∀a,b,c. eqrel b a → eqrel c a → eqrel b c.
705#acctype #eqrel #R #T #S #a #b #c
706#H1 #H2 @S @(T … H2 (S … H1))
707qed.
708
709(* --------------------------------------------------------------------------- *)
710(* Quick and dirty implementation of finite sets relying on lists. The
711 * implementation is split in two: an abstract equivalence defined using inclusion
712 * of lists, and a concrete one where equivalence is defined as the closure of
713 * duplication, contraction and transposition of elements. We rely on the latter
714 * to prove stuff on folds over sets.  *)
715(* --------------------------------------------------------------------------- *)
716
717definition lset ≝ λA:Type[0]. list A.
718
719(* The empty set. *)
720definition empty_lset ≝ λA:Type[0]. nil A.
721
722(* Standard operations. *)
723definition lset_union ≝ λA:Type[0].λl1,l2 : lset A. l1 @ l2.
724
725definition lset_remove ≝ λA:DeqSet.λl:lset (carr A).λelt:carr A. (filter … (λx.¬x==elt) l).
726
727definition lset_difference ≝ λA:DeqSet.λl1,l2:lset (carr A). (filter … (λx.¬ (memb ? x l2)) l1).
728
729(* Standard predicates on sets *)
730definition lset_in ≝ λA:Type[0].λx : A. λl : lset A. mem … x l.
731
732definition lset_disjoint ≝ λA:Type[0].λl1, l2 : lset A.
733  ∀x,y. mem … x l1 → mem … y l2 → x ≠ y.
734 
735definition lset_inclusion ≝ λA:Type[0].λl1,l2.
736  All A (λx1. mem … x1 l2) l1.
737
738(* Definition of abstract set equivalence. *)
739definition lset_eq ≝ λA:Type[0].λl1,l2.
740  lset_inclusion A l1 l2 ∧
741  lset_inclusion A l2 l1.
742
743(* Properties of inclusion. *) 
744lemma reflexive_lset_inclusion : ∀A. ∀l. lset_inclusion A l l.
745#A #l elim l try //
746#hd #tl #Hind whd @conj
747[ 1: %1 @refl
748| 2: whd in Hind; @(All_mp … Hind)
749     #a #H whd %2 @H
750] qed.
751
752lemma transitive_lset_inclusion : ∀A. ∀l1,l2,l3. lset_inclusion A l1 l2 → lset_inclusion A l2 l3 → lset_inclusion A l1 l3 .
753#A #l1 #l2 #l3
754#Hincl1 #Hincl2 @(All_mp … Hincl1)
755whd in Hincl2;
756#a elim l2 in Hincl2;
757[ 1: normalize #_ @False_ind
758| 2: #hd #tl #Hind whd in ⊢ (% → ?);
759     * #Hmem #Hincl_tl whd in ⊢ (% → ?);
760     * [ 1: #Heq destruct @Hmem
761       | 2: #Hmem_tl @Hind assumption ]
762] qed.
763
764lemma cons_preserves_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A l1 (x::l2).
765#A #l1 #l2 #Hincl #x @(All_mp … Hincl) #a #Hmem whd %2 @Hmem qed.
766
767lemma cons_monotonic_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A (x::l1) (x::l2).
768#A #l1 #l2 #Hincl #x whd @conj
769[ 1: /2 by or_introl/
770| 2: @(All_mp … Hincl) #a #Hmem whd %2 @Hmem ] qed.
771
772lemma lset_inclusion_concat : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A l1 (l3 @ l2).
773#A #l1 #l2 #Hincl #l3 elim l3
774try /2 by cons_preserves_inclusion/
775qed.
776
777lemma lset_inclusion_concat_monotonic : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A (l3 @ l1) (l3 @ l2).
778#A #l1 #l2 #Hincl #l3 elim l3
779try @Hincl #hd #tl #Hind @cons_monotonic_inclusion @Hind
780qed.
781 
782(* lset_eq is an equivalence relation. *)
783lemma reflexive_lset_eq : ∀A. ∀l. lset_eq A l l. /2 by conj/ qed.
784
785lemma transitive_lset_eq : ∀A. ∀l1,l2,l3. lset_eq A l1 l2 → lset_eq A l2 l3 → lset_eq A l1 l3.
786#A #l1 #l2 #l3 * #Hincl1 #Hincl2 * #Hincl3 #Hincl4
787@conj @(transitive_lset_inclusion ??l2) assumption
788qed.
789
790lemma symmetric_lset_eq : ∀A. ∀l1,l2. lset_eq A l1 l2 → lset_eq A l2 l1.
791#A #l1 #l2 * #Hincl1 #Hincl2 @conj assumption
792qed.
793
794(* Properties of inclusion vs union and equality. *)
795lemma lset_union_inclusion : ∀A:Type[0]. ∀a,b,c. 
796  lset_inclusion A a c → lset_inclusion ? b c → lset_inclusion ? (lset_union ? a b) c.
797#A #a #b #c #H1 #H2 whd whd in match (lset_union ???);
798@All_append assumption qed.
799
800lemma lset_inclusion_union : ∀A:Type[0]. ∀a,b,c. 
801  lset_inclusion A a b ∨ lset_inclusion A a c → lset_inclusion ? a (lset_union ? b c).
802#A #a #b #c *
803[ 1: @All_mp #elt #Hmem @mem_append_backwards %1 @Hmem
804| 2: @All_mp #elt #Hmem @mem_append_backwards %2 @Hmem
805] qed.
806
807lemma lset_inclusion_eq : ∀A : Type[0]. ∀a,b,c : lset A.
808  lset_eq ? a b → lset_inclusion ? b c → lset_inclusion ? a c.
809#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H1 H3)
810qed.
811
812lemma lset_inclusion_eq2 : ∀A : Type[0]. ∀a,b,c : lset A.
813  lset_eq ? b c → lset_inclusion ? a b → lset_inclusion ? a c.
814#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H3 H1)
815qed.
816
817(* Properties of lset_eq and mem *)
818lemma lset_eq_mem :
819  ∀A:Type[0].
820  ∀s1,s2 : lset A.
821  lset_eq ? s1 s2 →
822  ∀b.mem ? b s1 → mem ? b s2.
823#A #s1 #s2 * #Hincl12 #_ #b
824whd in Hincl12; elim s1 in Hincl12;
825[ 1: normalize #_ *
826| 2: #hd #tl #Hind whd in ⊢ (% → % → ?); * #Hmem' #Hall * #Heq
827     [ 1: destruct (Heq) assumption
828     | 2: @Hind assumption ]
829] qed.
830
831lemma lset_eq_memb :
832  ∀A : DeqSet.
833  ∀s1,s2 : lset (carr A).
834  lset_eq ? s1 s2 →
835  ∀b.memb ? b s1 = true → memb ? b s2 = true.
836#A #s1 #s2 #Heq #b
837lapply (memb_to_mem A s1 b) #H1 #H2
838lapply (H1 H2) #Hmem lapply (lset_eq_mem … Heq ? Hmem) @mem_to_memb
839qed.
840
841lemma lset_eq_memb_eq :
842  ∀A : DeqSet.
843  ∀s1,s2 : lset (carr A).
844  lset_eq ? s1 s2 →
845  ∀b.memb ? b s1 = memb ? b s2.
846#A #s1 #s2 #Hlset_eq #b
847lapply (lset_eq_memb … Hlset_eq b)
848lapply (lset_eq_memb … (symmetric_lset_eq … Hlset_eq) b) 
849cases (b∈s1)
850[ 1: #_ #H lapply (H (refl ??)) #Hmem >H @refl
851| 2: cases (b∈s2) // #H lapply (H (refl ??)) #Habsurd destruct
852] qed.
853
854lemma lset_eq_filter_eq :
855  ∀A : DeqSet.
856  ∀s1,s2 : lset (carr A).
857  lset_eq ? s1 s2 → 
858  ∀l.
859     (filter ? (λwb.¬wb∈s1) l) =
860     (filter ? (λwb.¬wb∈s2) l).
861#A #s1 #s2 #Heq #l elim l
862[ 1: @refl
863| 2: #hd #tl #Hind >filter_cons_unfold >filter_cons_unfold
864      >(lset_eq_memb_eq … Heq) cases (hd∈s2)
865      normalize in match (notb ?); normalize nodelta
866      try @Hind >Hind @refl
867] qed.
868
869lemma cons_monotonic_eq : ∀A. ∀l1,l2 : lset A. lset_eq A l1 l2 → ∀x. lset_eq A (x::l1) (x::l2).
870#A #l1 #l2 #Heq #x cases Heq #Hincl1 #Hincl2
871@conj
872[ 1: @cons_monotonic_inclusion
873| 2: @cons_monotonic_inclusion ]
874assumption
875qed.
876
877(* Properties of difference and remove *)
878lemma lset_difference_unfold :
879  ∀A : DeqSet.
880  ∀s1, s2 : lset (carr A).
881  ∀hd. lset_difference A (hd :: s1) s2 =
882    if hd∈s2 then
883      lset_difference A s1 s2
884    else
885      hd :: (lset_difference A s1 s2).
886#A #s1 #s2 #hd normalize
887cases (hd∈s2) @refl
888qed.
889
890lemma lset_difference_unfold2 :
891  ∀A : DeqSet.
892  ∀s1, s2 : lset (carr A).
893  ∀hd. lset_difference A s1 (hd :: s2) =
894       lset_difference A (lset_remove ? s1 hd) s2.
895#A #s1
896elim s1
897[ 1: //
898| 2: #hd1 #tl1 #Hind #s2 #hd
899     whd in match (lset_remove ???);
900     whd in match (lset_difference A ??);
901     whd in match (memb ???);
902     lapply (eqb_true … hd1 hd)
903     cases (hd1==hd) normalize nodelta
904     [ 1: * #H #_ lapply (H (refl ??)) -H #H
905           @Hind
906     | 2: * #_ #Hguard >lset_difference_unfold
907          cases (hd1∈s2) normalize in match (notb ?); normalize nodelta
908          <Hind @refl ]
909] qed.         
910
911lemma lset_difference_disjoint :
912 ∀A : DeqSet.
913 ∀s1,s2 : lset (carr A).
914  lset_disjoint A s1 (lset_difference A s2 s1).
915#A #s1 elim s1
916[ 1: #s2 normalize #x #y *
917| 2: #hd1 #tl1 #Hind #s2 >lset_difference_unfold2 #x #y
918     whd in ⊢ (% → ?); *
919     [ 2: @Hind
920     | 1: #Heq >Heq elim s2
921          [ 1: normalize *
922          | 2: #hd2 #tl2 #Hind2 whd in match (lset_remove ???);
923               lapply (eqb_true … hd2 hd1)
924               cases (hd2 == hd1) normalize in match (notb ?); normalize nodelta * #H1 #H2
925               [ 1: @Hind2
926               | 2: >lset_difference_unfold cases (hd2 ∈ tl1) normalize nodelta try @Hind2
927                     whd in ⊢ (% → ?); *
928                     [ 1: #Hyhd2 destruct % #Heq lapply (H2 … (sym_eq … Heq)) #Habsurd destruct
929                     | 2: @Hind2 ]
930               ]
931          ]
932    ]
933] qed.
934
935
936lemma lset_remove_split : ∀A : DeqSet. ∀l1,l2 : lset A. ∀elt. lset_remove A (l1 @ l2) elt = (lset_remove … l1 elt) @ (lset_remove … l2 elt).
937#A #l1 #l2 #elt /2 by filter_append/ qed.
938
939lemma lset_inclusion_remove :
940  ∀A : DeqSet.
941  ∀s1, s2 : lset A.
942  lset_inclusion ? s1 s2 →
943  ∀elt. lset_inclusion ? (lset_remove ? s1 elt) (lset_remove ? s2 elt).
944#A #s1 elim s1
945[ 1: normalize //
946| 2: #hd1 #tl1 #Hind1 #s2 * #Hmem #Hincl
947     elim (list_mem_split ??? Hmem) #s2A * #s2B #Hs2_eq destruct #elt
948     whd in match (lset_remove ???);
949     @(match (hd1 == elt)
950       return λx. (hd1 == elt = x) → ?
951       with
952       [ true ⇒ λH. ?
953       | false ⇒ λH. ? ] (refl ? (hd1 == elt))) normalize in match (notb ?);
954     normalize nodelta
955     [ 1:  @Hind1 @Hincl
956     | 2: whd @conj
957          [ 2: @(Hind1 … Hincl)
958          | 1: >lset_remove_split >lset_remove_split
959               normalize in match (lset_remove A [hd1] elt);
960               >H normalize nodelta @mem_append_backwards %2
961               @mem_append_backwards %1 normalize %1 @refl ]
962     ]
963] qed.
964
965lemma lset_difference_lset_eq :
966  ∀A : DeqSet. ∀a,b,c.
967   lset_eq A b c →
968   lset_eq A (lset_difference A a b) (lset_difference A a c).
969#A #a #b #c #Heq
970whd in match (lset_difference ???) in ⊢ (??%%);   
971elim a
972[ 1: normalize @conj @I
973| 2: #hda #tla #Hind whd in match (foldr ?????) in ⊢ (??%%);
974     >(lset_eq_memb_eq … Heq hda) cases (hda∈c)
975     normalize in match (notb ?); normalize nodelta
976     try @Hind @cons_monotonic_eq @Hind
977] qed.
978
979lemma lset_difference_lset_remove_commute :
980  ∀A:DeqSet.
981  ∀elt,s1,s2.
982  (lset_difference A (lset_remove ? s1 elt) s2) =
983  (lset_remove A (lset_difference ? s1 s2) elt).
984#A #elt #s1 #s2
985elim s1 try //
986#hd #tl #Hind
987>lset_difference_unfold
988whd in match (lset_remove ???);
989@(match (hd==elt) return λx. (hd==elt) = x → ?
990  with
991  [ true ⇒ λHhd. ?
992  | false ⇒ λHhd. ?
993  ] (refl ? (hd==elt)))
994@(match (hd∈s2) return λx. (hd∈s2) = x → ?
995  with
996  [ true ⇒ λHmem. ?
997  | false ⇒ λHmem. ?
998  ] (refl ? (hd∈s2)))
999>notb_true >notb_false normalize nodelta try //
1000try @Hind
1001[ 1:  whd in match (lset_remove ???) in ⊢ (???%); >Hhd
1002     elim (eqb_true ? elt elt) #_ #H >(H (refl ??))
1003     normalize in match (notb ?); normalize nodelta @Hind
1004| 2: >lset_difference_unfold >Hmem @Hind
1005| 3: whd in match (lset_remove ???) in ⊢ (???%);
1006     >lset_difference_unfold >Hhd >Hmem
1007     normalize in match (notb ?);
1008     normalize nodelta >Hind @refl
1009] qed.
1010
1011(* Inversion lemma on emptyness *)
1012lemma lset_eq_empty_inv : ∀A. ∀l. lset_eq A l [ ] → l = [ ].
1013#A #l elim l //
1014#hd' #tl' normalize #Hind * * @False_ind
1015qed.
1016
1017(* Inversion lemma on singletons *)
1018lemma lset_eq_singleton_inv : ∀A,hd,l. lset_eq A [hd] (hd::l) → All ? (λx.x=hd) l.
1019#A #hd #l
1020* #Hincl1 whd in ⊢ (% → ?); * #_ @All_mp
1021normalize #a * [ 1: #H @H | 2: @False_ind ]
1022qed.
1023
1024(* Permutation of two elements on top of the list is ok. *)
1025lemma lset_eq_permute : ∀A,l,x1,x2. lset_eq A (x1 :: x2 :: l) (x2 :: x1 :: l).
1026#A #l #x1 #x2 @conj normalize
1027[ 1: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
1028| 2: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
1029] qed.
1030
1031(* "contraction" of an element. *)
1032lemma lset_eq_contract : ∀A,l,x. lset_eq A (x :: x :: l) (x :: l).
1033#A #l #x @conj
1034[ 1: /5 by or_introl, conj, transitive_lset_inclusion/
1035| 2: /5 by cons_preserves_inclusion, cons_monotonic_inclusion/ ]
1036qed.
1037
1038(* We don't need more than one instance of each element. *)
1039lemma lset_eq_filter : ∀A:DeqSet.∀tl.∀hd.
1040  lset_eq A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
1041#A #tl elim tl
1042[ 1: #hd normalize /4 by or_introl, conj, I/
1043| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
1044     lapply (eqb_true A hd' hd) cases (hd'==hd)
1045     [ 2: #_ normalize in match (notb ?); normalize nodelta
1046          lapply (cons_monotonic_eq … (Hind hd) hd') #H
1047          lapply (lset_eq_permute ? tl' hd' hd) #H'
1048          @(transitive_lset_eq ? ? (hd'::hd::tl') ? … H')
1049          @(transitive_lset_eq ? ?? (hd'::hd::tl') … H)
1050          @lset_eq_permute
1051     | 1: * #Heq #_ >(Heq (refl ??)) normalize in match (notb ?); normalize nodelta
1052          lapply (Hind hd) #H
1053          @(transitive_lset_eq ? ? (hd::tl') (hd::hd::tl') H)
1054          @conj
1055          [ 1: whd @conj /2 by or_introl/ @cons_preserves_inclusion @cons_preserves_inclusion
1056               @reflexive_lset_inclusion
1057          | 2: whd @conj /2 by or_introl/ ]
1058     ]
1059] qed.
1060
1061lemma lset_inclusion_filter_self :
1062  ∀A:DeqSet.∀l,pred.
1063    lset_inclusion A (filter ? pred l) l.
1064#A #l #pred elim l
1065[ 1: normalize @I
1066| 2: #hd #tl #Hind whd in match (filter ???);
1067     cases (pred hd) normalize nodelta
1068     [ 1: @cons_monotonic_inclusion @Hind
1069     | 2: @cons_preserves_inclusion @Hind ]
1070] qed.   
1071
1072lemma lset_inclusion_filter_monotonic :
1073  ∀A:DeqSet.∀l1,l2. lset_inclusion (carr A) l1 l2 →
1074  ∀elt. lset_inclusion A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
1075#A #l1 elim l1
1076[ 1: #l2 normalize //
1077| 2: #hd1 #tl1 #Hind #l2 whd in ⊢ (% → ?); * #Hmem1 #Htl1_incl #elt
1078     whd >filter_cons_unfold
1079     lapply (eqb_true A hd1 elt) cases (hd1==elt)
1080     [ 1: * #H1 #_ lapply (H1 (refl ??)) #H1_eq >H1_eq in Hmem1; #Hmem
1081          normalize in match (notb ?); normalize nodelta @Hind assumption
1082     | 2: * #_ #Hneq normalize in match (notb ?); normalize nodelta
1083          whd @conj
1084          [ 1: elim l2 in Hmem1; try //
1085               #hd2 #tl2 #Hincl whd in ⊢ (% → ?); *
1086               [ 1: #Heq >Heq in Hneq; normalize
1087                    lapply (eqb_true A hd2 elt) cases (hd2==elt)
1088                    [ 1: * #H #_ #H2 lapply (H2 (H (refl ??))) #Habsurd destruct (Habsurd)
1089                    | 2: #_ normalize nodelta #_ /2 by or_introl/ ]
1090               | 2: #H lapply (Hincl H) #Hok
1091                    normalize cases (hd2==elt) normalize nodelta
1092                    [ 1: @Hok
1093                    | 2: %2 @Hok ] ]
1094          | 2: @Hind assumption ] ] ]
1095qed.
1096
1097(* removing an element of two equivalent sets conserves equivalence. *)
1098lemma lset_eq_filter_monotonic :
1099  ∀A:DeqSet.∀l1,l2. lset_eq (carr A) l1 l2 →
1100  ∀elt. lset_eq A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
1101#A #l1 #l2 * #Hincl1 #Hincl2 #elt @conj
1102/2 by lset_inclusion_filter_monotonic/
1103qed.
1104
1105(* ---------------- Concrete implementation of sets --------------------- *)
1106
1107(* We can give an explicit characterization of equivalent sets: they are permutations with repetitions, i,e.
1108   a composition of transpositions and duplications. We restrict ourselves to DeqSets. *)
1109inductive iso_step_lset (A : DeqSet) : lset A → lset A → Prop ≝
1110| lset_transpose : ∀a,x,b,y,c. iso_step_lset A (a @ [x] @ b @ [y] @ c) (a @ [y] @ b @ [x] @ c)
1111| lset_weaken : ∀a,x,b. iso_step_lset A (a @ [x] @ b) (a @ [x] @ [x] @ b)
1112| lset_contract : ∀a,x,b. iso_step_lset A (a @ [x] @ [x] @ b) (a @ [x] @ b).
1113
1114(* The equivalence is the reflexive, transitive and symmetric closure of iso_step_lset *)
1115inductive lset_eq_concrete (A : DeqSet) : lset A → lset A → Prop ≝
1116| lset_trans : ∀a,b,c. iso_step_lset A a b → lset_eq_concrete A b c → lset_eq_concrete A a c
1117| lset_refl  : ∀a. lset_eq_concrete A a a.
1118
1119(* lset_eq_concrete is symmetric and transitive *)
1120lemma 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.
1121#A #l1 #l2 #l3 #Hequiv
1122elim Hequiv //
1123#a #b #c #Hstep #Hequiv #Hind #Hcl3 lapply (Hind Hcl3) #Hbl3
1124@(lset_trans ???? Hstep Hbl3)
1125qed.
1126
1127lemma symmetric_step : ∀A,l1,l2. iso_step_lset A l1 l2 → iso_step_lset A l2 l1.
1128#A #l1 #l2 * /2/ qed.
1129
1130lemma symmetric_lset_eq_concrete : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l1.
1131#A #l1 #l2 #H elim H //
1132#a #b #c #Hab #Hbc #Hcb
1133@(transitive_lset_eq_concrete ???? Hcb ?)
1134@(lset_trans … (symmetric_step ??? Hab) (lset_refl …))
1135qed.
1136 
1137(* lset_eq_concrete is conserved by cons. *)
1138lemma equivalent_step_cons : ∀A,l1,l2. iso_step_lset A l1 l2 → ∀x. iso_step_lset A (x :: l1) (x :: l2).
1139#A #l1 #l2 * // qed. (* That // was impressive. *)
1140
1141lemma lset_eq_concrete_cons : ∀A,l1,l2. lset_eq_concrete A l1 l2 → ∀x. lset_eq_concrete A (x :: l1) (x :: l2).
1142#A #l1 #l2 #Hequiv elim Hequiv try //
1143#a #b #c #Hab #Hbc #Hind #x %1{(equivalent_step_cons ??? Hab x) (Hind x)}
1144qed.
1145
1146lemma absurd_list_eq_append : ∀A.∀x.∀l1,l2:list A. [ ] = l1 @ [x] @ l2 → False.
1147#A #x #l1 #l2 elim l1 normalize
1148[ 1: #Habsurd destruct
1149| 2: #hd #tl #_ #Habsurd destruct
1150] qed.
1151
1152(* Inversion lemma for emptyness, step case *)
1153lemma equivalent_iso_step_empty_inv : ∀A,l. iso_step_lset A l [] → l = [ ].
1154#A #l elim l //
1155#hd #tl #Hind #H inversion H
1156[ 1: #a #x #b #y #c #_ #Habsurd
1157      @(False_ind … (absurd_list_eq_append ? y … Habsurd))
1158| 2: #a #x #b #_ #Habsurd
1159      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
1160| 3: #a #x #b #_ #Habsurd
1161      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
1162] qed.
1163
1164(* Same thing for non-emptyness *)
1165lemma equivalent_iso_step_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → iso_step_lset A l1 l2 → l2 ≠ [ ].
1166#A #l1 elim l1
1167[ 1: #l2 * #H @(False_ind … (H (refl ??)))
1168| 2: #hd #tl #H #l2 #_ #Hstep % #Hl2 >Hl2 in Hstep; #Hstep
1169     lapply (equivalent_iso_step_empty_inv … Hstep) #Habsurd destruct
1170] qed.
1171
1172lemma lset_eq_concrete_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → lset_eq_concrete A l1 l2 → l2 ≠ [ ].
1173#A #l1 #l2 #Hl1 #H lapply Hl1 elim H
1174[ 2: #a #H @H
1175| 1: #a #b #c #Hab #Hbc #H #Ha lapply (equivalent_iso_step_cons_inv … Ha Hab) #Hb @H @Hb
1176] qed.
1177
1178lemma lset_eq_concrete_empty_inv : ∀A,l1,l2. l1 = [ ] → lset_eq_concrete A l1 l2 → l2 = [ ].
1179#A #l1 #l2 #Hl1 #H lapply Hl1 elim H //
1180#a #b #c #Hab #Hbc #Hbc_eq #Ha >Ha in Hab; #H_b lapply (equivalent_iso_step_empty_inv … ?? (symmetric_step … H_b))
1181#Hb @Hbc_eq @Hb
1182qed.
1183
1184(* Square equivalence diagram *)
1185lemma square_lset_eq_concrete :
1186  ∀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'.
1187#A #a #b #a' #b' #H1 #H2 #H3
1188@(transitive_lset_eq_concrete ???? (symmetric_lset_eq_concrete … H2))
1189@(transitive_lset_eq_concrete ???? H1)
1190@H3
1191qed.
1192
1193(* Make the transposition of elements visible at top-level *)
1194lemma transpose_lset_eq_concrete :
1195  ∀A. ∀x,y,a,b,c,a',b',c'.
1196  lset_eq_concrete A (a @ [x] @ b @ [y] @ c) (a' @ [x] @ b' @ [y] @ c') →
1197  lset_eq_concrete A (a @ [y] @ b @ [x] @ c) (a' @ [y] @ b' @ [x] @ c').
1198#A #x #y #a #b #c #a' #b' #c
1199#H @(square_lset_eq_concrete ????? H) /2 by lset_trans, lset_refl, lset_transpose/
1200qed.
1201
1202lemma switch_lset_eq_concrete :
1203  ∀A. ∀a,b,c. lset_eq_concrete A (a@[b]@c) ([b]@a@c).
1204#A #a elim a //
1205#hda #tla #Hind #b #c lapply (Hind hda c) #H
1206lapply (lset_eq_concrete_cons … H b)
1207#H' normalize in H' ⊢ %; @symmetric_lset_eq_concrete
1208/3 by lset_transpose, lset_trans, symmetric_lset_eq_concrete/
1209qed.
1210
1211(* Folding a commutative and idempotent function on equivalent sets yields the same result. *)
1212lemma lset_eq_concrete_fold :
1213  ∀A : DeqSet.
1214  ∀acctype : Type[0].
1215  ∀l1,l2 : list (carr A).
1216  lset_eq_concrete A l1 l2 →
1217  ∀f:carr A → acctype → acctype.
1218  (∀x1,x2. ∀acc. f x1 (f x2 acc) = f x2 (f x1 acc)) →
1219  (∀x.∀acc. f x (f x acc) = f x acc) →
1220  ∀acc. foldr ?? f acc l1 = foldr ?? f acc l2.
1221#A #acctype #l1 #l2 #Heq #f #Hcomm #Hidem
1222elim Heq
1223try //
1224#a' #b' #c' #Hstep #Hbc #H #acc <H -H
1225elim Hstep
1226[ 1: #a #x #b #y #c
1227     >fold_append >fold_append >fold_append >fold_append
1228     >fold_append >fold_append >fold_append >fold_append
1229     normalize
1230     cut (f x (foldr A acctype f (f y (foldr A acctype f acc c)) b) =
1231          f y (foldr A acctype f (f x (foldr A acctype f acc c)) b)) [   
1232     elim c
1233     [ 1: normalize elim b
1234          [ 1: normalize >(Hcomm x y) @refl
1235          | 2: #hdb #tlb #Hind normalize
1236               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ]
1237     | 2: #hdc #tlc #Hind normalize elim b
1238          [ 1: normalize >(Hcomm x y) @refl
1239          | 2: #hdb #tlb #Hind normalize
1240               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] ]
1241     ]
1242     #Hind >Hind @refl
1243| 2: #a #x #b
1244     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
1245     normalize >Hidem @refl
1246| 3: #a #x #b
1247     >fold_append  >(fold_append ?? ([x]@[x])) >fold_append >fold_append
1248     normalize >Hidem @refl
1249] qed.
1250
1251(* Folding over equivalent sets yields equivalent results, for any equivalence. *)
1252lemma inj_to_fold_inj :
1253  ∀A,acctype : Type[0].
1254  ∀eqrel : acctype → acctype → Prop.
1255  ∀refl_eqrel  : reflexive ? eqrel.
1256  ∀trans_eqrel : transitive ? eqrel.
1257  ∀sym_eqrel   : symmetric ? eqrel.
1258  ∀f           : A → acctype → acctype.
1259  (∀x:A.∀acc1:acctype.∀acc2:acctype.eqrel acc1 acc2→eqrel (f x acc1) (f x acc2)) →
1260  ∀l : list A. ∀acc1, acc2 : acctype. eqrel acc1 acc2 → eqrel (foldr … f acc1 l) (foldr … f acc2 l).
1261#A #acctype #eqrel #R #T #S #f #Hinj #l elim l
1262//
1263#hd #tl #Hind #acc1 #acc2 #Heq normalize @Hinj @Hind @Heq
1264qed.
1265
1266(* We need to extend the above proof to arbitrary equivalence relation instead of
1267   just standard equality. *)
1268lemma lset_eq_concrete_fold_ext :
1269  ∀A : DeqSet.
1270  ∀acctype : Type[0].
1271  ∀eqrel : acctype → acctype → Prop.
1272  ∀refl_eqrel  : reflexive ? eqrel.
1273  ∀trans_eqrel : transitive ? eqrel.
1274  ∀sym_eqrel   : symmetric ? eqrel.
1275  ∀f:carr A → acctype → acctype.
1276  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1277  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1278  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1279  ∀l1,l2 : list (carr A).
1280  lset_eq_concrete A l1 l2 → 
1281  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1282#A #acctype #eqrel #R #T #S #f #Hinj #Hcomm #Hidem #l1 #l2 #Heq
1283elim Heq
1284try //
1285#a' #b' #c' #Hstep #Hbc #H inversion Hstep
1286[ 1: #a #x #b #y #c #HlA #HlB #_ #acc
1287     >HlB in H; #H @(T … ? (H acc))
1288     >fold_append >fold_append >fold_append >fold_append
1289     >fold_append >fold_append >fold_append >fold_append
1290     normalize
1291     cut (eqrel (f x (foldr ? acctype f (f y (foldr ? acctype f acc c)) b))
1292                (f y (foldr ? acctype f (f x (foldr ? acctype f acc c)) b)))
1293     [ 1:
1294     elim c
1295     [ 1: normalize elim b
1296          [ 1: normalize @(Hcomm x y)
1297          | 2: #hdb #tlb #Hind normalize
1298               lapply (Hinj hdb ?? Hind) #Hind'
1299               lapply (T … Hind' (Hcomm ???)) #Hind''
1300               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
1301     | 2: #hdc #tlc #Hind normalize elim b
1302          [ 1: normalize @(Hcomm x y)
1303          | 2: #hdb #tlb #Hind normalize
1304               lapply (Hinj hdb ?? Hind) #Hind'
1305               lapply (T … Hind' (Hcomm ???)) #Hind''
1306               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
1307     ] ]
1308     #Hind @(inj_to_fold_inj … eqrel R T S ? Hinj … Hind)
1309| 2: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
1310     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
1311     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @S @Hidem
1312| 3: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
1313     >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append
1314     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @Hidem
1315] qed.
1316
1317(* Prepare some well-founded induction principles on lists. The idea is to perform
1318   an induction on the sequence of filterees of a list : taking the first element,
1319   filtering it out of the tail, etc. We give such principles for pairs of lists
1320   and isolated lists.  *)
1321
1322(* The two lists [l1,l2] share at least the head of l1. *)
1323definition head_shared ≝ λA. λl1,l2 : list A.
1324match l1 with
1325[ nil ⇒ l2 = (nil ?)
1326| cons hd _ ⇒  mem … hd l2
1327].
1328
1329(* Relation on pairs of lists, as described above. *)
1330definition filtered_lists : ∀A:DeqSet. relation (list (carr A)×(list (carr A))) ≝
1331λA:DeqSet. λll1,ll2.
1332let 〈la1,lb1〉 ≝ ll1 in
1333let 〈la2,lb2〉 ≝ ll2 in
1334match la2 with
1335[ nil ⇒ False
1336| cons hda2 tla2 ⇒
1337    head_shared ? la2 lb2 ∧
1338    la1 = filter … (λx.¬(x==hda2)) tla2 ∧
1339    lb1 = filter … (λx.¬(x==hda2)) lb2
1340].
1341
1342(* Notice the absence of plural : this relation works on a simple list, not a pair. *)
1343definition filtered_list : ∀A:DeqSet. relation (list (carr A)) ≝
1344λA:DeqSet. λl1,l2.
1345match l2 with
1346[ nil ⇒ False
1347| cons hd2 tl2 ⇒
1348    l1 = filter … (λx.¬(x==hd2)) l2
1349].
1350
1351(* Relation on lists based on their lengths. We know this one is well-founded. *)
1352definition length_lt : ∀A:DeqSet. relation (list (carr A)) ≝
1353λA:DeqSet. λl1,l2. lt (length ? l1) (length ? l2).
1354
1355(* length_lt can be extended on pairs by just measuring the first component *)
1356definition length_fst_lt : ∀A:DeqSet. relation (list (carr A) × (list (carr A))) ≝
1357λA:DeqSet. λll1,ll2. lt (length ? (\fst ll1)) (length ? (\fst ll2)).
1358
1359lemma filter_length : ∀A. ∀l. ∀f. |filter A f l| ≤ |l|.
1360#A #l #f elim l //
1361#hd #tl #Hind whd in match (filter ???); cases (f hd) normalize nodelta
1362[ 1: /2 by le_S_S/
1363| 2: @le_S @Hind
1364] qed.
1365
1366(* The order on lists defined by their length is wf *)
1367lemma length_lt_wf : ∀A. ∀l. WF (list (carr A)) (length_lt A) l.
1368#A #l % elim l
1369[ 1: #a normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1370| 2: #hd #tl #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1371@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1372qed.
1373
1374(* Order on pairs of list by measuring the first proj *)
1375lemma length_fst_lt_wf : ∀A. ∀ll. WF ? (length_fst_lt A) ll.
1376#A * #l1 #l2 % elim l1
1377[ 1: * #a1 #a2 normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1378| 2: #hd1 #tl1 #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1379@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1380qed.
1381
1382lemma length_to_filtered_lists : ∀A. subR ? (filtered_lists A) (length_fst_lt A).
1383#A whd * #a1 #a2 * #b1 #b2 elim b1
1384[ 1: @False_ind
1385| 2: #hd1 #tl1 #Hind whd in ⊢ (% → ?); * * #Hmem #Ha1 #Ha2 whd
1386     >Ha1 whd in match (length ??) in ⊢ (??%); @le_S_S @filter_length
1387] qed.
1388
1389lemma length_to_filtered_list : ∀A. subR ? (filtered_list A) (length_lt A).
1390#A whd #a #b elim b
1391[ 1: @False_ind
1392| 2: #hd #tl #Hind whd in ⊢ (% → ?); whd in match (filter ???);
1393     lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?);
1394     normalize nodelta #Ha whd @le_S_S >Ha @filter_length ]
1395qed.
1396
1397(* Prove well-foundedness by embedding in lt *)
1398lemma filtered_lists_wf : ∀A. ∀ll. WF ? (filtered_lists A) ll.
1399#A #ll @(WF_antimonotonic … (length_to_filtered_lists A)) @length_fst_lt_wf
1400qed.
1401
1402lemma filtered_list_wf : ∀A. ∀l. WF ? (filtered_list A) l.
1403#A #l @(WF_antimonotonic … (length_to_filtered_list A)) @length_lt_wf
1404qed.
1405
1406definition Acc_elim : ∀A,R,x. WF A R x → (∀a. R a x → WF A R a) ≝
1407λA,R,x,acc.
1408match acc with
1409[ wf _ a0 ⇒ a0 ].
1410
1411(* Stolen from Coq. Warped to avoid prop-to-type restriction. *)
1412let rec WF_rect
1413  (A : Type[0])
1414  (R : A → A → Prop)
1415  (P : A → Type[0])
1416  (f : ∀ x : A.
1417       (∀ y : A. R y x → WF ? R y) →
1418       (∀ y : A. R y x → P y) → P x)
1419  (x : A)
1420  (a : WF A R x) on a : P x ≝
1421f x (Acc_elim … a) (λy:A. λRel:R y x. WF_rect A R P f y ((Acc_elim … a) y Rel)).
1422
1423lemma lset_eq_concrete_filter : ∀A:DeqSet.∀tl.∀hd.
1424  lset_eq_concrete A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
1425#A #tl elim tl
1426[ 1: #hd //
1427| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
1428     lapply (eqb_true A hd' hd)
1429     cases (hd'==hd)
1430     [ 2: #_ normalize in match (notb false); normalize nodelta
1431          >cons_to_append >(cons_to_append … hd')
1432          >cons_to_append in ⊢ (???%); >(cons_to_append … hd') in ⊢ (???%);
1433          @(transpose_lset_eq_concrete ? hd' hd [ ] [ ] (filter A (λy:A.¬y==hd) tl') [ ] [ ] tl')
1434          >nil_append >nil_append >nil_append >nil_append
1435          @lset_eq_concrete_cons >nil_append >nil_append
1436          @Hind
1437     | 1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta
1438          >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));
1439          @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))
1440          [ 1: @Hind
1441          | 2: %2
1442          | 3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]
1443     ]
1444] qed.
1445
1446
1447(* The "abstract", observational definition of set equivalence implies the concrete one. *)
1448
1449lemma lset_eq_to_lset_eq_concrete_aux :
1450  ∀A,ll.
1451    head_shared … (\fst ll) (\snd ll) →
1452    lset_eq (carr A) (\fst ll) (\snd ll) →
1453    lset_eq_concrete A (\fst ll) (\snd ll).
1454#A #ll @(WF_ind ????? (filtered_lists_wf A ll))
1455* *
1456[ 1: #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hb2 >Hb2 #_ %2
1457| 2: #hd1 #tl1 #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hmem
1458     lapply (list_mem_split ??? Hmem) * #l2A * #l2B #Hb2 #Heq
1459     destruct
1460     lapply (Hind_wf 〈filter … (λx.¬x==hd1) tl1,filter … (λx.¬x==hd1) (l2A@l2B)〉)
1461     cut (filtered_lists A 〈filter A (λx:A.¬x==hd1) tl1,filter A (λx:A.¬x==hd1) (l2A@l2B)〉 〈hd1::tl1,l2A@[hd1]@l2B〉)
1462     [ @conj try @conj try @refl whd
1463       [ 1: /2 by /
1464       | 2: >filter_append in ⊢ (???%); >filter_append in ⊢ (???%);
1465            whd in match (filter ?? [hd1]);
1466            elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1467            normalize nodelta <filter_append @refl ] ]
1468     #Hfiltered #Hind_aux lapply (Hind_aux Hfiltered) -Hind_aux
1469     cut (lset_eq A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1470     [ 1: lapply (lset_eq_filter_monotonic … Heq hd1)
1471          >filter_cons_unfold >filter_append >(filter_append … [hd1])
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 #Hsol @Hsol ]
1475     #Hset_eq
1476     cut (head_shared A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1477     [ 1: lapply Hset_eq cases (filter A (λx:A.¬x==hd1) tl1)
1478          [ 1: whd in ⊢ (% → ?); * #_ elim (filter A (λx:A.¬x==hd1) (l2A@l2B)) //
1479               #hd' #tl' normalize #Hind * @False_ind
1480          | 2: #hd' #tl' * #Hincl1 #Hincl2 whd elim Hincl1 #Hsol #_ @Hsol ] ]
1481     #Hshared #Hind_aux lapply (Hind_aux Hshared Hset_eq)
1482     #Hconcrete_set_eq
1483     >cons_to_append
1484     @(transitive_lset_eq_concrete ? ([hd1]@tl1) ([hd1]@l2A@l2B) (l2A@[hd1]@l2B))
1485     [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete ]
1486     lapply (lset_eq_concrete_cons … Hconcrete_set_eq hd1) #Hconcrete_cons_eq
1487     @(square_lset_eq_concrete … Hconcrete_cons_eq)
1488     [ 1: @(lset_eq_concrete_filter ? tl1 hd1)
1489     | 2: @(lset_eq_concrete_filter ? (l2A@l2B) hd1) ]
1490] qed.
1491
1492lemma lset_eq_to_lset_eq_concrete : ∀A,l1,l2. lset_eq (carr A) l1 l2 → lset_eq_concrete A l1 l2.
1493#A *
1494[ 1: #l2 #Heq >(lset_eq_empty_inv … (symmetric_lset_eq … Heq)) //
1495| 2: #hd1 #tl1 #l2 #Hincl lapply Hincl lapply (lset_eq_to_lset_eq_concrete_aux ? 〈hd1::tl1,l2〉) #H @H
1496     whd elim Hincl * //
1497] qed.
1498
1499
1500(* The concrete one implies the abstract one. *)
1501lemma lset_eq_concrete_to_lset_eq : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq A l1 l2.
1502#A #l1 #l2 #Hconcrete
1503elim Hconcrete try //
1504#a #b #c #Hstep #Heq_bc_concrete #Heq_bc
1505cut (lset_eq A a b)
1506[ 1: elim Hstep
1507     [ 1: #a' elim a'
1508          [ 2: #hda #tla #Hind #x #b' #y #c' >cons_to_append
1509               >(associative_append ? [hda] tla ?)
1510               >(associative_append ? [hda] tla ?)
1511               @cons_monotonic_eq >nil_append >nil_append @Hind
1512          | 1: #x #b' #y #c' >nil_append >nil_append
1513               elim b' try //
1514               #hdb #tlc #Hind >append_cons >append_cons in ⊢ (???%);
1515               >associative_append >associative_append
1516               lapply (cons_monotonic_eq … Hind hdb) #Hind'               
1517               @(transitive_lset_eq ? ([x]@[hdb]@tlc@[y]@c') ([hdb]@[x]@tlc@[y]@c'))
1518               /2 by transitive_lset_eq/ ]
1519     | 2: #a' elim a'
1520          [ 2: #hda #tla #Hind #x #b' >cons_to_append
1521               >(associative_append ? [hda] tla ?)
1522               >(associative_append ? [hda] tla ?)
1523               @cons_monotonic_eq >nil_append >nil_append @Hind
1524          | 1: #x #b' >nil_append >nil_append @conj normalize
1525               [ 1: @conj [ 1: %1 @refl ] elim b'
1526                    [ 1: @I
1527                    | 2: #hdb #tlb #Hind normalize @conj
1528                         [ 1: %2 %2 %1 @refl
1529                         | 2: @(All_mp … Hind) #a0 *
1530                              [ 1: #Heq %1 @Heq
1531                              | 2: * /2 by or_introl, or_intror/ ] ] ]
1532                    #H %2 %2 %2 @H
1533               | 2: @conj try @conj try /2 by or_introl, or_intror/ elim b'
1534                    [ 1: @I
1535                    | 2: #hdb #tlb #Hind normalize @conj
1536                         [ 1: %2 %1 @refl
1537                         | 2: @(All_mp … Hind) #a0 *
1538                              [ 1: #Heq %1 @Heq
1539                              | 2: #H %2 %2 @H ] ] ] ] ]
1540     | 3: #a #x #b elim a try @lset_eq_contract
1541          #hda #tla #Hind @cons_monotonic_eq @Hind ] ]
1542#Heq_ab @(transitive_lset_eq … Heq_ab Heq_bc)
1543qed.
1544
1545lemma lset_eq_fold :
1546  ∀A : DeqSet.
1547  ∀acctype : Type[0].
1548  ∀eqrel : acctype → acctype → Prop.
1549  ∀refl_eqrel  : reflexive ? eqrel.
1550  ∀trans_eqrel : transitive ? eqrel.
1551  ∀sym_eqrel   : symmetric ? eqrel.
1552  ∀f:carr A → acctype → acctype.
1553  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1554  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1555  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1556  ∀l1,l2 : list (carr A).
1557  lset_eq A l1 l2 → 
1558  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1559#A #acctype #eqrel #refl_eqrel #trans_eqrel #sym_eqrel #f #Hinj #Hsym #Hcontract #l1 #l2 #Heq #acc
1560lapply (lset_eq_to_lset_eq_concrete … Heq) #Heq_concrete
1561@(lset_eq_concrete_fold_ext A acctype eqrel refl_eqrel trans_eqrel sym_eqrel f Hinj Hsym Hcontract l1 l2 Heq_concrete acc)
1562qed.
1563
1564(* Additional lemmas on lsets *)
1565
1566lemma lset_difference_empty :
1567  ∀A : DeqSet.
1568  ∀s1. lset_difference A s1 [ ] = s1.
1569#A #s1 elim s1 try //
1570#hd #tl #Hind >lset_difference_unfold >Hind @refl
1571qed.
1572
1573lemma lset_not_mem_difference :
1574  ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3).
1575#A #s1 #s2 #s3 #Hincl #x #Hmem
1576lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
1577elim s1 in Hincl Hmem;
1578[ 1: #_ *
1579| 2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall *
1580     [ 2: #Hmem_x_tl @Hind assumption
1581     | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]
1582] qed.
1583
1584lemma lset_mem_inclusion_mem :
1585  ∀A,s1,s2,elt.
1586  mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2.
1587#A #s1 elim s1
1588[ 1: #s2 #elt *
1589| 2: #hd #tl #Hind #s2 #elt *
1590     [ 1: #Heq destruct * //
1591     | 2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl;
1592          [ 1: #_ *
1593          | 2: #hd' #tl' #Hind * #Hmem' #Hall *
1594               [ 1: #Heq destruct @Hmem'
1595               | 2: #Hmem'' @Hind assumption ] ] ] ]
1596qed.
1597
1598lemma lset_remove_inclusion :
1599  ∀A : DeqSet. ∀s,elt.
1600    lset_inclusion A (lset_remove ? s elt) s.
1601#A #s elim s try // qed.
1602
1603lemma lset_difference_remove_inclusion :
1604  ∀A : DeqSet. ∀s1,s2,elt.
1605    lset_inclusion A
1606      (lset_difference ? (lset_remove ? s1 elt) s2) 
1607      (lset_difference ? s1 s2).
1608#A #s elim s try // qed.
1609
1610lemma lset_difference_permute :
1611  ∀A : DeqSet. ∀s1,s2,s3.
1612    lset_difference A s1 (s2 @ s3) =
1613    lset_difference A s1 (s3 @ s2).
1614#A #s1 #s2 elim s2 try //
1615#hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute
1616>Hind elim s3 try //
1617#hd' #tl' #Hind' >cons_to_append >associative_append
1618>associative_append >(cons_to_append … hd tl)
1619>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
1620>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
1621<Hind' generalize in match (lset_difference ???); #foo
1622whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
1623whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
1624elim foo
1625[ 1: normalize @refl
1626| 2: #hd'' #tl'' #Hind normalize
1627      @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with
1628        [ true ⇒ λH. ?
1629        | false ⇒ λH. ?
1630        ] (refl ? (hd''==hd')))
1631      @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with
1632        [ true ⇒ λH'. ?
1633        | false ⇒ λH'. ?
1634        ] (refl ? (hd''==hd)))
1635      normalize nodelta
1636      try @Hind
1637[ 1: normalize >H normalize nodelta @Hind
1638| 2: normalize >H' normalize nodelta @Hind
1639| 3: normalize >H >H' normalize nodelta >Hind @refl
1640] qed.
1641
1642
1643
1644lemma lset_disjoint_dec :
1645  ∀A : DeqSet.
1646  ∀s1,elt,s2.
1647  mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1).
1648#A #s1 #elt #s2
1649@(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ?
1650  with
1651  [ false ⇒ λHA. ?
1652  | true ⇒ λHA. ? ] (refl ? (elt ∈ s1)))
1653[ 1: lapply (memb_to_mem … HA) #Hmem
1654     %1 @Hmem
1655| 2: %2 elim s1 in HA;
1656     [ 1: #_ whd %1 @refl
1657     | 2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?);
1658          >lset_difference_unfold
1659          >lset_difference_unfold2
1660          lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %);
1661          cases (elt==hd1) normalize nodelta
1662          [ 1: #_ #Habsurd destruct
1663          | 2: #HA #HB >HB normalize nodelta %1 @refl ] ] ]
1664qed.
1665
1666lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2.
1667  mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l.
1668#A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/
1669qed.
1670
1671lemma lset_inclusion_difference_aux :
1672  ∀A : DeqSet. ∀s1,s2.
1673  lset_inclusion A s1 s2 →
1674  (lset_eq A s2 (s1@lset_difference A s2 s1)).
1675#A #s1
1676@(WF_ind ????? (filtered_list_wf A s1))
1677*
1678[ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq
1679| 2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl
1680     lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?)
1681     [ 1: whd normalize
1682          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ]
1683     #Hind_wf     
1684     elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq
1685     >cons_to_append in ⊢ (???%); >associative_append
1686     >lset_difference_unfold2
1687     >nil_append
1688     >lset_remove_split >lset_remove_split
1689     normalize in match (lset_remove ? [hd1] hd1);
1690     >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
1691     >nil_append <lset_remove_split >lset_difference_lset_remove_commute
1692     lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?)
1693     [ 1: lapply (lset_inclusion_remove … Hincl hd1)
1694          >Heq @lset_inclusion_eq2
1695          >lset_remove_split >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 @reflexive_lset_eq ]
1699     #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind
1700     @lset_eq_concrete_to_lset_eq
1701     lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc
1702     @(square_lset_eq_concrete ????? Hindc) -Hindc -Hind
1703     [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B))
1704          [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete
1705          | 1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ]
1706     | 2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …))
1707          elim (s2A@s2B)
1708          [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq
1709          | 2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold
1710               @(match (hd2∈filter A (λx:A.¬x==hd1) tl1)
1711                 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ?
1712                 with
1713                 [ false ⇒ λH. ?
1714                 | true ⇒ λH. ?
1715                 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta
1716               [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter))
1717                    normalize nodelta @Hind
1718               | 2: @(match (hd2∈tl1)
1719                      return λx. ((hd2∈tl1) = x) → ?
1720                      with
1721                      [ false ⇒ λH'. ?
1722                      | true ⇒ λH'. ?
1723                      ] (refl ? (hd2∈tl1))) normalize nodelta
1724                      [ 1: (* We have hd2 = hd1 *)
1725                            cut (hd2 = hd1)
1726                            [ elim tl1 in H H';
1727                              [ 1: normalize #_ #Habsurd destruct (Habsurd)
1728                              | 2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?);
1729                                    lapply (eqb_true ? hdtl1 hd1)
1730                                    cases (hdtl1==hd1) normalize nodelta
1731                                    [ 1: * #H >(H (refl ??)) #_
1732                                         lapply (eqb_true ? hd2 hd1)
1733                                         cases (hd2==hd1) normalize nodelta *
1734                                         [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl
1735                                         | 2: #_ #_ @Hind ]
1736                                    | 2: #_ normalize lapply (eqb_true ? hd2 hdtl1)
1737                                         cases (hd2 == hdtl1) normalize nodelta *
1738                                         [ 1: #_ #_ #Habsurd destruct (Habsurd)
1739                                         | 2: #_ #_ @Hind ] ] ] ]
1740                           #Heq_hd2hd1 destruct (Heq_hd2hd1)
1741                           @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind)
1742                           #Hind' @(square_lset_eq_concrete … Hind')
1743                           [ 2: @lset_refl
1744                           | 1: >cons_to_append >cons_to_append in ⊢ (???%);
1745                                @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
1746                                [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract
1747                                | 2: >(cons_to_append … hd1 (lset_difference ???))
1748                                     @lset_eq_concrete_cons >nil_append >nil_append
1749                                     @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ]
1750                        | 2: @(match hd2 == hd1
1751                               return λx. ((hd2 == hd1) = x) → ?
1752                               with
1753                               [ true ⇒ λH''. ?
1754                               | false ⇒ λH''. ?
1755                               ] (refl ? (hd2 == hd1)))
1756                             [ 1: whd in match (lset_remove ???) in ⊢ (???%);
1757                                  >H'' normalize nodelta >((proj1 … (eqb_true …)) H'')
1758                                  @(transitive_lset_eq … Hind)
1759                                  @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
1760                                  [ 2: @lset_eq_contract ]                                                                   
1761                                  @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons                                 
1762                                  @switch_lset_eq_concrete
1763                             | 2: whd in match (lset_remove ???) in ⊢ (???%);
1764                                  >H'' >notb_false normalize nodelta
1765                                  @lset_eq_concrete_to_lset_eq
1766                                  lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc
1767                                  lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' -Hindc
1768                                  @(square_lset_eq_concrete … Hindc')
1769                                  [ 1: @symmetric_lset_eq_concrete
1770                                       >cons_to_append >cons_to_append in ⊢ (???%);
1771                                       >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%);
1772                                       @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
1773                                  | 2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
1774                                  ]
1775                              ]
1776                        ]
1777                    ]
1778             ]
1779      ]
1780] qed.             
1781                                                       
1782lemma lset_inclusion_difference :
1783  ∀A : DeqSet.
1784  ∀s1,s2 : lset (carr A).
1785    lset_inclusion ? s1 s2 →
1786    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
1787          lset_disjoint ? s1 s2' ∧
1788          lset_eq ? s2' (lset_difference ? s2 s1).
1789#A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj
1790[ 1: @lset_inclusion_difference_aux @Hincl
1791| 2: /2 by lset_difference_disjoint/
1792| 3,4: @reflexive_lset_inclusion ]
1793qed.
1794
1795(* --------------------------------------------------------------------------- *)
1796(* Stuff on bitvectors, previously in memoryInjections.ma *)
1797(* --------------------------------------------------------------------------- *)
1798(* --------------------------------------------------------------------------- *)   
1799(* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
1800(* --------------------------------------------------------------------------- *)
1801 
1802lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
1803#n #bv whd in match (add_with_carries ????); elim bv //
1804#n #hd #tl #Hind whd in match (fold_right2_i ????????);
1805>Hind normalize
1806cases n in tl;
1807[ 1: #tl cases hd normalize @refl
1808| 2: #n' #tl cases hd normalize @refl ]
1809qed.
1810
1811lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
1812#n #bv whd in match (addition_n ???);
1813>add_with_carries_n_O //
1814qed.
1815
1816lemma replicate_Sn : ∀A,sz,elt.
1817  replicate A (S sz) elt = elt ::: (replicate A sz elt).
1818// qed.
1819
1820lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
1821
1822lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
1823#n #xa #a normalize @refl qed.
1824
1825(* useful facts on carry_of *)
1826lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
1827lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
1828lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
1829lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
1830lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
1831
1832
1833
1834definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
1835
1836lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
1837    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
1838    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
1839#n elim n
1840[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
1841     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
1842     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
1843     normalize #Heq destruct (Heq) @refl
1844| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
1845     destruct #Hind >add_with_carries_Sn >replicate_Sn
1846     whd in match (zero ?) in Hind; lapply Hind
1847     elim (add_with_carries (S (S n'))
1848            (false:::replicate bool (S n') false)
1849            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
1850            normalize >add_with_carries_Sn in Hind;
1851     elim (add_with_carries (S n') (replicate bool (S n') false)
1852                    (replicate bool (S n') false) true) #flags' #bits'
1853     normalize
1854     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
1855            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
1856     normalize #Heq destruct @refl
1857] qed.     
1858
1859lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
1860#n lapply (one_bv_Sn_aux n)
1861whd in match (one_bv ?) in ⊢ (? → (??%%));
1862elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
1863#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
1864qed.
1865
1866lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
1867    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
1868#n   
1869elim n
1870[ 1: #a >(BitVector_O … a) normalize @refl
1871| 2: #n' cases n'
1872     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
1873          >(BitVector_O … tl) normalize cases xa @refl
1874     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
1875          >one_bv_Sn >zero_Sn
1876          lapply (Hind tl)
1877          >add_with_carries_Sn >add_with_carries_Sn
1878          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
1879          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
1880          normalize nodelta @refl
1881] qed.         
1882
1883(* In order to use associativity on increment, we hide it under addition_n. *)
1884lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
1885#n
1886whd in match (increment ??) in ⊢ (∀_.??%?);
1887whd in match (addition_n ???) in ⊢ (∀_.???%);
1888#a lapply (increment_to_addition_n_aux n a)
1889#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
1890qed.
1891
1892(* Explicit formulation of addition *)
1893
1894(* Explicit formulation of the last carry bit *)
1895let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
1896match n return λx. BitVector x → BitVector x → bool with
1897[ O ⇒ λ_,_. init
1898| S x ⇒ λa',b'.
1899  let hd_a ≝ head' … a' in
1900  let hd_b ≝ head' … b' in
1901  let tl_a ≝ tail … a' in
1902  let tl_b ≝ tail … b' in
1903  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
1904] a b.
1905
1906lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
1907  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
1908#n #init #a #b @refl qed.
1909
1910lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
1911  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
1912
1913(* correction of [ith_carry] *)
1914lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
1915  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
1916  head' … flags_ab = ith_carry ? a b init.
1917#n elim n
1918[ 1: #init #a #b #res_ab #flags_ab
1919     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1920     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1921     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1922     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1923     destruct
1924     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
1925     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
1926     @refl
1927| 2: #n' #Hind #init #a #b #res_ab #flags_ab
1928     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1929     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1930     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1931     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1932     destruct
1933     lapply (Hind … init tl_a tl_b tl_res tl_flags)
1934     >add_with_carries_Sn >(ith_carry_Sn (S n'))
1935     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
1936     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
1937     normalize nodelta cases hd_flags_ab normalize nodelta
1938     whd in match (head' ? (S n') ?); #H1 #H2
1939     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
1940] qed.
1941
1942(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
1943definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
1944match n return λx. BitVector x → BitVector x → bool with
1945[ O ⇒ λ_,_. init
1946| S x ⇒ λa',b'.
1947  let hd_a ≝ head' … a' in
1948  let hd_b ≝ head' … b' in
1949  let tl_a ≝ tail … a' in
1950  let tl_b ≝ tail … b' in
1951  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
1952] a b.
1953
1954lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
1955  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
1956#n #a #b // qed.
1957
1958lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
1959  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
1960
1961(* correction of ith_bit *)
1962lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
1963  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
1964  head' … res_ab = ith_bit ? a b init.
1965#n
1966cases n
1967[ 1: #init #a #b #res_ab #flags_ab
1968     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1969     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1970     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1971     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1972     destruct
1973     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
1974     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
1975     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
1976| 2: #n' #init #a #b #res_ab #flags_ab
1977     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
1978     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
1979     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
1980     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
1981     destruct
1982     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
1983     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
1984     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
1985     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
1986     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
1987     <(H1 (refl ??)) @refl
1988] qed.
1989
1990(* Transform a function from bit-vectors to bits into a vector by folding *)
1991let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
1992match v with
1993[ VEmpty ⇒ VEmpty ?
1994| VCons sz elt tl ⇒
1995  let bit ≝ f ? v in
1996  bit ::: (bitvector_fold ? tl f)
1997].
1998
1999(* Two-arguments version *)
2000let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
2001match v1  with
2002[ VEmpty ⇒ λ_. VEmpty ?
2003| VCons sz elt tl ⇒ λv2'.
2004  let bit ≝ f ? v1 v2 in
2005  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
2006] v2.
2007
2008lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
2009  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
2010
2011(* These functions pack all the relevant information (including carries) directly. *)
2012definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
2013
2014lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
2015  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
2016 
2017lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
2018
2019(* Prove the equivalence of addition_n_direct with add_with_carries *)
2020lemma addition_n_direct_ok : ∀n,carry,v1,v2.
2021  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
2022#n elim n
2023[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
2024| 2: #n' #Hind #carry #v1 #v2
2025     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
2026     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
2027     lapply (Hind carry tl1 tl2)
2028     lapply (ith_bit_ok ? carry v1 v2)
2029     lapply (ith_carry_ok ? carry v1 v2)
2030     destruct
2031     #Hind >addition_n_direct_Sn
2032     >ith_bit_Sn >add_with_carries_Sn
2033     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
2034     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
2035            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
2036     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
2037     whd in match head'; normalize nodelta
2038     #H1 #H2 >H1 >H2 @refl
2039] qed.
2040
2041lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
2042  (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
2043#n #carry #v1 #v2 <addition_n_direct_ok
2044cases (add_with_carries ????) //
2045qed.
2046 
2047(* trivially lift associativity to our new setting *)     
2048lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
2049  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
2050  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
2051#n #carry1 #carry2 #v1 #v2 #v3
2052<addition_n_direct_ok <addition_n_direct_ok
2053<addition_n_direct_ok <addition_n_direct_ok
2054lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
2055elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
2056elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
2057#H @(sym_eq … H)
2058qed.
2059
2060lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
2061  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
2062#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
2063qed.
2064
2065definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
2066definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
2067
2068
2069(* fold andb on a bitvector. *)
2070let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
2071match b with
2072[ VEmpty ⇒ true
2073| VCons sz elt tl ⇒
2074  andb elt (andb_fold ? tl)
2075].
2076
2077lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
2078
2079lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
2080#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
2081qed.
2082
2083lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
2084  ith_carry … a (one_bv ?) false = andb_fold … a.
2085#n elim n
2086[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
2087     cases hd normalize @refl
2088| 2: #n' #Hind #a
2089     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
2090     lapply (Hind … tl) #Hind >one_bv_Sn
2091     >ith_carry_Sn whd in match (andb_fold ??);
2092     cases hd >Hind @refl
2093] qed.
2094
2095lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
2096  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
2097#n #a
2098elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
2099whd in match (head' ???);
2100-a cases n in tl;
2101[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
2102| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
2103     >ith_increment_carry >tail_Sn
2104     cases hd try //
2105] qed.
2106
2107(* Lemma used to prove involutivity of two-complement negation *)
2108lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
2109   (andb_fold (S n) (negation_bv (S n) v) =
2110    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
2111#n elim n
2112[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
2113| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2114     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
2115     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
2116     cases hd normalize nodelta
2117     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
2118     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
2119     >ith_increment_carry
2120     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
2121] qed.
2122   
2123(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
2124lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
2125#n elim n
2126[ 1: #v >(BitVector_O v) @refl
2127| 2: #n' cases n'
2128     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2129          >(BitVector_O … tl) normalize cases hd @refl
2130     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2131          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
2132          whd in match twocomp_neg_direct; normalize nodelta
2133          whd in match increment_direct; normalize nodelta
2134          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
2135          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
2136          generalize in match (addition_n_direct (S n'')
2137                                                   (negation_bv (S n'')
2138                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
2139                                                   (one_bv (S n'')) false); #tail
2140          >ith_increment_carry >ith_increment_carry
2141          cases hd normalize nodelta
2142          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
2143          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
2144          <twocomp_neg_involutive_aux
2145          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
2146      ]
2147] qed.
2148
2149lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
2150#n #a #b #va #vb #H destruct (H) @conj @refl qed.
2151
2152lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
2153
2154(* Injectivity of increment *)
2155lemma increment_inj : ∀n. ∀a,b : BitVector n.
2156  increment_direct ? a = increment_direct ? b →
2157  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
2158#n whd in match increment_direct; normalize nodelta elim n
2159[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
2160| 2: #n' cases n'
2161   [ 1: #_ #a #b
2162        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
2163        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
2164        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
2165        normalize #H @conj try //
2166   | 2: #n'' #Hind #a #b
2167        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
2168        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
2169        lapply (Hind … tl_a tl_b) -Hind #Hind
2170        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
2171        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
2172        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
2173        lapply (Hind Heq2) * #Heq3 #Heq4
2174        cut (hd_a = hd_b)
2175        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
2176             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
2177             @refl ]
2178        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
2179        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
2180] qed.
2181
2182(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
2183lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
2184  a = b → increment_direct ? a = increment_direct ? b. // qed.
2185
2186(* A more general result. *)
2187lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
2188  addition_n_direct ? x delta false = addition_n_direct ? y delta false →
2189  x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
2190#n elim n
2191[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
2192| 2: #n' #Hind #x #y #delta
2193     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
2194     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
2195     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
2196     >addition_n_direct_Sn >ith_bit_Sn
2197     >addition_n_direct_Sn >ith_bit_Sn
2198     >ith_carry_Sn >ith_carry_Sn
2199     lapply (Hind … tlx tly tld) -Hind #Hind #Heq
2200     elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
2201     lapply (Hind Heq_tl) -Hind * #HindA #HindB
2202     >HindA >HindB >HindB in Heq_hd; #Heq_hd
2203     cut (hdx = hdy)
2204     [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
2205          cases hdx cases hdy normalize #H try @H try @refl
2206          >H try @refl ]
2207     #Heq_hd >Heq_hd @conj @refl
2208] qed.
2209
2210(* We also need it the other way around. *)
2211lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
2212  x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
2213   addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
2214#n elim n
2215[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
2216| 2: #n' #Hind #x #y #delta
2217     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
2218     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
2219     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
2220     #Hneq
2221     cut (hdx ≠ hdy ∨ tlx ≠ tly)
2222     [ @(eq_bv_elim … tlx tly)
2223       [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
2224         #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
2225                                 #H @H @refl ]
2226         #H %1 @H
2227       | #H %2 @H ] ]
2228     -Hneq #Hneq
2229     >addition_n_direct_Sn >addition_n_direct_Sn
2230     >ith_bit_Sn >ith_bit_Sn cases Hneq
2231     [ 1: #Hneq_hd
2232          lapply (addition_n_direct_inj … tlx tly tld)         
2233          @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
2234          [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
2235               % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
2236               lapply Hneq_hd
2237               cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
2238               normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
2239               try @(absurd … Heq_hd Hneq_hd)
2240               elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
2241               try @refl try assumption try @(sym_eq … Heq_hd)
2242          | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
2243               elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
2244     | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
2245          % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
2246          elim Hind -Hind #HA #HB @HA @HB ]
2247] qed.
2248
2249lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
2250
2251lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
2252   ith_carry (S n) a (one_bv (S n)) false
2253   = ith_carry (S n) a (zero (S n)) true.
2254#n elim n
2255[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
2256| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
2257     lapply (Hind tl_a) #Hind
2258     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
2259] qed.
2260
2261lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
2262#n elim n //
2263#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
2264>ith_carry_Sn >(Hind tl) cases hd @refl.
2265qed.
2266
2267lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
2268  addition_n_direct ? v (zero ?) false = v.
2269#n elim n
2270[ 1: #v >(BitVector_O … v) normalize @refl
2271| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
2272     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
2273     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
2274     >xorb_false @refl
2275] qed.
2276
2277lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
2278#n elim n
2279[ 1: #a >(BitVector_O … a) normalize @refl
2280| 2: #n' cases n'
2281     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
2282     | 2: #n'' #Hind #a
2283          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
2284          lapply (Hind tl_a) -Hind #Hind
2285          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
2286          >addition_n_direct_Sn >ith_bit_Sn
2287          >xorb_false >Hind @bitvector_cons_eq
2288          >increment_to_carry_aux @refl
2289     ]
2290] qed.
2291
2292lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
2293  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
2294#n #a #b >increment_to_carry_zero <associative_addition_n_direct
2295>neutral_addition_n_direct @refl
2296qed.
2297
2298lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
2299#n #v whd in match (increment ??);
2300>addition_n_direct_ok <increment_to_carry_zero @refl
2301qed.
2302
2303(* Prove -(a + b) = -a + -b *)
2304lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
2305  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
2306whd in match twocomp_neg_direct; normalize nodelta
2307lapply increment_inj_inv
2308whd in match increment_direct; normalize nodelta
2309#H #n #a #b
2310<associative_addition_n_direct @H
2311>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
2312>increment_to_carry
2313-H lapply b lapply a -b -a
2314cases n
2315[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
2316| 2: #n' #a #b
2317     cut (negation_bv ? (addition_n_direct ? a b false)
2318           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
2319          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
2320     [ -n lapply b lapply a elim n'
2321     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
2322          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
2323          cases hd_a cases hd_b normalize @conj @refl
2324     | 2: #n #Hind #a #b
2325          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
2326          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
2327          lapply (Hind tl_a tl_b) * #H1 #H2
2328          @conj
2329          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
2330               >carry_notb >H2 @refl
2331          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
2332               >negation_bv_Sn >negation_bv_Sn
2333               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
2334               >xorb_lneg >xorb_rneg >notb_notb
2335               <xorb_rneg >H2 @refl
2336          ]
2337      ] ]
2338      * #H1 #H2 @H1
2339] qed.
2340
2341lemma addition_n_direct_neg : ∀n. ∀a.
2342 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
2343 ∧ (ith_carry n a (negation_bv n a) false = false).
2344#n elim n
2345[ 1: #a >(BitVector_O … a) @conj @refl
2346| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
2347     lapply (Hind … tl) -Hind * #HA #HB
2348     @conj
2349     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
2350     | 1: >negation_bv_Sn >addition_n_direct_Sn
2351          >ith_bit_Sn >HB >xorb_false >HA
2352          @bitvector_cons_eq elim hd @refl
2353     ]
2354] qed.
2355
2356(* -a + a = 0 *)
2357lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
2358whd in match twocomp_neg_direct;
2359whd in match increment_direct;
2360normalize nodelta
2361#n #a <associative_addition_n_direct
2362elim (addition_n_direct_neg … a) #H #_ >H
2363-H -a
2364cases n try //
2365#n'
2366cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
2367       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
2368[ elim n'
2369     [ 1: @conj @refl
2370     | 2: #n' * #HA #HB @conj
2371          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
2372               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
2373          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
2374     ]
2375] * #H1 #H2 @H1
2376qed.
2377
2378(* Lift back the previous result to standard operations. *)
2379lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
2380#n #v whd in match twocomp_neg_direct; normalize nodelta
2381whd in match increment_direct; normalize nodelta
2382whd in match two_complement_negation; normalize nodelta
2383>increment_to_addition_n <addition_n_direct_ok
2384whd in match addition_n; normalize nodelta
2385elim (add_with_carries ????) #a #b @refl
2386qed.
2387
2388lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
2389  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
2390#n #a #b
2391lapply (twocomp_neg_plus ? a b)
2392>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
2393<addition_n_direct_ok <addition_n_direct_ok
2394whd in match addition_n; normalize nodelta
2395elim (add_with_carries n a b false) #bits #flags normalize nodelta
2396elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
2397normalize nodelta #H @H
2398qed.
2399
2400lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
2401#n #a lapply (bitvector_opp_direct ? a)
2402>twocomp_neg_direct_ok <addition_n_direct_ok
2403whd in match (addition_n ???);
2404elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
2405qed.
2406
2407lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
2408#n #a
2409lapply (neutral_addition_n_direct n a)
2410<addition_n_direct_ok
2411whd in match (addition_n ???);
2412elim (add_with_carries n a (zero n) false) #bits #flags #H @H
2413qed.
2414
2415lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
2416  addition_n ? x delta = addition_n ? y delta → x = y. 
2417#n #x #y #delta 
2418lapply (addition_n_direct_inj … x y delta)
2419<addition_n_direct_ok <addition_n_direct_ok
2420whd in match addition_n; normalize nodelta
2421elim (add_with_carries n x delta false) #bitsx #flagsx
2422elim (add_with_carries n y delta false) #bitsy #flagsy
2423normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
2424qed.
2425
2426lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
2427  x ≠ y → addition_n ? x delta ≠ addition_n ? y delta. 
2428#n #x #y #delta 
2429lapply (addition_n_direct_inj_inv … x y delta)
2430<addition_n_direct_ok <addition_n_direct_ok
2431whd in match addition_n; normalize nodelta
2432elim (add_with_carries n x delta false) #bitsx #flagsx
2433elim (add_with_carries n y delta false) #bitsy #flagsy
2434normalize #H1 #H2 @(H1 H2)
2435qed.
2436
Note: See TracBrowser for help on using the repository browser.