source: src/Clight/frontend_misc.ma @ 2441

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

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

File size: 50.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(* 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
1420
Note: See TracBrowser for help on using the repository browser.