source: src/Clight/frontend_misc.ma @ 2448

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

Comitting current state of switch removal.

File size: 61.4 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(* Misc. *)
15(* --------------------------------------------------------------------------- *)
16
17lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
18* normalize //
19qed.
20
21lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
22* normalize //
23qed.
24
25lemma type_eq_identity : ∀t. type_eq t t = true.
26#t normalize elim (type_eq_dec t t)
27[ 1: #Heq normalize //
28| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.
29
30lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
31#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
32[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
33| 2: #Hneq' normalize // ] qed.
34
35lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
36
37lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
38
39lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
40#A #B #a #b * #a' #b' #H destruct @refl
41qed.
42
43lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
44#A #B #a #b * #a' #b' #H destruct @refl
45qed.
46
47lemma bindIO_Error : ∀err,f. bindIO io_out io_in (val×trace) (trace×state) (Error … err) f = Wrong io_out io_in (trace×state) err.
48// qed.
49
50lemma bindIO_Value : ∀v,f. bindIO io_out io_in (val×trace) (trace×state) (Value … v) f = (f v).
51// qed.
52
53lemma bindIO_elim :
54         ∀A.
55         ∀P : (IO io_out io_in A) → Prop.
56         ∀e : res A. (*IO io_out io_in A.*)
57         ∀f.
58         (∀v. (e:IO io_out io_in A) = OK … v →  P (f v)) →
59         (∀err. (e:IO io_out io_in A) = Error … err →  P (Wrong ??? err)) →
60         P (bindIO io_out io_in ? A (e:IO io_out io_in A) f).
61#A #P * try /2/ qed.
62
63lemma opt_to_io_Value :
64  ∀A,B,C,err,x,res. opt_to_io A B C err x = return res → x = Some ? res.
65#A #B #C #err #x cases x normalize
66[ 1: #res #Habsurd destruct
67| 2: #c #res #Heq destruct @refl ]
68qed. 
69
70lemma some_inversion :
71  ∀A,B:Type[0].
72  ∀e:option A.
73  ∀res:B.
74  ∀f:A → option B.
75 match e with
76 [ None ⇒ None ?
77 | Some x ⇒ f x ] = Some ? res →
78 ∃x. e = Some ? x ∧ f x = Some ? res.
79 #A #B #e #res #f cases e normalize nodelta
80[ 1: #Habsurd destruct (Habsurd)
81| 2: #a #Heq %{a} @conj >Heq @refl ]
82qed.
83
84lemma cons_inversion :
85  ∀A,B:Type[0].
86  ∀e:list A.
87  ∀res:B.
88  ∀f:A → list A → option B.
89 match e with
90 [ nil ⇒ None ?
91 | cons hd tl ⇒ f hd tl ] = Some ? res →
92 ∃hd,tl. e = hd::tl ∧ f hd tl = Some ? res.
93#A #B #e #res #f cases e normalize nodelta
94[ 1: #Habsurd destruct (Habsurd)
95| 2: #hd #tl #Heq %{hd} %{tl} @conj >Heq @refl ]
96qed.
97
98lemma if_opt_inversion :
99  ∀A:Type[0].
100  ∀x.
101  ∀y:A.
102  ∀e:bool.
103 (if e then
104    x
105  else
106    None ?) = Some ? y →
107 e = true ∧ x = Some ? y.
108#A #x #y * normalize
109#H destruct @conj @refl
110qed.
111
112lemma andb_inversion :
113  ∀a,b : bool. andb a b = true → a = true ∧ b = true.
114* * normalize /2 by conj, refl/ qed. 
115
116lemma identifier_eq_i_i : ∀tag,i. ∃pf. identifier_eq tag i i = inl … pf.
117#tag #i cases (identifier_eq ? i i)
118[ 1: #H %{H} @refl
119| 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ]
120qed.
121
122(* --------------------------------------------------------------------------- *)
123(* Useful facts on various boolean operations. *)
124(* --------------------------------------------------------------------------- *)
125 
126lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
127lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
128lemma andb_comm : ∀x,y. andb x y = andb y x. // qed.
129lemma notb_true : notb true = false. // qed.
130lemma notb_false : notb false = true. % #H destruct qed.
131lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
132
133(* --------------------------------------------------------------------------- *)
134(* Useful facts on Z. *)
135(* --------------------------------------------------------------------------- *)
136
137lemma Zltb_to_Zleb_true : ∀a,b. Zltb a b = true → Zleb a b = true.
138#a #b #Hltb lapply (Zltb_true_to_Zlt … Hltb) #Hlt @Zle_to_Zleb_true
139/3 by Zlt_to_Zle, transitive_Zle/ qed.
140
141lemma Zle_to_Zle_to_eq : ∀a,b. Zle a b → Zle b a → a = b.
142#a #b elim b
143[ 1: elim a // #a' normalize [ 1: @False_ind | 2: #_ @False_ind ] ]
144#b' elim a normalize
145[ 1: #_ @False_ind
146| 2: #a' #H1 #H2 >(le_to_le_to_eq … H1 H2) @refl
147| 3: #a' #_ @False_ind
148| 4: @False_ind
149| 5: #a' @False_ind
150| 6: #a' #H2 #H1 >(le_to_le_to_eq … H1 H2) @refl
151] qed.
152
153lemma Zleb_true_to_Zleb_true_to_eq : ∀a,b. (Zleb a b = true) → (Zleb b a = true) → a = b.
154#a #b #H1 #H2
155/3 by Zle_to_Zle_to_eq, Zleb_true_to_Zle/
156qed.
157
158lemma Zltb_dec : ∀a,b. (Zltb a b = true) ∨ (Zltb a b = false ∧ Zleb b a = true).
159#a #b
160lapply (Z_compare_to_Prop … a b)
161cases a
162[ 1: | 2,3: #a' ]
163cases b
164whd in match (Z_compare OZ OZ); normalize nodelta
165[ 2,3,5,6,8,9: #b' ]
166whd in match (Zleb ? ?);
167try /3 by or_introl, or_intror, conj, I, refl/
168whd in match (Zltb ??);
169whd in match (Zleb ??); #_
170[ 1: cases (decidable_le (succ a') b')
171     [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption
172     | 2:  #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2  @conj try @le_to_leb_true
173           /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ]
174| 2: cases (decidable_le (succ b') a')
175     [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption
176     | 2:  #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2  @conj try @le_to_leb_true
177           /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ]
178] qed.
179
180lemma Zleb_unsigned_OZ : ∀bv. Zleb OZ (Z_of_unsigned_bitvector 16 bv) = true.
181#bv elim bv try // #n' * #tl normalize /2/ qed.
182
183lemma Zltb_unsigned_OZ : ∀bv. Zltb (Z_of_unsigned_bitvector 16 bv) OZ = false.
184#bv elim bv try // #n' * #tl normalize /2/ qed.
185
186lemma Z_of_unsigned_not_neg : ∀bv.
187  (Z_of_unsigned_bitvector 16 bv = OZ) ∨ (∃p. Z_of_unsigned_bitvector 16 bv = pos p).
188#bv elim bv
189[ 1: normalize %1 @refl
190| 2: #n #hd #tl #Hind cases hd
191     [ 1: normalize %2 /2 by ex_intro/
192     | 2: cases Hind normalize [ 1: #H %1 @H | 2: * #p #H >H %2 %{p} @refl ]
193     ]
194] qed.
195
196lemma free_not_in_bounds : ∀x. if Zleb (pos one) x
197                                then Zltb x OZ 
198                                else false = false.
199#x lapply (Zltb_to_Zleb_true x OZ)
200elim (Zltb_dec … x OZ)
201[ 1: #Hlt >Hlt #H lapply (H (refl ??)) elim x
202     [ 2,3: #x' ] normalize in ⊢ (% → ?);
203     [ 1: #Habsurd destruct (Habsurd)
204     | 2,3: #_ @refl ]
205| 2: * #Hlt #Hle #_ >Hlt cases (Zleb (pos one) x) @refl ]
206qed.
207
208lemma free_not_valid : ∀x. if Zleb (pos one) x
209                            then Zltb x OZ 
210                            else false = false.
211#x
212cut (Zle (pos one) x ∧ Zlt x OZ → False)
213[ * #H1 #H2 lapply (transitive_Zle … (monotonic_Zle_Zsucc … H1) (Zlt_to_Zle … H2)) #H @H ] #Hguard
214cut (Zleb (pos one) x = true ∧ Zltb x OZ = true → False)
215[ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ @Zltb_true_to_Zlt assumption ]
216cases (Zleb (pos one) x) cases (Zltb x OZ)
217/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
218qed.
219
220(* follows from (0 ≤ a < b → mod a b = a) *)
221axiom Z_of_unsigned_bitvector_of_small_Z :
222  ∀z. OZ ≤ z → z < Z_two_power_nat 16 → Z_of_unsigned_bitvector 16 (bitvector_of_Z 16 z) = z.
223
224theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p.
225#n #m #p #Hle #Hlt /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle, transitive_Zle/
226qed.
227
228(* --------------------------------------------------------------------------- *)
229(* Useful facts on blocks. *)
230(* --------------------------------------------------------------------------- *)
231
232lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
233#b1 #b2 #Hneq
234@(eq_block_elim … b1 b2)
235[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
236| 2: #_ @refl ] qed.
237
238lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false.
239#b1 #b2 #Hneq
240@(eq_block_elim … b1 b2)
241[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
242| 2: #_ @refl ] qed.
243
244definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_block ?.
245* #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2)
246[ 1: #Heq >Heq cases r1 cases r2 normalize
247     >eqZb_z_z normalize try // @conj #H destruct (H)
248     try @refl
249| 2: #Hneq cases r1 cases r2 normalize
250     >(eqZb_false … Hneq) normalize @conj
251     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
252] qed.
253
254(* --------------------------------------------------------------------------- *)
255(* General results on lists. *)
256(* --------------------------------------------------------------------------- *)
257
258(* If mem succeeds in finding an element, then the list can be partitioned around this element. *)
259lemma list_mem_split : ∀A. ∀l : list A. ∀x : A. mem … x l → ∃l1,l2. l = l1 @ [x] @ l2.
260#A #l elim l
261[ 1: normalize #x @False_ind
262| 2: #hd #tl #Hind #x whd in ⊢ (% → ?); *
263     [ 1: #Heq %{(nil ?)} %{tl} destruct @refl
264     | 2: #Hmem lapply (Hind … Hmem) * #l1 * #l2 #Heq_tl >Heq_tl
265          %{(hd :: l1)} %{l2} @refl
266     ]
267] qed.
268
269lemma cons_to_append : ∀A. ∀hd : A. ∀l : list A. hd :: l = [hd] @ l. #A #hd #l @refl qed.
270
271lemma fold_append :
272  ∀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.
273#A #B #l1 elim l1 //
274#hd #tl #Hind #l2 #f #seed normalize >Hind @refl
275qed.
276
277lemma filter_append : ∀A:Type[0]. ∀l1,l2 : list A. ∀f. filter ? f (l1 @ l2) = (filter ? f l1) @ (filter ? f l2).
278#A #l1 elim l1 //
279#hd #tl #Hind #l2 #f
280>cons_to_append >associative_append
281normalize cases (f hd) normalize
282<Hind @refl
283qed.
284
285lemma filter_cons_unfold : ∀A:Type[0]. ∀f. ∀hd,tl.
286  filter ? f (hd :: tl) =
287  if f hd then
288    (hd :: filter A f tl)
289  else
290    (filter A f tl).
291#A #f #hd #tl elim tl // qed.
292
293
294lemma filter_elt_empty : ∀A:DeqSet. ∀elt,l. filter (carr A) (λx.¬(x==elt)) l = [ ] → All (carr A) (λx. x = elt) l.
295#A #elt #l elim l
296[ 1: //
297| 2: #hd #tl #Hind >filter_cons_unfold
298     lapply (eqb_true A hd elt)
299     cases (hd==elt) normalize nodelta
300     [ 2: #_ #Habsurd destruct
301     | 1: * #H1 #H2 #Heq lapply (Hind Heq) #Hall whd @conj //
302          @H1 @refl
303     ]
304] qed.
305
306lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed.
307
308alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
309
310lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2).
311#A #elt #l1 elim l1
312[ 1: #l2 normalize @conj [ 1: #H %2 @H | 2: * [ 1: @False_ind | 2: #H @H ] ]
313| 2: #hd #tl #Hind #l2 @conj
314     [ 1: whd in match (meml ???); *
315          [ 1: #Heq >Heq %1 normalize %1 @refl
316          | 2: #H1 lapply (Hind l2) * #HA #HB normalize
317               elim (HA H1)
318               [ 1: #H %1 %2 assumption | 2: #H %2 assumption ]
319          ]
320     | 2: normalize *
321          [ 1: * /2 by or_introl, or_intror/
322               #H %2 elim (Hind l2) #_ #H' @H' %1 @H
323          | 2: #H %2 elim (Hind l2) #_ #H' @H' %2 @H ]
324     ]
325] qed.
326
327lemma mem_append_forward : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) → (mem … elt l1) ∨ (mem … elt l2).
328#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #H' #_ @H' @H qed.
329
330lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) .
331#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed.
332
333(* "Observational" equivalence on list implies concrete equivalence. Useful to
334 * prove equality from some reasoning on indexings. Needs a particular induction
335 * principle. *)
336 
337let rec double_list_ind
338  (A : Type[0])
339  (P : list A → list A → Prop)
340  (base_nil  : P [ ] [ ])
341  (base_l1   : ∀hd1,l1. P (hd1::l1) [ ])
342  (base_l2   : ∀hd2,l2. P [ ] (hd2::l2))
343  (ind  : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2))
344  (l1, l2 : list A) on l1 ≝
345match l1 with
346[ nil ⇒
347  match l2 with
348  [ nil ⇒ base_nil
349  | cons hd2 tl2 ⇒ base_l2 hd2 tl2 ]
350| cons hd1 tl1 ⇒ 
351  match l2 with
352  [ nil ⇒ base_l1 hd1 tl1
353  | cons hd2 tl2 ⇒
354    ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2)
355  ]
356]. 
357
358lemma nth_eq_tl :
359  ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2.
360  (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) →
361  (∀i. nth_opt A i l1 = nth_opt A i l2).
362#A #l1 #l2 @(double_list_ind … l1 l2)
363[ 1: #hd1 #hd2 #_ #i elim i try /2/
364| 2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
365| 3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct
366| 4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2
367     #Hind
368     @(λi. Hind (S i))
369] qed.     
370
371
372lemma nth_eq_to_eq :
373  ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2.
374#A #l1 elim l1
375[ 1: #l2 #H lapply (H 0) normalize
376     cases l2
377     [ 1: //
378     | 2: #hd2 #tl2 normalize #Habsurd destruct ]
379| 2: #hd1 #tl1 #Hind *
380     [ 1: #H lapply (H 0) normalize #Habsurd destruct
381     | 2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq)
382          >(Hind tl2) try @refl @(nth_eq_tl … H)
383     ]
384] qed.
385
386(* --------------------------------------------------------------------------- *)
387(* General results on vectors. *)
388(* --------------------------------------------------------------------------- *)
389
390(* copied from AssemblyProof, TODO get rid of the redundant stuff. *)
391lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
392 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
393 #n #hd #tl #abs @⊥ destruct (abs)
394qed.
395
396lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
397 ∃hd.∃tl.v ≃ VCons A n hd tl.
398 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
399 [ #abs @⊥ destruct (abs)
400 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
401qed.
402
403lemma vector_append_zero:
404  ∀A,m.
405  ∀v: Vector A m.
406  ∀q: Vector A 0.
407    v = q@@v.
408  #A #m #v #q
409  >(Vector_O A q) %
410qed.
411
412corollary prod_vector_zero_eq_left:
413  ∀A, n.
414  ∀q: Vector A O.
415  ∀r: Vector A n.
416    〈q, r〉 = 〈[[ ]], r〉.
417  #A #n #q #r
418  generalize in match (Vector_O A q …);
419  #hyp
420  >hyp in ⊢ (??%?);
421  %
422qed.
423 
424lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
425# A #m #n elim m
426[ 1: normalize #v
427  elim (Vector_Sn ?? v) #hd * #tl #Eq
428  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
429  >Eq normalize //
430| 2: #n' #Hind #v
431  elim (Vector_Sn ?? v) #hd * #tl #Eq
432  elim (Hind tl)
433  #tl1 * #tl2 #Eq_tl
434  @(ex_intro … (hd ::: tl1))
435  @(ex_intro … tl2) 
436  destruct normalize //
437] qed.
438
439lemma vsplit_zero:
440  ∀A,m.
441  ∀v: Vector A m.
442    〈[[]], v〉 = vsplit A 0 m v.
443  #A #m #v
444  elim v
445  [ %
446  | #n #hd #tl #ih
447    normalize in ⊢ (???%); %
448  ]
449qed.
450
451lemma vsplit_zero2:
452  ∀A,m.
453  ∀v: Vector A m.
454    〈[[]], v〉 = vsplit' A 0 m v.
455  #A #m #v
456  elim v
457  [ %
458  | #n #hd #tl #ih
459    normalize in ⊢ (???%); %
460  ]
461qed.
462
463lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
464# A #m #n elim m
465[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
466| 2: #n' #Hind #v
467  elim (Vector_Sn ?? v) #hd * #tl #Eq
468  elim (Hind tl)
469  #tl1 * #tl2 #Eq_tl
470  @(ex_intro … (hd ::: tl1))
471  @(ex_intro … tl2) 
472  destruct normalize //
473] qed.
474
475(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
476 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
477axiom vsplit_succ:
478  ∀A, m, n.
479  ∀l: Vector A m.
480  ∀r: Vector A n.
481  ∀v: Vector A (m + n).
482  ∀hd.
483    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
484
485axiom vsplit_succ2:
486  ∀A, m, n.
487  ∀l: Vector A m.
488  ∀r: Vector A n.
489  ∀v: Vector A (m + n).
490  ∀hd.
491    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
492     
493lemma vsplit_prod2:
494  ∀A,m,n.
495  ∀p: Vector A (m + n).
496  ∀v: Vector A m.
497  ∀q: Vector A n.
498    p = v@@q → 〈v, q〉 = vsplit' A m n p.
499  #A #m
500  elim m
501  [ #n #p #v #q #hyp
502    >hyp <(vector_append_zero A n q v)
503    >(prod_vector_zero_eq_left A …)
504    @vsplit_zero2
505  | #r #ih #n #p #v #q #hyp
506    >hyp
507    cases (Vector_Sn A r v)
508    #hd #exists
509    cases exists
510    #tl #jmeq >jmeq
511    @vsplit_succ2 [1: % |2: @ih % ]
512  ]
513qed.
514
515lemma vsplit_prod:
516  ∀A,m,n.
517  ∀p: Vector A (m + n).
518  ∀v: Vector A m.
519  ∀q: Vector A n.
520    p = v@@q → 〈v, q〉 = vsplit A m n p.
521  #A #m
522  elim m
523  [ #n #p #v #q #hyp
524    >hyp <(vector_append_zero A n q v)
525    >(prod_vector_zero_eq_left A …)
526    @vsplit_zero
527  | #r #ih #n #p #v #q #hyp
528    >hyp
529    cases (Vector_Sn A r v)
530    #hd #exists
531    cases exists
532    #tl #jmeq >jmeq
533    @vsplit_succ [1: % |2: @ih % ]
534  ]
535qed.
536
537
538(* --------------------------------------------------------------------------- *)
539(* Generic properties of equivalence relations *)
540(* --------------------------------------------------------------------------- *)
541
542lemma triangle_diagram :
543  ∀acctype : Type[0].
544  ∀eqrel : acctype → acctype → Prop.
545  ∀refl_eqrel  : reflexive ? eqrel.
546  ∀trans_eqrel : transitive ? eqrel.
547  ∀sym_eqrel   : symmetric ? eqrel.
548  ∀a,b,c. eqrel a b → eqrel a c → eqrel b c.
549#acctype #eqrel #R #T #S #a #b #c
550#H1 #H2 @(T … (S … H1) H2)
551qed.
552
553lemma cotriangle_diagram :
554  ∀acctype : Type[0].
555  ∀eqrel : acctype → acctype → Prop.
556  ∀refl_eqrel  : reflexive ? eqrel.
557  ∀trans_eqrel : transitive ? eqrel.
558  ∀sym_eqrel   : symmetric ? eqrel.
559  ∀a,b,c. eqrel b a → eqrel c a → eqrel b c.
560#acctype #eqrel #R #T #S #a #b #c
561#H1 #H2 @S @(T … H2 (S … H1))
562qed.
563
564(* --------------------------------------------------------------------------- *)
565(* Quick and dirty implementation of finite sets relying on lists. The
566 * implementation is split in two: an abstract equivalence defined using inclusion
567 * of lists, and a concrete one where equivalence is defined as the closure of
568 * duplication, contraction and transposition of elements. We rely on the latter
569 * to prove stuff on folds over sets.  *)
570(* --------------------------------------------------------------------------- *)
571
572definition lset ≝ λA:Type[0]. list A.
573
574(* The empty set. *)
575definition empty_lset ≝ λA:Type[0]. nil A.
576
577(* Standard operations. *)
578definition lset_union ≝ λA:Type[0].λl1,l2 : lset A. l1 @ l2.
579
580definition lset_remove ≝ λA:DeqSet.λl:lset (carr A).λelt:carr A. (filter … (λx.¬x==elt) l).
581
582definition lset_difference ≝ λA:DeqSet.λl1,l2:lset (carr A). (filter … (λx.¬ (memb ? x l2)) l1).
583
584(* Standard predicates on sets *)
585definition lset_in ≝ λA:Type[0].λx : A. λl : lset A. mem … x l.
586
587definition lset_disjoint ≝ λA:Type[0].λl1, l2 : lset A.
588  ∀x,y. mem … x l1 → mem … y l2 → x ≠ y.
589 
590definition lset_inclusion ≝ λA:Type[0].λl1,l2.
591  All A (λx1. mem … x1 l2) l1.
592
593(* Definition of abstract set equivalence. *)
594definition lset_eq ≝ λA:Type[0].λl1,l2.
595  lset_inclusion A l1 l2 ∧
596  lset_inclusion A l2 l1.
597
598(* Properties of inclusion. *) 
599lemma reflexive_lset_inclusion : ∀A. ∀l. lset_inclusion A l l.
600#A #l elim l try //
601#hd #tl #Hind whd @conj
602[ 1: %1 @refl
603| 2: whd in Hind; @(All_mp … Hind)
604     #a #H whd %2 @H
605] qed.
606
607lemma transitive_lset_inclusion : ∀A. ∀l1,l2,l3. lset_inclusion A l1 l2 → lset_inclusion A l2 l3 → lset_inclusion A l1 l3 .
608#A #l1 #l2 #l3
609#Hincl1 #Hincl2 @(All_mp … Hincl1)
610whd in Hincl2;
611#a elim l2 in Hincl2;
612[ 1: normalize #_ @False_ind
613| 2: #hd #tl #Hind whd in ⊢ (% → ?);
614     * #Hmem #Hincl_tl whd in ⊢ (% → ?);
615     * [ 1: #Heq destruct @Hmem
616       | 2: #Hmem_tl @Hind assumption ]
617] qed.
618
619lemma cons_preserves_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A l1 (x::l2).
620#A #l1 #l2 #Hincl #x @(All_mp … Hincl) #a #Hmem whd %2 @Hmem qed.
621
622lemma cons_monotonic_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A (x::l1) (x::l2).
623#A #l1 #l2 #Hincl #x whd @conj
624[ 1: /2 by or_introl/
625| 2: @(All_mp … Hincl) #a #Hmem whd %2 @Hmem ] qed.
626
627lemma lset_inclusion_concat : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A l1 (l3 @ l2).
628#A #l1 #l2 #Hincl #l3 elim l3
629try /2 by cons_preserves_inclusion/
630qed.
631
632lemma lset_inclusion_concat_monotonic : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A (l3 @ l1) (l3 @ l2).
633#A #l1 #l2 #Hincl #l3 elim l3
634try @Hincl #hd #tl #Hind @cons_monotonic_inclusion @Hind
635qed.
636 
637(* lset_eq is an equivalence relation. *)
638lemma reflexive_lset_eq : ∀A. ∀l. lset_eq A l l. /2 by conj/ qed.
639
640lemma transitive_lset_eq : ∀A. ∀l1,l2,l3. lset_eq A l1 l2 → lset_eq A l2 l3 → lset_eq A l1 l3.
641#A #l1 #l2 #l3 * #Hincl1 #Hincl2 * #Hincl3 #Hincl4
642@conj @(transitive_lset_inclusion ??l2) assumption
643qed.
644
645lemma symmetric_lset_eq : ∀A. ∀l1,l2. lset_eq A l1 l2 → lset_eq A l2 l1.
646#A #l1 #l2 * #Hincl1 #Hincl2 @conj assumption
647qed.
648
649(* Properties of inclusion vs union and equality. *)
650lemma lset_union_inclusion : ∀A:Type[0]. ∀a,b,c. 
651  lset_inclusion A a c → lset_inclusion ? b c → lset_inclusion ? (lset_union ? a b) c.
652#A #a #b #c #H1 #H2 whd whd in match (lset_union ???);
653@All_append assumption qed.
654
655lemma lset_inclusion_union : ∀A:Type[0]. ∀a,b,c. 
656  lset_inclusion A a b ∨ lset_inclusion A a c → lset_inclusion ? a (lset_union ? b c).
657#A #a #b #c *
658[ 1: @All_mp #elt #Hmem @mem_append_backwards %1 @Hmem
659| 2: @All_mp #elt #Hmem @mem_append_backwards %2 @Hmem
660] qed.
661
662lemma lset_inclusion_eq : ∀A : Type[0]. ∀a,b,c : lset A.
663  lset_eq ? a b → lset_inclusion ? b c → lset_inclusion ? a c.
664#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H1 H3)
665qed.
666
667lemma lset_inclusion_eq2 : ∀A : Type[0]. ∀a,b,c : lset A.
668  lset_eq ? b c → lset_inclusion ? a b → lset_inclusion ? a c.
669#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H3 H1)
670qed.
671
672(* Properties of lset_eq and mem *)
673lemma lset_eq_mem :
674  ∀A:Type[0].
675  ∀s1,s2 : lset A.
676  lset_eq ? s1 s2 →
677  ∀b.mem ? b s1 → mem ? b s2.
678#A #s1 #s2 * #Hincl12 #_ #b
679whd in Hincl12; elim s1 in Hincl12;
680[ 1: normalize #_ *
681| 2: #hd #tl #Hind whd in ⊢ (% → % → ?); * #Hmem' #Hall * #Heq
682     [ 1: destruct (Heq) assumption
683     | 2: @Hind assumption ]
684] qed.
685
686lemma lset_eq_memb :
687  ∀A : DeqSet.
688  ∀s1,s2 : lset (carr A).
689  lset_eq ? s1 s2 →
690  ∀b.memb ? b s1 = true → memb ? b s2 = true.
691#A #s1 #s2 #Heq #b
692lapply (memb_to_mem A s1 b) #H1 #H2
693lapply (H1 H2) #Hmem lapply (lset_eq_mem … Heq ? Hmem) @mem_to_memb
694qed.
695
696lemma lset_eq_memb_eq :
697  ∀A : DeqSet.
698  ∀s1,s2 : lset (carr A).
699  lset_eq ? s1 s2 →
700  ∀b.memb ? b s1 = memb ? b s2.
701#A #s1 #s2 #Hlset_eq #b
702lapply (lset_eq_memb … Hlset_eq b)
703lapply (lset_eq_memb … (symmetric_lset_eq … Hlset_eq) b) 
704cases (b∈s1)
705[ 1: #_ #H lapply (H (refl ??)) #Hmem >H @refl
706| 2: cases (b∈s2) // #H lapply (H (refl ??)) #Habsurd destruct
707] qed.
708
709lemma lset_eq_filter_eq :
710  ∀A : DeqSet.
711  ∀s1,s2 : lset (carr A).
712  lset_eq ? s1 s2 → 
713  ∀l.
714     (filter ? (λwb.¬wb∈s1) l) =
715     (filter ? (λwb.¬wb∈s2) l).
716#A #s1 #s2 #Heq #l elim l
717[ 1: @refl
718| 2: #hd #tl #Hind >filter_cons_unfold >filter_cons_unfold
719      >(lset_eq_memb_eq … Heq) cases (hd∈s2)
720      normalize in match (notb ?); normalize nodelta
721      try @Hind >Hind @refl
722] qed.
723
724lemma cons_monotonic_eq : ∀A. ∀l1,l2 : lset A. lset_eq A l1 l2 → ∀x. lset_eq A (x::l1) (x::l2).
725#A #l1 #l2 #Heq #x cases Heq #Hincl1 #Hincl2
726@conj
727[ 1: @cons_monotonic_inclusion
728| 2: @cons_monotonic_inclusion ]
729assumption
730qed.
731
732(* Properties of difference and remove *)
733lemma lset_difference_unfold :
734  ∀A : DeqSet.
735  ∀s1, s2 : lset (carr A).
736  ∀hd. lset_difference A (hd :: s1) s2 =
737    if hd∈s2 then
738      lset_difference A s1 s2
739    else
740      hd :: (lset_difference A s1 s2).
741#A #s1 #s2 #hd normalize
742cases (hd∈s2) @refl
743qed.
744
745lemma lset_difference_unfold2 :
746  ∀A : DeqSet.
747  ∀s1, s2 : lset (carr A).
748  ∀hd. lset_difference A s1 (hd :: s2) =
749       lset_difference A (lset_remove ? s1 hd) s2.
750#A #s1
751elim s1
752[ 1: //
753| 2: #hd1 #tl1 #Hind #s2 #hd
754     whd in match (lset_remove ???);
755     whd in match (lset_difference A ??);
756     whd in match (memb ???);
757     lapply (eqb_true … hd1 hd)
758     cases (hd1==hd) normalize nodelta
759     [ 1: * #H #_ lapply (H (refl ??)) -H #H
760           @Hind
761     | 2: * #_ #Hguard >lset_difference_unfold
762          cases (hd1∈s2) normalize in match (notb ?); normalize nodelta
763          <Hind @refl ]
764] qed.         
765
766lemma lset_difference_disjoint :
767 ∀A : DeqSet.
768 ∀s1,s2 : lset (carr A).
769  lset_disjoint A s1 (lset_difference A s2 s1).
770#A #s1 elim s1
771[ 1: #s2 normalize #x #y *
772| 2: #hd1 #tl1 #Hind #s2 >lset_difference_unfold2 #x #y
773     whd in ⊢ (% → ?); *
774     [ 2: @Hind
775     | 1: #Heq >Heq elim s2
776          [ 1: normalize *
777          | 2: #hd2 #tl2 #Hind2 whd in match (lset_remove ???);
778               lapply (eqb_true … hd2 hd1)
779               cases (hd2 == hd1) normalize in match (notb ?); normalize nodelta * #H1 #H2
780               [ 1: @Hind2
781               | 2: >lset_difference_unfold cases (hd2 ∈ tl1) normalize nodelta try @Hind2
782                     whd in ⊢ (% → ?); *
783                     [ 1: #Hyhd2 destruct % #Heq lapply (H2 … (sym_eq … Heq)) #Habsurd destruct
784                     | 2: @Hind2 ]
785               ]
786          ]
787    ]
788] qed.
789
790
791lemma lset_remove_split : ∀A : DeqSet. ∀l1,l2 : lset A. ∀elt. lset_remove A (l1 @ l2) elt = (lset_remove … l1 elt) @ (lset_remove … l2 elt).
792#A #l1 #l2 #elt /2 by filter_append/ qed.
793
794lemma lset_inclusion_remove :
795  ∀A : DeqSet.
796  ∀s1, s2 : lset A.
797  lset_inclusion ? s1 s2 →
798  ∀elt. lset_inclusion ? (lset_remove ? s1 elt) (lset_remove ? s2 elt).
799#A #s1 elim s1
800[ 1: normalize //
801| 2: #hd1 #tl1 #Hind1 #s2 * #Hmem #Hincl
802     elim (list_mem_split ??? Hmem) #s2A * #s2B #Hs2_eq destruct #elt
803     whd in match (lset_remove ???);
804     @(match (hd1 == elt)
805       return λx. (hd1 == elt = x) → ?
806       with
807       [ true ⇒ λH. ?
808       | false ⇒ λH. ? ] (refl ? (hd1 == elt))) normalize in match (notb ?);
809     normalize nodelta
810     [ 1:  @Hind1 @Hincl
811     | 2: whd @conj
812          [ 2: @(Hind1 … Hincl)
813          | 1: >lset_remove_split >lset_remove_split
814               normalize in match (lset_remove A [hd1] elt);
815               >H normalize nodelta @mem_append_backwards %2
816               @mem_append_backwards %1 normalize %1 @refl ]
817     ]
818] qed.
819
820lemma lset_difference_lset_eq :
821  ∀A : DeqSet. ∀a,b,c.
822   lset_eq A b c →
823   lset_eq A (lset_difference A a b) (lset_difference A a c).
824#A #a #b #c #Heq
825whd in match (lset_difference ???) in ⊢ (??%%);   
826elim a
827[ 1: normalize @conj @I
828| 2: #hda #tla #Hind whd in match (foldr ?????) in ⊢ (??%%);
829     >(lset_eq_memb_eq … Heq hda) cases (hda∈c)
830     normalize in match (notb ?); normalize nodelta
831     try @Hind @cons_monotonic_eq @Hind
832] qed.
833
834lemma lset_difference_lset_remove_commute :
835  ∀A:DeqSet.
836  ∀elt,s1,s2.
837  (lset_difference A (lset_remove ? s1 elt) s2) =
838  (lset_remove A (lset_difference ? s1 s2) elt).
839#A #elt #s1 #s2
840elim s1 try //
841#hd #tl #Hind
842>lset_difference_unfold
843whd in match (lset_remove ???);
844@(match (hd==elt) return λx. (hd==elt) = x → ?
845  with
846  [ true ⇒ λHhd. ?
847  | false ⇒ λHhd. ?
848  ] (refl ? (hd==elt)))
849@(match (hd∈s2) return λx. (hd∈s2) = x → ?
850  with
851  [ true ⇒ λHmem. ?
852  | false ⇒ λHmem. ?
853  ] (refl ? (hd∈s2)))
854>notb_true >notb_false normalize nodelta try //
855try @Hind
856[ 1:  whd in match (lset_remove ???) in ⊢ (???%); >Hhd
857     elim (eqb_true ? elt elt) #_ #H >(H (refl ??))
858     normalize in match (notb ?); normalize nodelta @Hind
859| 2: >lset_difference_unfold >Hmem @Hind
860| 3: whd in match (lset_remove ???) in ⊢ (???%);
861     >lset_difference_unfold >Hhd >Hmem
862     normalize in match (notb ?);
863     normalize nodelta >Hind @refl
864] qed.
865
866(* Inversion lemma on emptyness *)
867lemma lset_eq_empty_inv : ∀A. ∀l. lset_eq A l [ ] → l = [ ].
868#A #l elim l //
869#hd' #tl' normalize #Hind * * @False_ind
870qed.
871
872(* Inversion lemma on singletons *)
873lemma lset_eq_singleton_inv : ∀A,hd,l. lset_eq A [hd] (hd::l) → All ? (λx.x=hd) l.
874#A #hd #l
875* #Hincl1 whd in ⊢ (% → ?); * #_ @All_mp
876normalize #a * [ 1: #H @H | 2: @False_ind ]
877qed.
878
879(* Permutation of two elements on top of the list is ok. *)
880lemma lset_eq_permute : ∀A,l,x1,x2. lset_eq A (x1 :: x2 :: l) (x2 :: x1 :: l).
881#A #l #x1 #x2 @conj normalize
882[ 1: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
883| 2: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
884] qed.
885
886(* "contraction" of an element. *)
887lemma lset_eq_contract : ∀A,l,x. lset_eq A (x :: x :: l) (x :: l).
888#A #l #x @conj
889[ 1: /5 by or_introl, conj, transitive_lset_inclusion/
890| 2: /5 by cons_preserves_inclusion, cons_monotonic_inclusion/ ]
891qed.
892
893(* We don't need more than one instance of each element. *)
894lemma lset_eq_filter : ∀A:DeqSet.∀tl.∀hd.
895  lset_eq A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
896#A #tl elim tl
897[ 1: #hd normalize /4 by or_introl, conj, I/
898| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
899     lapply (eqb_true A hd' hd) cases (hd'==hd)
900     [ 2: #_ normalize in match (notb ?); normalize nodelta
901          lapply (cons_monotonic_eq … (Hind hd) hd') #H
902          lapply (lset_eq_permute ? tl' hd' hd) #H'
903          @(transitive_lset_eq ? ? (hd'::hd::tl') ? … H')
904          @(transitive_lset_eq ? ?? (hd'::hd::tl') … H)
905          @lset_eq_permute
906     | 1: * #Heq #_ >(Heq (refl ??)) normalize in match (notb ?); normalize nodelta
907          lapply (Hind hd) #H
908          @(transitive_lset_eq ? ? (hd::tl') (hd::hd::tl') H)
909          @conj
910          [ 1: whd @conj /2 by or_introl/ @cons_preserves_inclusion @cons_preserves_inclusion
911               @reflexive_lset_inclusion
912          | 2: whd @conj /2 by or_introl/ ]
913     ]
914] qed.
915
916lemma lset_inclusion_filter_self :
917  ∀A:DeqSet.∀l,pred.
918    lset_inclusion A (filter ? pred l) l.
919#A #l #pred elim l
920[ 1: normalize @I
921| 2: #hd #tl #Hind whd in match (filter ???);
922     cases (pred hd) normalize nodelta
923     [ 1: @cons_monotonic_inclusion @Hind
924     | 2: @cons_preserves_inclusion @Hind ]
925] qed.   
926
927lemma lset_inclusion_filter_monotonic :
928  ∀A:DeqSet.∀l1,l2. lset_inclusion (carr A) l1 l2 →
929  ∀elt. lset_inclusion A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
930#A #l1 elim l1
931[ 1: #l2 normalize //
932| 2: #hd1 #tl1 #Hind #l2 whd in ⊢ (% → ?); * #Hmem1 #Htl1_incl #elt
933     whd >filter_cons_unfold
934     lapply (eqb_true A hd1 elt) cases (hd1==elt)
935     [ 1: * #H1 #_ lapply (H1 (refl ??)) #H1_eq >H1_eq in Hmem1; #Hmem
936          normalize in match (notb ?); normalize nodelta @Hind assumption
937     | 2: * #_ #Hneq normalize in match (notb ?); normalize nodelta
938          whd @conj
939          [ 1: elim l2 in Hmem1; try //
940               #hd2 #tl2 #Hincl whd in ⊢ (% → ?); *
941               [ 1: #Heq >Heq in Hneq; normalize
942                    lapply (eqb_true A hd2 elt) cases (hd2==elt)
943                    [ 1: * #H #_ #H2 lapply (H2 (H (refl ??))) #Habsurd destruct (Habsurd)
944                    | 2: #_ normalize nodelta #_ /2 by or_introl/ ]
945               | 2: #H lapply (Hincl H) #Hok
946                    normalize cases (hd2==elt) normalize nodelta
947                    [ 1: @Hok
948                    | 2: %2 @Hok ] ]
949          | 2: @Hind assumption ] ] ]
950qed.
951
952(* removing an element of two equivalent sets conserves equivalence. *)
953lemma lset_eq_filter_monotonic :
954  ∀A:DeqSet.∀l1,l2. lset_eq (carr A) l1 l2 →
955  ∀elt. lset_eq A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
956#A #l1 #l2 * #Hincl1 #Hincl2 #elt @conj
957/2 by lset_inclusion_filter_monotonic/
958qed.
959
960(* ---------------- Concrete implementation of sets --------------------- *)
961
962(* We can give an explicit characterization of equivalent sets: they are permutations with repetitions, i,e.
963   a composition of transpositions and duplications. We restrict ourselves to DeqSets. *)
964inductive iso_step_lset (A : DeqSet) : lset A → lset A → Prop ≝
965| lset_transpose : ∀a,x,b,y,c. iso_step_lset A (a @ [x] @ b @ [y] @ c) (a @ [y] @ b @ [x] @ c)
966| lset_weaken : ∀a,x,b. iso_step_lset A (a @ [x] @ b) (a @ [x] @ [x] @ b)
967| lset_contract : ∀a,x,b. iso_step_lset A (a @ [x] @ [x] @ b) (a @ [x] @ b).
968
969(* The equivalence is the reflexive, transitive and symmetric closure of iso_step_lset *)
970inductive lset_eq_concrete (A : DeqSet) : lset A → lset A → Prop ≝
971| lset_trans : ∀a,b,c. iso_step_lset A a b → lset_eq_concrete A b c → lset_eq_concrete A a c
972| lset_refl  : ∀a. lset_eq_concrete A a a.
973
974(* lset_eq_concrete is symmetric and transitive *)
975lemma 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.
976#A #l1 #l2 #l3 #Hequiv
977elim Hequiv //
978#a #b #c #Hstep #Hequiv #Hind #Hcl3 lapply (Hind Hcl3) #Hbl3
979@(lset_trans ???? Hstep Hbl3)
980qed.
981
982lemma symmetric_step : ∀A,l1,l2. iso_step_lset A l1 l2 → iso_step_lset A l2 l1.
983#A #l1 #l2 * /2/ qed.
984
985lemma symmetric_lset_eq_concrete : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l1.
986#A #l1 #l2 #H elim H //
987#a #b #c #Hab #Hbc #Hcb
988@(transitive_lset_eq_concrete ???? Hcb ?)
989@(lset_trans … (symmetric_step ??? Hab) (lset_refl …))
990qed.
991 
992(* lset_eq_concrete is conserved by cons. *)
993lemma equivalent_step_cons : ∀A,l1,l2. iso_step_lset A l1 l2 → ∀x. iso_step_lset A (x :: l1) (x :: l2).
994#A #l1 #l2 * // qed. (* That // was impressive. *)
995
996lemma lset_eq_concrete_cons : ∀A,l1,l2. lset_eq_concrete A l1 l2 → ∀x. lset_eq_concrete A (x :: l1) (x :: l2).
997#A #l1 #l2 #Hequiv elim Hequiv try //
998#a #b #c #Hab #Hbc #Hind #x %1{(equivalent_step_cons ??? Hab x) (Hind x)}
999qed.
1000
1001lemma absurd_list_eq_append : ∀A.∀x.∀l1,l2:list A. [ ] = l1 @ [x] @ l2 → False.
1002#A #x #l1 #l2 elim l1 normalize
1003[ 1: #Habsurd destruct
1004| 2: #hd #tl #_ #Habsurd destruct
1005] qed.
1006
1007(* Inversion lemma for emptyness, step case *)
1008lemma equivalent_iso_step_empty_inv : ∀A,l. iso_step_lset A l [] → l = [ ].
1009#A #l elim l //
1010#hd #tl #Hind #H inversion H
1011[ 1: #a #x #b #y #c #_ #Habsurd
1012      @(False_ind … (absurd_list_eq_append ? y … Habsurd))
1013| 2: #a #x #b #_ #Habsurd
1014      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
1015| 3: #a #x #b #_ #Habsurd
1016      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
1017] qed.
1018
1019(* Same thing for non-emptyness *)
1020lemma equivalent_iso_step_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → iso_step_lset A l1 l2 → l2 ≠ [ ].
1021#A #l1 elim l1
1022[ 1: #l2 * #H @(False_ind … (H (refl ??)))
1023| 2: #hd #tl #H #l2 #_ #Hstep % #Hl2 >Hl2 in Hstep; #Hstep
1024     lapply (equivalent_iso_step_empty_inv … Hstep) #Habsurd destruct
1025] qed.
1026
1027lemma lset_eq_concrete_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → lset_eq_concrete A l1 l2 → l2 ≠ [ ].
1028#A #l1 #l2 #Hl1 #H lapply Hl1 elim H
1029[ 2: #a #H @H
1030| 1: #a #b #c #Hab #Hbc #H #Ha lapply (equivalent_iso_step_cons_inv … Ha Hab) #Hb @H @Hb
1031] qed.
1032
1033lemma lset_eq_concrete_empty_inv : ∀A,l1,l2. l1 = [ ] → lset_eq_concrete A l1 l2 → l2 = [ ].
1034#A #l1 #l2 #Hl1 #H lapply Hl1 elim H //
1035#a #b #c #Hab #Hbc #Hbc_eq #Ha >Ha in Hab; #H_b lapply (equivalent_iso_step_empty_inv … ?? (symmetric_step … H_b))
1036#Hb @Hbc_eq @Hb
1037qed.
1038
1039(* Square equivalence diagram *)
1040lemma square_lset_eq_concrete :
1041  ∀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'.
1042#A #a #b #a' #b' #H1 #H2 #H3
1043@(transitive_lset_eq_concrete ???? (symmetric_lset_eq_concrete … H2))
1044@(transitive_lset_eq_concrete ???? H1)
1045@H3
1046qed.
1047
1048(* Make the transposition of elements visible at top-level *)
1049lemma transpose_lset_eq_concrete :
1050  ∀A. ∀x,y,a,b,c,a',b',c'.
1051  lset_eq_concrete A (a @ [x] @ b @ [y] @ c) (a' @ [x] @ b' @ [y] @ c') →
1052  lset_eq_concrete A (a @ [y] @ b @ [x] @ c) (a' @ [y] @ b' @ [x] @ c').
1053#A #x #y #a #b #c #a' #b' #c
1054#H @(square_lset_eq_concrete ????? H) /2 by lset_trans, lset_refl, lset_transpose/
1055qed.
1056
1057lemma switch_lset_eq_concrete :
1058  ∀A. ∀a,b,c. lset_eq_concrete A (a@[b]@c) ([b]@a@c).
1059#A #a elim a //
1060#hda #tla #Hind #b #c lapply (Hind hda c) #H
1061lapply (lset_eq_concrete_cons … H b)
1062#H' normalize in H' ⊢ %; @symmetric_lset_eq_concrete
1063/3 by lset_transpose, lset_trans, symmetric_lset_eq_concrete/
1064qed.
1065
1066(* Folding a commutative and idempotent function on equivalent sets yields the same result. *)
1067lemma lset_eq_concrete_fold :
1068  ∀A : DeqSet.
1069  ∀acctype : Type[0].
1070  ∀l1,l2 : list (carr A).
1071  lset_eq_concrete A l1 l2 →
1072  ∀f:carr A → acctype → acctype.
1073  (∀x1,x2. ∀acc. f x1 (f x2 acc) = f x2 (f x1 acc)) →
1074  (∀x.∀acc. f x (f x acc) = f x acc) →
1075  ∀acc. foldr ?? f acc l1 = foldr ?? f acc l2.
1076#A #acctype #l1 #l2 #Heq #f #Hcomm #Hidem
1077elim Heq
1078try //
1079#a' #b' #c' #Hstep #Hbc #H #acc <H -H
1080elim Hstep
1081[ 1: #a #x #b #y #c
1082     >fold_append >fold_append >fold_append >fold_append
1083     >fold_append >fold_append >fold_append >fold_append
1084     normalize
1085     cut (f x (foldr A acctype f (f y (foldr A acctype f acc c)) b) =
1086          f y (foldr A acctype f (f x (foldr A acctype f acc c)) b)) [   
1087     elim c
1088     [ 1: normalize elim b
1089          [ 1: normalize >(Hcomm x y) @refl
1090          | 2: #hdb #tlb #Hind normalize
1091               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ]
1092     | 2: #hdc #tlc #Hind normalize elim b
1093          [ 1: normalize >(Hcomm x y) @refl
1094          | 2: #hdb #tlb #Hind normalize
1095               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] ]
1096     ]
1097     #Hind >Hind @refl
1098| 2: #a #x #b
1099     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
1100     normalize >Hidem @refl
1101| 3: #a #x #b
1102     >fold_append  >(fold_append ?? ([x]@[x])) >fold_append >fold_append
1103     normalize >Hidem @refl
1104] qed.
1105
1106(* Folding over equivalent sets yields equivalent results, for any equivalence. *)
1107lemma inj_to_fold_inj :
1108  ∀A,acctype : Type[0].
1109  ∀eqrel : acctype → acctype → Prop.
1110  ∀refl_eqrel  : reflexive ? eqrel.
1111  ∀trans_eqrel : transitive ? eqrel.
1112  ∀sym_eqrel   : symmetric ? eqrel.
1113  ∀f           : A → acctype → acctype.
1114  (∀x:A.∀acc1:acctype.∀acc2:acctype.eqrel acc1 acc2→eqrel (f x acc1) (f x acc2)) →
1115  ∀l : list A. ∀acc1, acc2 : acctype. eqrel acc1 acc2 → eqrel (foldr … f acc1 l) (foldr … f acc2 l).
1116#A #acctype #eqrel #R #T #S #f #Hinj #l elim l
1117//
1118#hd #tl #Hind #acc1 #acc2 #Heq normalize @Hinj @Hind @Heq
1119qed.
1120
1121(* We need to extend the above proof to arbitrary equivalence relation instead of
1122   just standard equality. *)
1123lemma lset_eq_concrete_fold_ext :
1124  ∀A : DeqSet.
1125  ∀acctype : Type[0].
1126  ∀eqrel : acctype → acctype → Prop.
1127  ∀refl_eqrel  : reflexive ? eqrel.
1128  ∀trans_eqrel : transitive ? eqrel.
1129  ∀sym_eqrel   : symmetric ? eqrel.
1130  ∀f:carr A → acctype → acctype.
1131  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1132  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1133  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1134  ∀l1,l2 : list (carr A).
1135  lset_eq_concrete A l1 l2 → 
1136  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1137#A #acctype #eqrel #R #T #S #f #Hinj #Hcomm #Hidem #l1 #l2 #Heq
1138elim Heq
1139try //
1140#a' #b' #c' #Hstep #Hbc #H inversion Hstep
1141[ 1: #a #x #b #y #c #HlA #HlB #_ #acc
1142     >HlB in H; #H @(T … ? (H acc))
1143     >fold_append >fold_append >fold_append >fold_append
1144     >fold_append >fold_append >fold_append >fold_append
1145     normalize
1146     cut (eqrel (f x (foldr ? acctype f (f y (foldr ? acctype f acc c)) b))
1147                (f y (foldr ? acctype f (f x (foldr ? acctype f acc c)) b)))
1148     [ 1:
1149     elim c
1150     [ 1: normalize elim b
1151          [ 1: normalize @(Hcomm x y)
1152          | 2: #hdb #tlb #Hind normalize
1153               lapply (Hinj hdb ?? Hind) #Hind'
1154               lapply (T … Hind' (Hcomm ???)) #Hind''
1155               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
1156     | 2: #hdc #tlc #Hind normalize elim b
1157          [ 1: normalize @(Hcomm x y)
1158          | 2: #hdb #tlb #Hind normalize
1159               lapply (Hinj hdb ?? Hind) #Hind'
1160               lapply (T … Hind' (Hcomm ???)) #Hind''
1161               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
1162     ] ]
1163     #Hind @(inj_to_fold_inj … eqrel R T S ? Hinj … Hind)
1164| 2: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
1165     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
1166     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @S @Hidem
1167| 3: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
1168     >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append
1169     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @Hidem
1170] qed.
1171
1172(* Prepare some well-founded induction principles on lists. The idea is to perform
1173   an induction on the sequence of filterees of a list : taking the first element,
1174   filtering it out of the tail, etc. We give such principles for pairs of lists
1175   and isolated lists.  *)
1176
1177(* The two lists [l1,l2] share at least the head of l1. *)
1178definition head_shared ≝ λA. λl1,l2 : list A.
1179match l1 with
1180[ nil ⇒ l2 = (nil ?)
1181| cons hd _ ⇒  mem … hd l2
1182].
1183
1184(* Relation on pairs of lists, as described above. *)
1185definition filtered_lists : ∀A:DeqSet. relation (list (carr A)×(list (carr A))) ≝
1186λA:DeqSet. λll1,ll2.
1187let 〈la1,lb1〉 ≝ ll1 in
1188let 〈la2,lb2〉 ≝ ll2 in
1189match la2 with
1190[ nil ⇒ False
1191| cons hda2 tla2 ⇒
1192    head_shared ? la2 lb2 ∧
1193    la1 = filter … (λx.¬(x==hda2)) tla2 ∧
1194    lb1 = filter … (λx.¬(x==hda2)) lb2
1195].
1196
1197(* Notice the absence of plural : this relation works on a simple list, not a pair. *)
1198definition filtered_list : ∀A:DeqSet. relation (list (carr A)) ≝
1199λA:DeqSet. λl1,l2.
1200match l2 with
1201[ nil ⇒ False
1202| cons hd2 tl2 ⇒
1203    l1 = filter … (λx.¬(x==hd2)) l2
1204].
1205
1206(* Relation on lists based on their lengths. We know this one is well-founded. *)
1207definition length_lt : ∀A:DeqSet. relation (list (carr A)) ≝
1208λA:DeqSet. λl1,l2. lt (length ? l1) (length ? l2).
1209
1210(* length_lt can be extended on pairs by just measuring the first component *)
1211definition length_fst_lt : ∀A:DeqSet. relation (list (carr A) × (list (carr A))) ≝
1212λA:DeqSet. λll1,ll2. lt (length ? (\fst ll1)) (length ? (\fst ll2)).
1213
1214lemma filter_length : ∀A. ∀l. ∀f. |filter A f l| ≤ |l|.
1215#A #l #f elim l //
1216#hd #tl #Hind whd in match (filter ???); cases (f hd) normalize nodelta
1217[ 1: /2 by le_S_S/
1218| 2: @le_S @Hind
1219] qed.
1220
1221(* The order on lists defined by their length is wf *)
1222lemma length_lt_wf : ∀A. ∀l. WF (list (carr A)) (length_lt A) l.
1223#A #l % elim l
1224[ 1: #a normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1225| 2: #hd #tl #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1226@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1227qed.
1228
1229(* Order on pairs of list by measuring the first proj *)
1230lemma length_fst_lt_wf : ∀A. ∀ll. WF ? (length_fst_lt A) ll.
1231#A * #l1 #l2 % elim l1
1232[ 1: * #a1 #a2 normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1233| 2: #hd1 #tl1 #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1234@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1235qed.
1236
1237lemma length_to_filtered_lists : ∀A. subR ? (filtered_lists A) (length_fst_lt A).
1238#A whd * #a1 #a2 * #b1 #b2 elim b1
1239[ 1: @False_ind
1240| 2: #hd1 #tl1 #Hind whd in ⊢ (% → ?); * * #Hmem #Ha1 #Ha2 whd
1241     >Ha1 whd in match (length ??) in ⊢ (??%); @le_S_S @filter_length
1242] qed.
1243
1244lemma length_to_filtered_list : ∀A. subR ? (filtered_list A) (length_lt A).
1245#A whd #a #b elim b
1246[ 1: @False_ind
1247| 2: #hd #tl #Hind whd in ⊢ (% → ?); whd in match (filter ???);
1248     lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?);
1249     normalize nodelta #Ha whd @le_S_S >Ha @filter_length ]
1250qed.
1251
1252(* Prove well-foundedness by embedding in lt *)
1253lemma filtered_lists_wf : ∀A. ∀ll. WF ? (filtered_lists A) ll.
1254#A #ll @(WF_antimonotonic … (length_to_filtered_lists A)) @length_fst_lt_wf
1255qed.
1256
1257lemma filtered_list_wf : ∀A. ∀l. WF ? (filtered_list A) l.
1258#A #l @(WF_antimonotonic … (length_to_filtered_list A)) @length_lt_wf
1259qed.
1260
1261definition Acc_elim : ∀A,R,x. WF A R x → (∀a. R a x → WF A R a) ≝
1262λA,R,x,acc.
1263match acc with
1264[ wf _ a0 ⇒ a0 ].
1265
1266(* Stolen from Coq. Warped to avoid prop-to-type restriction. *)
1267let rec WF_rect
1268  (A : Type[0])
1269  (R : A → A → Prop)
1270  (P : A → Type[0])
1271  (f : ∀ x : A.
1272       (∀ y : A. R y x → WF ? R y) →
1273       (∀ y : A. R y x → P y) → P x)
1274  (x : A)
1275  (a : WF A R x) on a : P x ≝
1276f x (Acc_elim … a) (λy:A. λRel:R y x. WF_rect A R P f y ((Acc_elim … a) y Rel)).
1277
1278lemma lset_eq_concrete_filter : ∀A:DeqSet.∀tl.∀hd.
1279  lset_eq_concrete A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
1280#A #tl elim tl
1281[ 1: #hd //
1282| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
1283     lapply (eqb_true A hd' hd)
1284     cases (hd'==hd)
1285     [ 2: #_ normalize in match (notb false); normalize nodelta
1286          >cons_to_append >(cons_to_append … hd')
1287          >cons_to_append in ⊢ (???%); >(cons_to_append … hd') in ⊢ (???%);
1288          @(transpose_lset_eq_concrete ? hd' hd [ ] [ ] (filter A (λy:A.¬y==hd) tl') [ ] [ ] tl')
1289          >nil_append >nil_append >nil_append >nil_append
1290          @lset_eq_concrete_cons >nil_append >nil_append
1291          @Hind
1292     | 1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta
1293          >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));
1294          @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))
1295          [ 1: @Hind
1296          | 2: %2
1297          | 3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]
1298     ]
1299] qed.
1300
1301
1302(* The "abstract", observational definition of set equivalence implies the concrete one. *)
1303
1304lemma lset_eq_to_lset_eq_concrete_aux :
1305  ∀A,ll.
1306    head_shared … (\fst ll) (\snd ll) →
1307    lset_eq (carr A) (\fst ll) (\snd ll) →
1308    lset_eq_concrete A (\fst ll) (\snd ll).
1309#A #ll @(WF_ind ????? (filtered_lists_wf A ll))
1310* *
1311[ 1: #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hb2 >Hb2 #_ %2
1312| 2: #hd1 #tl1 #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hmem
1313     lapply (list_mem_split ??? Hmem) * #l2A * #l2B #Hb2 #Heq
1314     destruct
1315     lapply (Hind_wf 〈filter … (λx.¬x==hd1) tl1,filter … (λx.¬x==hd1) (l2A@l2B)〉)
1316     cut (filtered_lists A 〈filter A (λx:A.¬x==hd1) tl1,filter A (λx:A.¬x==hd1) (l2A@l2B)〉 〈hd1::tl1,l2A@[hd1]@l2B〉)
1317     [ @conj try @conj try @refl whd
1318       [ 1: /2 by /
1319       | 2: >filter_append in ⊢ (???%); >filter_append in ⊢ (???%);
1320            whd in match (filter ?? [hd1]);
1321            elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1322            normalize nodelta <filter_append @refl ] ]
1323     #Hfiltered #Hind_aux lapply (Hind_aux Hfiltered) -Hind_aux
1324     cut (lset_eq A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1325     [ 1: lapply (lset_eq_filter_monotonic … Heq hd1)
1326          >filter_cons_unfold >filter_append >(filter_append … [hd1])
1327          whd in match (filter ?? [hd1]);
1328          elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1329          normalize nodelta <filter_append #Hsol @Hsol ]
1330     #Hset_eq
1331     cut (head_shared A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1332     [ 1: lapply Hset_eq cases (filter A (λx:A.¬x==hd1) tl1)
1333          [ 1: whd in ⊢ (% → ?); * #_ elim (filter A (λx:A.¬x==hd1) (l2A@l2B)) //
1334               #hd' #tl' normalize #Hind * @False_ind
1335          | 2: #hd' #tl' * #Hincl1 #Hincl2 whd elim Hincl1 #Hsol #_ @Hsol ] ]
1336     #Hshared #Hind_aux lapply (Hind_aux Hshared Hset_eq)
1337     #Hconcrete_set_eq
1338     >cons_to_append
1339     @(transitive_lset_eq_concrete ? ([hd1]@tl1) ([hd1]@l2A@l2B) (l2A@[hd1]@l2B))
1340     [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete ]
1341     lapply (lset_eq_concrete_cons … Hconcrete_set_eq hd1) #Hconcrete_cons_eq
1342     @(square_lset_eq_concrete … Hconcrete_cons_eq)
1343     [ 1: @(lset_eq_concrete_filter ? tl1 hd1)
1344     | 2: @(lset_eq_concrete_filter ? (l2A@l2B) hd1) ]
1345] qed.
1346
1347lemma lset_eq_to_lset_eq_concrete : ∀A,l1,l2. lset_eq (carr A) l1 l2 → lset_eq_concrete A l1 l2.
1348#A *
1349[ 1: #l2 #Heq >(lset_eq_empty_inv … (symmetric_lset_eq … Heq)) //
1350| 2: #hd1 #tl1 #l2 #Hincl lapply Hincl lapply (lset_eq_to_lset_eq_concrete_aux ? 〈hd1::tl1,l2〉) #H @H
1351     whd elim Hincl * //
1352] qed.
1353
1354
1355(* The concrete one implies the abstract one. *)
1356lemma lset_eq_concrete_to_lset_eq : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq A l1 l2.
1357#A #l1 #l2 #Hconcrete
1358elim Hconcrete try //
1359#a #b #c #Hstep #Heq_bc_concrete #Heq_bc
1360cut (lset_eq A a b)
1361[ 1: elim Hstep
1362     [ 1: #a' elim a'
1363          [ 2: #hda #tla #Hind #x #b' #y #c' >cons_to_append
1364               >(associative_append ? [hda] tla ?)
1365               >(associative_append ? [hda] tla ?)
1366               @cons_monotonic_eq >nil_append >nil_append @Hind
1367          | 1: #x #b' #y #c' >nil_append >nil_append
1368               elim b' try //
1369               #hdb #tlc #Hind >append_cons >append_cons in ⊢ (???%);
1370               >associative_append >associative_append
1371               lapply (cons_monotonic_eq … Hind hdb) #Hind'               
1372               @(transitive_lset_eq ? ([x]@[hdb]@tlc@[y]@c') ([hdb]@[x]@tlc@[y]@c'))
1373               /2 by transitive_lset_eq/ ]
1374     | 2: #a' elim a'
1375          [ 2: #hda #tla #Hind #x #b' >cons_to_append
1376               >(associative_append ? [hda] tla ?)
1377               >(associative_append ? [hda] tla ?)
1378               @cons_monotonic_eq >nil_append >nil_append @Hind
1379          | 1: #x #b' >nil_append >nil_append @conj normalize
1380               [ 1: @conj [ 1: %1 @refl ] elim b'
1381                    [ 1: @I
1382                    | 2: #hdb #tlb #Hind normalize @conj
1383                         [ 1: %2 %2 %1 @refl
1384                         | 2: @(All_mp … Hind) #a0 *
1385                              [ 1: #Heq %1 @Heq
1386                              | 2: * /2 by or_introl, or_intror/ ] ] ]
1387                    #H %2 %2 %2 @H
1388               | 2: @conj try @conj try /2 by or_introl, or_intror/ elim b'
1389                    [ 1: @I
1390                    | 2: #hdb #tlb #Hind normalize @conj
1391                         [ 1: %2 %1 @refl
1392                         | 2: @(All_mp … Hind) #a0 *
1393                              [ 1: #Heq %1 @Heq
1394                              | 2: #H %2 %2 @H ] ] ] ] ]
1395     | 3: #a #x #b elim a try @lset_eq_contract
1396          #hda #tla #Hind @cons_monotonic_eq @Hind ] ]
1397#Heq_ab @(transitive_lset_eq … Heq_ab Heq_bc)
1398qed.
1399
1400lemma lset_eq_fold :
1401  ∀A : DeqSet.
1402  ∀acctype : Type[0].
1403  ∀eqrel : acctype → acctype → Prop.
1404  ∀refl_eqrel  : reflexive ? eqrel.
1405  ∀trans_eqrel : transitive ? eqrel.
1406  ∀sym_eqrel   : symmetric ? eqrel.
1407  ∀f:carr A → acctype → acctype.
1408  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1409  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1410  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1411  ∀l1,l2 : list (carr A).
1412  lset_eq A l1 l2 → 
1413  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1414#A #acctype #eqrel #refl_eqrel #trans_eqrel #sym_eqrel #f #Hinj #Hsym #Hcontract #l1 #l2 #Heq #acc
1415lapply (lset_eq_to_lset_eq_concrete … Heq) #Heq_concrete
1416@(lset_eq_concrete_fold_ext A acctype eqrel refl_eqrel trans_eqrel sym_eqrel f Hinj Hsym Hcontract l1 l2 Heq_concrete acc)
1417qed.
1418
1419(* Additional lemmas on lsets *)
1420
1421lemma lset_difference_empty :
1422  ∀A : DeqSet.
1423  ∀s1. lset_difference A s1 [ ] = s1.
1424#A #s1 elim s1 try //
1425#hd #tl #Hind >lset_difference_unfold >Hind @refl
1426qed.
1427
1428lemma lset_not_mem_difference :
1429  ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3).
1430#A #s1 #s2 #s3 #Hincl #x #Hmem
1431lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
1432elim s1 in Hincl Hmem;
1433[ 1: #_ *
1434| 2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall *
1435     [ 2: #Hmem_x_tl @Hind assumption
1436     | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]
1437] qed.
1438
1439lemma lset_mem_inclusion_mem :
1440  ∀A,s1,s2,elt.
1441  mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2.
1442#A #s1 elim s1
1443[ 1: #s2 #elt *
1444| 2: #hd #tl #Hind #s2 #elt *
1445     [ 1: #Heq destruct * //
1446     | 2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl;
1447          [ 1: #_ *
1448          | 2: #hd' #tl' #Hind * #Hmem' #Hall *
1449               [ 1: #Heq destruct @Hmem'
1450               | 2: #Hmem'' @Hind assumption ] ] ] ]
1451qed.
1452
1453lemma lset_remove_inclusion :
1454  ∀A : DeqSet. ∀s,elt.
1455    lset_inclusion A (lset_remove ? s elt) s.
1456#A #s elim s try // qed.
1457
1458lemma lset_difference_remove_inclusion :
1459  ∀A : DeqSet. ∀s1,s2,elt.
1460    lset_inclusion A
1461      (lset_difference ? (lset_remove ? s1 elt) s2) 
1462      (lset_difference ? s1 s2).
1463#A #s elim s try // qed.
1464
1465lemma lset_difference_permute :
1466  ∀A : DeqSet. ∀s1,s2,s3.
1467    lset_difference A s1 (s2 @ s3) =
1468    lset_difference A s1 (s3 @ s2).
1469#A #s1 #s2 elim s2 try //
1470#hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute
1471>Hind elim s3 try //
1472#hd' #tl' #Hind' >cons_to_append >associative_append
1473>associative_append >(cons_to_append … hd tl)
1474>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
1475>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
1476<Hind' generalize in match (lset_difference ???); #foo
1477whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
1478whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
1479elim foo
1480[ 1: normalize @refl
1481| 2: #hd'' #tl'' #Hind normalize
1482      @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with
1483        [ true ⇒ λH. ?
1484        | false ⇒ λH. ?
1485        ] (refl ? (hd''==hd')))
1486      @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with
1487        [ true ⇒ λH'. ?
1488        | false ⇒ λH'. ?
1489        ] (refl ? (hd''==hd)))
1490      normalize nodelta
1491      try @Hind
1492[ 1: normalize >H normalize nodelta @Hind
1493| 2: normalize >H' normalize nodelta @Hind
1494| 3: normalize >H >H' normalize nodelta >Hind @refl
1495] qed.
1496
1497
1498
1499lemma lset_disjoint_dec :
1500  ∀A : DeqSet.
1501  ∀s1,elt,s2.
1502  mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1).
1503#A #s1 #elt #s2
1504@(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ?
1505  with
1506  [ false ⇒ λHA. ?
1507  | true ⇒ λHA. ? ] (refl ? (elt ∈ s1)))
1508[ 1: lapply (memb_to_mem … HA) #Hmem
1509     %1 @Hmem
1510| 2: %2 elim s1 in HA;
1511     [ 1: #_ whd %1 @refl
1512     | 2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?);
1513          >lset_difference_unfold
1514          >lset_difference_unfold2
1515          lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %);
1516          cases (elt==hd1) normalize nodelta
1517          [ 1: #_ #Habsurd destruct
1518          | 2: #HA #HB >HB normalize nodelta %1 @refl ] ] ]
1519qed.
1520
1521lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2.
1522  mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l.
1523#A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/
1524qed.
1525
1526lemma lset_inclusion_difference_aux :
1527  ∀A : DeqSet. ∀s1,s2.
1528  lset_inclusion A s1 s2 →
1529  (lset_eq A s2 (s1@lset_difference A s2 s1)).
1530#A #s1
1531@(WF_ind ????? (filtered_list_wf A s1))
1532*
1533[ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq
1534| 2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl
1535     lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?)
1536     [ 1: whd normalize
1537          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ]
1538     #Hind_wf     
1539     elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq
1540     >cons_to_append in ⊢ (???%); >associative_append
1541     >lset_difference_unfold2
1542     >nil_append
1543     >lset_remove_split >lset_remove_split
1544     normalize in match (lset_remove ? [hd1] hd1);
1545     >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
1546     >nil_append <lset_remove_split >lset_difference_lset_remove_commute
1547     lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?)
1548     [ 1: lapply (lset_inclusion_remove … Hincl hd1)
1549          >Heq @lset_inclusion_eq2
1550          >lset_remove_split >lset_remove_split >lset_remove_split
1551          normalize in match (lset_remove ? [hd1] hd1);
1552          >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta
1553          >nil_append @reflexive_lset_eq ]
1554     #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind
1555     @lset_eq_concrete_to_lset_eq
1556     lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc
1557     @(square_lset_eq_concrete ????? Hindc) -Hindc -Hind
1558     [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B))
1559          [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete
1560          | 1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ]
1561     | 2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …))
1562          elim (s2A@s2B)
1563          [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq
1564          | 2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold
1565               @(match (hd2∈filter A (λx:A.¬x==hd1) tl1)
1566                 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ?
1567                 with
1568                 [ false ⇒ λH. ?
1569                 | true ⇒ λH. ?
1570                 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta
1571               [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter))
1572                    normalize nodelta @Hind
1573               | 2: @(match (hd2∈tl1)
1574                      return λx. ((hd2∈tl1) = x) → ?
1575                      with
1576                      [ false ⇒ λH'. ?
1577                      | true ⇒ λH'. ?
1578                      ] (refl ? (hd2∈tl1))) normalize nodelta
1579                      [ 1: (* We have hd2 = hd1 *)
1580                            cut (hd2 = hd1)
1581                            [ elim tl1 in H H';
1582                              [ 1: normalize #_ #Habsurd destruct (Habsurd)
1583                              | 2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?);
1584                                    lapply (eqb_true ? hdtl1 hd1)
1585                                    cases (hdtl1==hd1) normalize nodelta
1586                                    [ 1: * #H >(H (refl ??)) #_
1587                                         lapply (eqb_true ? hd2 hd1)
1588                                         cases (hd2==hd1) normalize nodelta *
1589                                         [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl
1590                                         | 2: #_ #_ @Hind ]
1591                                    | 2: #_ normalize lapply (eqb_true ? hd2 hdtl1)
1592                                         cases (hd2 == hdtl1) normalize nodelta *
1593                                         [ 1: #_ #_ #Habsurd destruct (Habsurd)
1594                                         | 2: #_ #_ @Hind ] ] ] ]
1595                           #Heq_hd2hd1 destruct (Heq_hd2hd1)
1596                           @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind)
1597                           #Hind' @(square_lset_eq_concrete … Hind')
1598                           [ 2: @lset_refl
1599                           | 1: >cons_to_append >cons_to_append in ⊢ (???%);
1600                                @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
1601                                [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract
1602                                | 2: >(cons_to_append … hd1 (lset_difference ???))
1603                                     @lset_eq_concrete_cons >nil_append >nil_append
1604                                     @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ]
1605                        | 2: @(match hd2 == hd1
1606                               return λx. ((hd2 == hd1) = x) → ?
1607                               with
1608                               [ true ⇒ λH''. ?
1609                               | false ⇒ λH''. ?
1610                               ] (refl ? (hd2 == hd1)))
1611                             [ 1: whd in match (lset_remove ???) in ⊢ (???%);
1612                                  >H'' normalize nodelta >((proj1 … (eqb_true …)) H'')
1613                                  @(transitive_lset_eq … Hind)
1614                                  @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1)))
1615                                  [ 2: @lset_eq_contract ]                                                                   
1616                                  @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons                                 
1617                                  @switch_lset_eq_concrete
1618                             | 2: whd in match (lset_remove ???) in ⊢ (???%);
1619                                  >H'' >notb_false normalize nodelta
1620                                  @lset_eq_concrete_to_lset_eq
1621                                  lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc
1622                                  lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' -Hindc
1623                                  @(square_lset_eq_concrete … Hindc')
1624                                  [ 1: @symmetric_lset_eq_concrete
1625                                       >cons_to_append >cons_to_append in ⊢ (???%);
1626                                       >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%);
1627                                       @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
1628                                  | 2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?)
1629                                  ]
1630                              ]
1631                        ]
1632                    ]
1633             ]
1634      ]
1635] qed.             
1636                                                       
1637lemma lset_inclusion_difference :
1638  ∀A : DeqSet.
1639  ∀s1,s2 : lset (carr A).
1640    lset_inclusion ? s1 s2 →
1641    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
1642          lset_disjoint ? s1 s2' ∧
1643          lset_eq ? s2' (lset_difference ? s2 s1).
1644#A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj
1645[ 1: @lset_inclusion_difference_aux @Hincl
1646| 2: /2 by lset_difference_disjoint/
1647| 3,4: @reflexive_lset_inclusion ]
1648qed.
Note: See TracBrowser for help on using the repository browser.