source: src/Clight/frontend_misc.ma @ 2438

Last change on this file since 2438 was 2438, checked in by garnier, 8 years ago

Sync of the w.i.p. for switch removal.

File size: 45.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(* --------------------------------------------------------------------------- *)
334(* Generic properties of equivalence relations *)
335(* --------------------------------------------------------------------------- *)
336
337lemma triangle_diagram :
338  ∀acctype : Type[0].
339  ∀eqrel : acctype → acctype → Prop.
340  ∀refl_eqrel  : reflexive ? eqrel.
341  ∀trans_eqrel : transitive ? eqrel.
342  ∀sym_eqrel   : symmetric ? eqrel.
343  ∀a,b,c. eqrel a b → eqrel a c → eqrel b c.
344#acctype #eqrel #R #T #S #a #b #c
345#H1 #H2 @(T … (S … H1) H2)
346qed.
347
348lemma cotriangle_diagram :
349  ∀acctype : Type[0].
350  ∀eqrel : acctype → acctype → Prop.
351  ∀refl_eqrel  : reflexive ? eqrel.
352  ∀trans_eqrel : transitive ? eqrel.
353  ∀sym_eqrel   : symmetric ? eqrel.
354  ∀a,b,c. eqrel b a → eqrel c a → eqrel b c.
355#acctype #eqrel #R #T #S #a #b #c
356#H1 #H2 @S @(T … H2 (S … H1))
357qed.
358
359(* --------------------------------------------------------------------------- *)
360(* Quick and dirty implementation of finite sets relying on lists. The
361 * implementation is split in two: an abstract equivalence defined using inclusion
362 * of lists, and a concrete one where equivalence is defined as the closure of
363 * duplication, contraction and transposition of elements. We rely on the latter
364 * to prove stuff on folds over sets.  *)
365(* --------------------------------------------------------------------------- *)
366
367definition lset ≝ λA:Type[0]. list A.
368
369(* The empty set. *)
370definition empty_lset ≝ λA:Type[0]. nil A.
371
372(* Standard operations. *)
373definition lset_union ≝ λA:Type[0].λl1,l2 : lset A. l1 @ l2.
374
375definition lset_remove ≝ λA:DeqSet.λl:lset (carr A).λelt:carr A. (filter … (λx.¬x==elt) l).
376
377definition lset_difference ≝ λA:DeqSet.λl1,l2:lset (carr A). (filter … (λx.¬ (memb ? x l2)) l1).
378
379(* Standard predicates on sets *)
380definition lset_in ≝ λA:Type[0].λx : A. λl : lset A. mem … x l.
381
382definition lset_disjoint ≝ λA:Type[0].λl1, l2 : lset A.
383  ∀x,y. mem … x l1 → mem … y l2 → x ≠ y.
384 
385definition lset_inclusion ≝ λA:Type[0].λl1,l2.
386  All A (λx1. mem … x1 l2) l1.
387
388(* Definition of abstract set equivalence. *)
389definition lset_eq ≝ λA:Type[0].λl1,l2.
390  lset_inclusion A l1 l2 ∧
391  lset_inclusion A l2 l1.
392
393(* Properties of inclusion. *) 
394lemma reflexive_lset_inclusion : ∀A. ∀l. lset_inclusion A l l.
395#A #l elim l try //
396#hd #tl #Hind whd @conj
397[ 1: %1 @refl
398| 2: whd in Hind; @(All_mp … Hind)
399     #a #H whd %2 @H
400] qed.
401
402lemma transitive_lset_inclusion : ∀A. ∀l1,l2,l3. lset_inclusion A l1 l2 → lset_inclusion A l2 l3 → lset_inclusion A l1 l3 .
403#A #l1 #l2 #l3
404#Hincl1 #Hincl2 @(All_mp … Hincl1)
405whd in Hincl2;
406#a elim l2 in Hincl2;
407[ 1: normalize #_ @False_ind
408| 2: #hd #tl #Hind whd in ⊢ (% → ?);
409     * #Hmem #Hincl_tl whd in ⊢ (% → ?);
410     * [ 1: #Heq destruct @Hmem
411       | 2: #Hmem_tl @Hind assumption ]
412] qed.
413
414lemma cons_preserves_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A l1 (x::l2).
415#A #l1 #l2 #Hincl #x @(All_mp … Hincl) #a #Hmem whd %2 @Hmem qed.
416
417lemma cons_monotonic_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A (x::l1) (x::l2).
418#A #l1 #l2 #Hincl #x whd @conj
419[ 1: /2 by or_introl/
420| 2: @(All_mp … Hincl) #a #Hmem whd %2 @Hmem ] qed.
421
422lemma lset_inclusion_concat : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A l1 (l3 @ l2).
423#A #l1 #l2 #Hincl #l3 elim l3
424try /2 by cons_preserves_inclusion/
425qed.
426
427lemma lset_inclusion_concat_monotonic : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A (l3 @ l1) (l3 @ l2).
428#A #l1 #l2 #Hincl #l3 elim l3
429try @Hincl #hd #tl #Hind @cons_monotonic_inclusion @Hind
430qed.
431 
432(* lset_eq is an equivalence relation. *)
433lemma reflexive_lset_eq : ∀A. ∀l. lset_eq A l l. /2 by conj/ qed.
434
435lemma transitive_lset_eq : ∀A. ∀l1,l2,l3. lset_eq A l1 l2 → lset_eq A l2 l3 → lset_eq A l1 l3.
436#A #l1 #l2 #l3 * #Hincl1 #Hincl2 * #Hincl3 #Hincl4
437@conj @(transitive_lset_inclusion ??l2) assumption
438qed.
439
440lemma symmetric_lset_eq : ∀A. ∀l1,l2. lset_eq A l1 l2 → lset_eq A l2 l1.
441#A #l1 #l2 * #Hincl1 #Hincl2 @conj assumption
442qed.
443
444(* Properties of inclusion vs union and equality. *)
445lemma lset_union_inclusion : ∀A:Type[0]. ∀a,b,c. 
446  lset_inclusion A a c → lset_inclusion ? b c → lset_inclusion ? (lset_union ? a b) c.
447#A #a #b #c #H1 #H2 whd whd in match (lset_union ???);
448@All_append assumption qed.
449
450lemma lset_inclusion_union : ∀A:Type[0]. ∀a,b,c. 
451  lset_inclusion A a b ∨ lset_inclusion A a c → lset_inclusion ? a (lset_union ? b c).
452#A #a #b #c *
453[ 1: @All_mp #elt #Hmem @mem_append_backwards %1 @Hmem
454| 2: @All_mp #elt #Hmem @mem_append_backwards %2 @Hmem
455] qed.
456
457lemma lset_inclusion_eq : ∀A : Type[0]. ∀a,b,c : lset A.
458  lset_eq ? a b → lset_inclusion ? b c → lset_inclusion ? a c.
459#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H1 H3)
460qed.
461
462lemma lset_inclusion_eq2 : ∀A : Type[0]. ∀a,b,c : lset A.
463  lset_eq ? b c → lset_inclusion ? a b → lset_inclusion ? a c.
464#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H3 H1)
465qed.
466
467(* Properties of lset_eq and mem *)
468lemma lset_eq_mem :
469  ∀A:Type[0].
470  ∀s1,s2 : lset A.
471  lset_eq ? s1 s2 →
472  ∀b.mem ? b s1 → mem ? b s2.
473#A #s1 #s2 * #Hincl12 #_ #b
474whd in Hincl12; elim s1 in Hincl12;
475[ 1: normalize #_ *
476| 2: #hd #tl #Hind whd in ⊢ (% → % → ?); * #Hmem' #Hall * #Heq
477     [ 1: destruct (Heq) assumption
478     | 2: @Hind assumption ]
479] qed.
480
481lemma lset_eq_memb :
482  ∀A : DeqSet.
483  ∀s1,s2 : lset (carr A).
484  lset_eq ? s1 s2 →
485  ∀b.memb ? b s1 = true → memb ? b s2 = true.
486#A #s1 #s2 #Heq #b
487lapply (memb_to_mem A s1 b) #H1 #H2
488lapply (H1 H2) #Hmem lapply (lset_eq_mem … Heq ? Hmem) @mem_to_memb
489qed.
490
491lemma lset_eq_memb_eq :
492  ∀A : DeqSet.
493  ∀s1,s2 : lset (carr A).
494  lset_eq ? s1 s2 →
495  ∀b.memb ? b s1 = memb ? b s2.
496#A #s1 #s2 #Hlset_eq #b
497lapply (lset_eq_memb … Hlset_eq b)
498lapply (lset_eq_memb … (symmetric_lset_eq … Hlset_eq) b) 
499cases (b∈s1)
500[ 1: #_ #H lapply (H (refl ??)) #Hmem >H @refl
501| 2: cases (b∈s2) // #H lapply (H (refl ??)) #Habsurd destruct
502] qed.
503
504lemma lset_eq_filter_eq :
505  ∀A : DeqSet.
506  ∀s1,s2 : lset (carr A).
507  lset_eq ? s1 s2 → 
508  ∀l.
509     (filter ? (λwb.¬wb∈s1) l) =
510     (filter ? (λwb.¬wb∈s2) l).
511#A #s1 #s2 #Heq #l elim l
512[ 1: @refl
513| 2: #hd #tl #Hind >filter_cons_unfold >filter_cons_unfold
514      >(lset_eq_memb_eq … Heq) cases (hd∈s2)
515      normalize in match (notb ?); normalize nodelta
516      try @Hind >Hind @refl
517] qed.
518
519lemma cons_monotonic_eq : ∀A. ∀l1,l2 : lset A. lset_eq A l1 l2 → ∀x. lset_eq A (x::l1) (x::l2).
520#A #l1 #l2 #Heq #x cases Heq #Hincl1 #Hincl2
521@conj
522[ 1: @cons_monotonic_inclusion
523| 2: @cons_monotonic_inclusion ]
524assumption
525qed.
526
527(* Properties of difference and remove *)
528lemma lset_difference_unfold :
529  ∀A : DeqSet.
530  ∀s1, s2 : lset (carr A).
531  ∀hd. lset_difference A (hd :: s1) s2 =
532    if hd∈s2 then
533      lset_difference A s1 s2
534    else
535      hd :: (lset_difference A s1 s2).
536#A #s1 #s2 #hd normalize
537cases (hd∈s2) @refl
538qed.
539
540lemma lset_difference_unfold2 :
541  ∀A : DeqSet.
542  ∀s1, s2 : lset (carr A).
543  ∀hd. lset_difference A s1 (hd :: s2) =
544       lset_difference A (lset_remove ? s1 hd) s2.
545#A #s1
546elim s1
547[ 1: //
548| 2: #hd1 #tl1 #Hind #s2 #hd
549     whd in match (lset_remove ???);
550     whd in match (lset_difference A ??);
551     whd in match (memb ???);
552     lapply (eqb_true … hd1 hd)
553     cases (hd1==hd) normalize nodelta
554     [ 1: * #H #_ lapply (H (refl ??)) -H #H
555           @Hind
556     | 2: * #_ #Hguard >lset_difference_unfold
557          cases (hd1∈s2) normalize in match (notb ?); normalize nodelta
558          <Hind @refl ]
559] qed.         
560
561lemma lset_difference_disjoint :
562 ∀A : DeqSet.
563 ∀s1,s2 : lset (carr A).
564  lset_disjoint A s1 (lset_difference A s2 s1).
565#A #s1 elim s1
566[ 1: #s2 normalize #x #y *
567| 2: #hd1 #tl1 #Hind #s2 >lset_difference_unfold2 #x #y
568     whd in ⊢ (% → ?); *
569     [ 2: @Hind
570     | 1: #Heq >Heq elim s2
571          [ 1: normalize *
572          | 2: #hd2 #tl2 #Hind2 whd in match (lset_remove ???);
573               lapply (eqb_true … hd2 hd1)
574               cases (hd2 == hd1) normalize in match (notb ?); normalize nodelta * #H1 #H2
575               [ 1: @Hind2
576               | 2: >lset_difference_unfold cases (hd2 ∈ tl1) normalize nodelta try @Hind2
577                     whd in ⊢ (% → ?); *
578                     [ 1: #Hyhd2 destruct % #Heq lapply (H2 … (sym_eq … Heq)) #Habsurd destruct
579                     | 2: @Hind2 ]
580               ]
581          ]
582    ]
583] qed.
584
585
586lemma lset_remove_split : ∀A : DeqSet. ∀l1,l2 : lset A. ∀elt. lset_remove A (l1 @ l2) elt = (lset_remove … l1 elt) @ (lset_remove … l2 elt).
587#A #l1 #l2 #elt /2 by filter_append/ qed.
588
589lemma lset_inclusion_remove :
590  ∀A : DeqSet.
591  ∀s1, s2 : lset A.
592  lset_inclusion ? s1 s2 →
593  ∀elt. lset_inclusion ? (lset_remove ? s1 elt) (lset_remove ? s2 elt).
594#A #s1 elim s1
595[ 1: normalize //
596| 2: #hd1 #tl1 #Hind1 #s2 * #Hmem #Hincl
597     elim (list_mem_split ??? Hmem) #s2A * #s2B #Hs2_eq destruct #elt
598     whd in match (lset_remove ???);
599     @(match (hd1 == elt)
600       return λx. (hd1 == elt = x) → ?
601       with
602       [ true ⇒ λH. ?
603       | false ⇒ λH. ? ] (refl ? (hd1 == elt))) normalize in match (notb ?);
604     normalize nodelta
605     [ 1:  @Hind1 @Hincl
606     | 2: whd @conj
607          [ 2: @(Hind1 … Hincl)
608          | 1: >lset_remove_split >lset_remove_split
609               normalize in match (lset_remove A [hd1] elt);
610               >H normalize nodelta @mem_append_backwards %2
611               @mem_append_backwards %1 normalize %1 @refl ]
612     ]
613] qed.
614
615lemma lset_difference_lset_eq :
616  ∀A : DeqSet. ∀a,b,c.
617   lset_eq A b c →
618   lset_eq A (lset_difference A a b) (lset_difference A a c).
619#A #a #b #c #Heq
620whd in match (lset_difference ???) in ⊢ (??%%);   
621elim a
622[ 1: normalize @conj @I
623| 2: #hda #tla #Hind whd in match (foldr ?????) in ⊢ (??%%);
624     >(lset_eq_memb_eq … Heq hda) cases (hda∈c)
625     normalize in match (notb ?); normalize nodelta
626     try @Hind @cons_monotonic_eq @Hind
627] qed.
628
629lemma lset_difference_lset_remove_commute :
630  ∀A:DeqSet.
631  ∀elt,s1,s2.
632  (lset_difference A (lset_remove ? s1 elt) s2) =
633  (lset_remove A (lset_difference ? s1 s2) elt).
634#A #elt #s1 #s2
635elim s1 try //
636#hd #tl #Hind
637>lset_difference_unfold
638whd in match (lset_remove ???);
639@(match (hd==elt) return λx. (hd==elt) = x → ?
640  with
641  [ true ⇒ λHhd. ?
642  | false ⇒ λHhd. ?
643  ] (refl ? (hd==elt)))
644@(match (hd∈s2) return λx. (hd∈s2) = x → ?
645  with
646  [ true ⇒ λHmem. ?
647  | false ⇒ λHmem. ?
648  ] (refl ? (hd∈s2)))
649>notb_true >notb_false normalize nodelta try //
650try @Hind
651[ 1:  whd in match (lset_remove ???) in ⊢ (???%); >Hhd
652     elim (eqb_true ? elt elt) #_ #H >(H (refl ??))
653     normalize in match (notb ?); normalize nodelta @Hind
654| 2: >lset_difference_unfold >Hmem @Hind
655| 3: whd in match (lset_remove ???) in ⊢ (???%);
656     >lset_difference_unfold >Hhd >Hmem
657     normalize in match (notb ?);
658     normalize nodelta >Hind @refl
659] qed.
660
661(* Inversion lemma on emptyness *)
662lemma lset_eq_empty_inv : ∀A. ∀l. lset_eq A l [ ] → l = [ ].
663#A #l elim l //
664#hd' #tl' normalize #Hind * * @False_ind
665qed.
666
667(* Inversion lemma on singletons *)
668lemma lset_eq_singleton_inv : ∀A,hd,l. lset_eq A [hd] (hd::l) → All ? (λx.x=hd) l.
669#A #hd #l
670* #Hincl1 whd in ⊢ (% → ?); * #_ @All_mp
671normalize #a * [ 1: #H @H | 2: @False_ind ]
672qed.
673
674(* Permutation of two elements on top of the list is ok. *)
675lemma lset_eq_permute : ∀A,l,x1,x2. lset_eq A (x1 :: x2 :: l) (x2 :: x1 :: l).
676#A #l #x1 #x2 @conj normalize
677[ 1: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
678| 2: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
679] qed.
680
681(* "contraction" of an element. *)
682lemma lset_eq_contract : ∀A,l,x. lset_eq A (x :: x :: l) (x :: l).
683#A #l #x @conj
684[ 1: /5 by or_introl, conj, transitive_lset_inclusion/
685| 2: /5 by cons_preserves_inclusion, cons_monotonic_inclusion/ ]
686qed.
687
688(* We don't need more than one instance of each element. *)
689lemma lset_eq_filter : ∀A:DeqSet.∀tl.∀hd.
690  lset_eq A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
691#A #tl elim tl
692[ 1: #hd normalize /4 by or_introl, conj, I/
693| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
694     lapply (eqb_true A hd' hd) cases (hd'==hd)
695     [ 2: #_ normalize in match (notb ?); normalize nodelta
696          lapply (cons_monotonic_eq … (Hind hd) hd') #H
697          lapply (lset_eq_permute ? tl' hd' hd) #H'
698          @(transitive_lset_eq ? ? (hd'::hd::tl') ? … H')
699          @(transitive_lset_eq ? ?? (hd'::hd::tl') … H)
700          @lset_eq_permute
701     | 1: * #Heq #_ >(Heq (refl ??)) normalize in match (notb ?); normalize nodelta
702          lapply (Hind hd) #H
703          @(transitive_lset_eq ? ? (hd::tl') (hd::hd::tl') H)
704          @conj
705          [ 1: whd @conj /2 by or_introl/ @cons_preserves_inclusion @cons_preserves_inclusion
706               @reflexive_lset_inclusion
707          | 2: whd @conj /2 by or_introl/ ]
708     ]
709] qed.
710
711lemma lset_inclusion_filter_self :
712  ∀A:DeqSet.∀l,pred.
713    lset_inclusion A (filter ? pred l) l.
714#A #l #pred elim l
715[ 1: normalize @I
716| 2: #hd #tl #Hind whd in match (filter ???);
717     cases (pred hd) normalize nodelta
718     [ 1: @cons_monotonic_inclusion @Hind
719     | 2: @cons_preserves_inclusion @Hind ]
720] qed.   
721
722lemma lset_inclusion_filter_monotonic :
723  ∀A:DeqSet.∀l1,l2. lset_inclusion (carr A) l1 l2 →
724  ∀elt. lset_inclusion A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
725#A #l1 elim l1
726[ 1: #l2 normalize //
727| 2: #hd1 #tl1 #Hind #l2 whd in ⊢ (% → ?); * #Hmem1 #Htl1_incl #elt
728     whd >filter_cons_unfold
729     lapply (eqb_true A hd1 elt) cases (hd1==elt)
730     [ 1: * #H1 #_ lapply (H1 (refl ??)) #H1_eq >H1_eq in Hmem1; #Hmem
731          normalize in match (notb ?); normalize nodelta @Hind assumption
732     | 2: * #_ #Hneq normalize in match (notb ?); normalize nodelta
733          whd @conj
734          [ 1: elim l2 in Hmem1; try //
735               #hd2 #tl2 #Hincl whd in ⊢ (% → ?); *
736               [ 1: #Heq >Heq in Hneq; normalize
737                    lapply (eqb_true A hd2 elt) cases (hd2==elt)
738                    [ 1: * #H #_ #H2 lapply (H2 (H (refl ??))) #Habsurd destruct (Habsurd)
739                    | 2: #_ normalize nodelta #_ /2 by or_introl/ ]
740               | 2: #H lapply (Hincl H) #Hok
741                    normalize cases (hd2==elt) normalize nodelta
742                    [ 1: @Hok
743                    | 2: %2 @Hok ] ]
744          | 2: @Hind assumption ] ] ]
745qed.
746
747(* removing an element of two equivalent sets conserves equivalence. *)
748lemma lset_eq_filter_monotonic :
749  ∀A:DeqSet.∀l1,l2. lset_eq (carr A) l1 l2 →
750  ∀elt. lset_eq A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
751#A #l1 #l2 * #Hincl1 #Hincl2 #elt @conj
752/2 by lset_inclusion_filter_monotonic/
753qed.
754
755(* ---------------- Concrete implementation of sets --------------------- *)
756
757(* We can give an explicit characterization of equivalent sets: they are permutations with repetitions, i,e.
758   a composition of transpositions and duplications. We restrict ourselves to DeqSets. *)
759inductive iso_step_lset (A : DeqSet) : lset A → lset A → Prop ≝
760| lset_transpose : ∀a,x,b,y,c. iso_step_lset A (a @ [x] @ b @ [y] @ c) (a @ [y] @ b @ [x] @ c)
761| lset_weaken : ∀a,x,b. iso_step_lset A (a @ [x] @ b) (a @ [x] @ [x] @ b)
762| lset_contract : ∀a,x,b. iso_step_lset A (a @ [x] @ [x] @ b) (a @ [x] @ b).
763
764(* The equivalence is the reflexive, transitive and symmetric closure of iso_step_lset *)
765inductive lset_eq_concrete (A : DeqSet) : lset A → lset A → Prop ≝
766| lset_trans : ∀a,b,c. iso_step_lset A a b → lset_eq_concrete A b c → lset_eq_concrete A a c
767| lset_refl  : ∀a. lset_eq_concrete A a a.
768
769(* lset_eq_concrete is symmetric and transitive *)
770lemma 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.
771#A #l1 #l2 #l3 #Hequiv
772elim Hequiv //
773#a #b #c #Hstep #Hequiv #Hind #Hcl3 lapply (Hind Hcl3) #Hbl3
774@(lset_trans ???? Hstep Hbl3)
775qed.
776
777lemma symmetric_step : ∀A,l1,l2. iso_step_lset A l1 l2 → iso_step_lset A l2 l1.
778#A #l1 #l2 * /2/ qed.
779
780lemma symmetric_lset_eq_concrete : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l1.
781#A #l1 #l2 #H elim H //
782#a #b #c #Hab #Hbc #Hcb
783@(transitive_lset_eq_concrete ???? Hcb ?)
784@(lset_trans … (symmetric_step ??? Hab) (lset_refl …))
785qed.
786 
787(* lset_eq_concrete is conserved by cons. *)
788lemma equivalent_step_cons : ∀A,l1,l2. iso_step_lset A l1 l2 → ∀x. iso_step_lset A (x :: l1) (x :: l2).
789#A #l1 #l2 * // qed. (* That // was impressive. *)
790
791lemma lset_eq_concrete_cons : ∀A,l1,l2. lset_eq_concrete A l1 l2 → ∀x. lset_eq_concrete A (x :: l1) (x :: l2).
792#A #l1 #l2 #Hequiv elim Hequiv try //
793#a #b #c #Hab #Hbc #Hind #x %1{(equivalent_step_cons ??? Hab x) (Hind x)}
794qed.
795
796lemma absurd_list_eq_append : ∀A.∀x.∀l1,l2:list A. [ ] = l1 @ [x] @ l2 → False.
797#A #x #l1 #l2 elim l1 normalize
798[ 1: #Habsurd destruct
799| 2: #hd #tl #_ #Habsurd destruct
800] qed.
801
802(* Inversion lemma for emptyness, step case *)
803lemma equivalent_iso_step_empty_inv : ∀A,l. iso_step_lset A l [] → l = [ ].
804#A #l elim l //
805#hd #tl #Hind #H inversion H
806[ 1: #a #x #b #y #c #_ #Habsurd
807      @(False_ind … (absurd_list_eq_append ? y … Habsurd))
808| 2: #a #x #b #_ #Habsurd
809      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
810| 3: #a #x #b #_ #Habsurd
811      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
812] qed.
813
814(* Same thing for non-emptyness *)
815lemma equivalent_iso_step_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → iso_step_lset A l1 l2 → l2 ≠ [ ].
816#A #l1 elim l1
817[ 1: #l2 * #H @(False_ind … (H (refl ??)))
818| 2: #hd #tl #H #l2 #_ #Hstep % #Hl2 >Hl2 in Hstep; #Hstep
819     lapply (equivalent_iso_step_empty_inv … Hstep) #Habsurd destruct
820] qed.
821
822lemma lset_eq_concrete_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → lset_eq_concrete A l1 l2 → l2 ≠ [ ].
823#A #l1 #l2 #Hl1 #H lapply Hl1 elim H
824[ 2: #a #H @H
825| 1: #a #b #c #Hab #Hbc #H #Ha lapply (equivalent_iso_step_cons_inv … Ha Hab) #Hb @H @Hb
826] qed.
827
828lemma lset_eq_concrete_empty_inv : ∀A,l1,l2. l1 = [ ] → lset_eq_concrete A l1 l2 → l2 = [ ].
829#A #l1 #l2 #Hl1 #H lapply Hl1 elim H //
830#a #b #c #Hab #Hbc #Hbc_eq #Ha >Ha in Hab; #H_b lapply (equivalent_iso_step_empty_inv … ?? (symmetric_step … H_b))
831#Hb @Hbc_eq @Hb
832qed.
833
834(* Square equivalence diagram *)
835lemma square_lset_eq_concrete :
836  ∀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'.
837#A #a #b #a' #b' #H1 #H2 #H3
838@(transitive_lset_eq_concrete ???? (symmetric_lset_eq_concrete … H2))
839@(transitive_lset_eq_concrete ???? H1)
840@H3
841qed.
842
843(* Make the transposition of elements visible at top-level *)
844lemma transpose_lset_eq_concrete :
845  ∀A. ∀x,y,a,b,c,a',b',c'.
846  lset_eq_concrete A (a @ [x] @ b @ [y] @ c) (a' @ [x] @ b' @ [y] @ c') →
847  lset_eq_concrete A (a @ [y] @ b @ [x] @ c) (a' @ [y] @ b' @ [x] @ c').
848#A #x #y #a #b #c #a' #b' #c
849#H @(square_lset_eq_concrete ????? H) /2 by lset_trans, lset_refl, lset_transpose/
850qed.
851
852lemma switch_lset_eq_concrete :
853  ∀A. ∀a,b,c. lset_eq_concrete A (a@[b]@c) ([b]@a@c).
854#A #a elim a //
855#hda #tla #Hind #b #c lapply (Hind hda c) #H
856lapply (lset_eq_concrete_cons … H b)
857#H' normalize in H' ⊢ %; @symmetric_lset_eq_concrete
858/3 by lset_transpose, lset_trans, symmetric_lset_eq_concrete/
859qed.
860
861(* Folding a commutative and idempotent function on equivalent sets yields the same result. *)
862lemma lset_eq_concrete_fold :
863  ∀A : DeqSet.
864  ∀acctype : Type[0].
865  ∀l1,l2 : list (carr A).
866  lset_eq_concrete A l1 l2 →
867  ∀f:carr A → acctype → acctype.
868  (∀x1,x2. ∀acc. f x1 (f x2 acc) = f x2 (f x1 acc)) →
869  (∀x.∀acc. f x (f x acc) = f x acc) →
870  ∀acc. foldr ?? f acc l1 = foldr ?? f acc l2.
871#A #acctype #l1 #l2 #Heq #f #Hcomm #Hidem
872elim Heq
873try //
874#a' #b' #c' #Hstep #Hbc #H #acc <H -H
875elim Hstep
876[ 1: #a #x #b #y #c
877     >fold_append >fold_append >fold_append >fold_append
878     >fold_append >fold_append >fold_append >fold_append
879     normalize
880     cut (f x (foldr A acctype f (f y (foldr A acctype f acc c)) b) =
881          f y (foldr A acctype f (f x (foldr A acctype f acc c)) b)) [   
882     elim c
883     [ 1: normalize elim b
884          [ 1: normalize >(Hcomm x y) @refl
885          | 2: #hdb #tlb #Hind normalize
886               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ]
887     | 2: #hdc #tlc #Hind normalize elim b
888          [ 1: normalize >(Hcomm x y) @refl
889          | 2: #hdb #tlb #Hind normalize
890               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] ]
891     ]
892     #Hind >Hind @refl
893| 2: #a #x #b
894     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
895     normalize >Hidem @refl
896| 3: #a #x #b
897     >fold_append  >(fold_append ?? ([x]@[x])) >fold_append >fold_append
898     normalize >Hidem @refl
899] qed.
900
901(* Folding over equivalent sets yields equivalent results, for any equivalence. *)
902lemma inj_to_fold_inj :
903  ∀A,acctype : Type[0].
904  ∀eqrel : acctype → acctype → Prop.
905  ∀refl_eqrel  : reflexive ? eqrel.
906  ∀trans_eqrel : transitive ? eqrel.
907  ∀sym_eqrel   : symmetric ? eqrel.
908  ∀f           : A → acctype → acctype.
909  (∀x:A.∀acc1:acctype.∀acc2:acctype.eqrel acc1 acc2→eqrel (f x acc1) (f x acc2)) →
910  ∀l : list A. ∀acc1, acc2 : acctype. eqrel acc1 acc2 → eqrel (foldr … f acc1 l) (foldr … f acc2 l).
911#A #acctype #eqrel #R #T #S #f #Hinj #l elim l
912//
913#hd #tl #Hind #acc1 #acc2 #Heq normalize @Hinj @Hind @Heq
914qed.
915
916(* We need to extend the above proof to arbitrary equivalence relation instead of
917   just standard equality. *)
918lemma lset_eq_concrete_fold_ext :
919  ∀A : DeqSet.
920  ∀acctype : Type[0].
921  ∀eqrel : acctype → acctype → Prop.
922  ∀refl_eqrel  : reflexive ? eqrel.
923  ∀trans_eqrel : transitive ? eqrel.
924  ∀sym_eqrel   : symmetric ? eqrel.
925  ∀f:carr A → acctype → acctype.
926  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
927  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
928  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
929  ∀l1,l2 : list (carr A).
930  lset_eq_concrete A l1 l2 → 
931  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
932#A #acctype #eqrel #R #T #S #f #Hinj #Hcomm #Hidem #l1 #l2 #Heq
933elim Heq
934try //
935#a' #b' #c' #Hstep #Hbc #H inversion Hstep
936[ 1: #a #x #b #y #c #HlA #HlB #_ #acc
937     >HlB in H; #H @(T … ? (H acc))
938     >fold_append >fold_append >fold_append >fold_append
939     >fold_append >fold_append >fold_append >fold_append
940     normalize
941     cut (eqrel (f x (foldr ? acctype f (f y (foldr ? acctype f acc c)) b))
942                (f y (foldr ? acctype f (f x (foldr ? acctype f acc c)) b)))
943     [ 1:
944     elim c
945     [ 1: normalize elim b
946          [ 1: normalize @(Hcomm x y)
947          | 2: #hdb #tlb #Hind normalize
948               lapply (Hinj hdb ?? Hind) #Hind'
949               lapply (T … Hind' (Hcomm ???)) #Hind''
950               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
951     | 2: #hdc #tlc #Hind normalize elim b
952          [ 1: normalize @(Hcomm x y)
953          | 2: #hdb #tlb #Hind normalize
954               lapply (Hinj hdb ?? Hind) #Hind'
955               lapply (T … Hind' (Hcomm ???)) #Hind''
956               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
957     ] ]
958     #Hind @(inj_to_fold_inj … eqrel R T S ? Hinj … Hind)
959| 2: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
960     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
961     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @S @Hidem
962| 3: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
963     >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append
964     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @Hidem
965] qed.
966
967(* Prepare some well-founded induction principles on lists. The idea is to perform
968   an induction on the sequence of filterees of a list : taking the first element,
969   filtering it out of the tail, etc. We give such principles for pairs of lists
970   and isolated lists.  *)
971
972(* The two lists [l1,l2] share at least the head of l1. *)
973definition head_shared ≝ λA. λl1,l2 : list A.
974match l1 with
975[ nil ⇒ l2 = (nil ?)
976| cons hd _ ⇒  mem … hd l2
977].
978
979(* Relation on pairs of lists, as described above. *)
980definition filtered_lists : ∀A:DeqSet. relation (list (carr A)×(list (carr A))) ≝
981λA:DeqSet. λll1,ll2.
982let 〈la1,lb1〉 ≝ ll1 in
983let 〈la2,lb2〉 ≝ ll2 in
984match la2 with
985[ nil ⇒ False
986| cons hda2 tla2 ⇒
987    head_shared ? la2 lb2 ∧
988    la1 = filter … (λx.¬(x==hda2)) tla2 ∧
989    lb1 = filter … (λx.¬(x==hda2)) lb2
990].
991
992(* Notice the absence of plural : this relation works on a simple list, not a pair. *)
993definition filtered_list : ∀A:DeqSet. relation (list (carr A)) ≝
994λA:DeqSet. λl1,l2.
995match l2 with
996[ nil ⇒ False
997| cons hd2 tl2 ⇒
998    l1 = filter … (λx.¬(x==hd2)) l2
999].
1000
1001(* Relation on lists based on their lengths. We know this one is well-founded. *)
1002definition length_lt : ∀A:DeqSet. relation (list (carr A)) ≝
1003λA:DeqSet. λl1,l2. lt (length ? l1) (length ? l2).
1004
1005(* length_lt can be extended on pairs by just measuring the first component *)
1006definition length_fst_lt : ∀A:DeqSet. relation (list (carr A) × (list (carr A))) ≝
1007λA:DeqSet. λll1,ll2. lt (length ? (\fst ll1)) (length ? (\fst ll2)).
1008
1009lemma filter_length : ∀A. ∀l. ∀f. |filter A f l| ≤ |l|.
1010#A #l #f elim l //
1011#hd #tl #Hind whd in match (filter ???); cases (f hd) normalize nodelta
1012[ 1: /2 by le_S_S/
1013| 2: @le_S @Hind
1014] qed.
1015
1016(* The order on lists defined by their length is wf *)
1017lemma length_lt_wf : ∀A. ∀l. WF (list (carr A)) (length_lt A) l.
1018#A #l % elim l
1019[ 1: #a normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1020| 2: #hd #tl #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1021@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1022qed.
1023
1024(* Order on pairs of list by measuring the first proj *)
1025lemma length_fst_lt_wf : ∀A. ∀ll. WF ? (length_fst_lt A) ll.
1026#A * #l1 #l2 % elim l1
1027[ 1: * #a1 #a2 normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
1028| 2: #hd1 #tl1 #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
1029@(transitive_le … Hlt') @(monotonic_pred … Hlt)
1030qed.
1031
1032lemma length_to_filtered_lists : ∀A. subR ? (filtered_lists A) (length_fst_lt A).
1033#A whd * #a1 #a2 * #b1 #b2 elim b1
1034[ 1: @False_ind
1035| 2: #hd1 #tl1 #Hind whd in ⊢ (% → ?); * * #Hmem #Ha1 #Ha2 whd
1036     >Ha1 whd in match (length ??) in ⊢ (??%); @le_S_S @filter_length
1037] qed.
1038
1039lemma length_to_filtered_list : ∀A. subR ? (filtered_list A) (length_lt A).
1040#A whd #a #b elim b
1041[ 1: @False_ind
1042| 2: #hd #tl #Hind whd in ⊢ (% → ?); whd in match (filter ???);
1043     lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?);
1044     normalize nodelta #Ha whd @le_S_S >Ha @filter_length ]
1045qed.
1046
1047(* Prove well-foundedness by embedding in lt *)
1048lemma filtered_lists_wf : ∀A. ∀ll. WF ? (filtered_lists A) ll.
1049#A #ll @(WF_antimonotonic … (length_to_filtered_lists A)) @length_fst_lt_wf
1050qed.
1051
1052lemma filtered_list_wf : ∀A. ∀l. WF ? (filtered_list A) l.
1053#A #l @(WF_antimonotonic … (length_to_filtered_list A)) @length_lt_wf
1054qed.
1055
1056definition Acc_elim : ∀A,R,x. WF A R x → (∀a. R a x → WF A R a) ≝
1057λA,R,x,acc.
1058match acc with
1059[ wf _ a0 ⇒ a0 ].
1060
1061(* Stolen from Coq. Warped to avoid prop-to-type restriction. *)
1062let rec WF_rect
1063  (A : Type[0])
1064  (R : A → A → Prop)
1065  (P : A → Type[0])
1066  (f : ∀ x : A.
1067       (∀ y : A. R y x → WF ? R y) →
1068       (∀ y : A. R y x → P y) → P x)
1069  (x : A)
1070  (a : WF A R x) on a : P x ≝
1071f x (Acc_elim … a) (λy:A. λRel:R y x. WF_rect A R P f y ((Acc_elim … a) y Rel)).
1072
1073lemma lset_eq_concrete_filter : ∀A:DeqSet.∀tl.∀hd.
1074  lset_eq_concrete A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
1075#A #tl elim tl
1076[ 1: #hd //
1077| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
1078     lapply (eqb_true A hd' hd)
1079     cases (hd'==hd)
1080     [ 2: #_ normalize in match (notb false); normalize nodelta
1081          >cons_to_append >(cons_to_append … hd')
1082          >cons_to_append in ⊢ (???%); >(cons_to_append … hd') in ⊢ (???%);
1083          @(transpose_lset_eq_concrete ? hd' hd [ ] [ ] (filter A (λy:A.¬y==hd) tl') [ ] [ ] tl')
1084          >nil_append >nil_append >nil_append >nil_append
1085          @lset_eq_concrete_cons >nil_append >nil_append
1086          @Hind
1087    | 1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta
1088         >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));
1089         @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))
1090         [ 1: @Hind
1091         | 2: %2
1092         | 3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]
1093    ]
1094] qed.
1095
1096
1097(* The "abstract", observational definition of set equivalence implies the concrete one. *)
1098
1099lemma lset_eq_to_lset_eq_concrete_aux :
1100  ∀A,ll.
1101    head_shared … (\fst ll) (\snd ll) →
1102    lset_eq (carr A) (\fst ll) (\snd ll) →
1103    lset_eq_concrete A (\fst ll) (\snd ll).
1104#A #ll @(WF_ind ????? (filtered_lists_wf A ll))
1105* *
1106[ 1: #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hb2 >Hb2 #_ %2
1107| 2: #hd1 #tl1 #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hmem
1108     lapply (list_mem_split ??? Hmem) * #l2A * #l2B #Hb2 #Heq
1109     destruct
1110     lapply (Hind_wf 〈filter … (λx.¬x==hd1) tl1,filter … (λx.¬x==hd1) (l2A@l2B)〉)
1111     cut (filtered_lists A 〈filter A (λx:A.¬x==hd1) tl1,filter A (λx:A.¬x==hd1) (l2A@l2B)〉 〈hd1::tl1,l2A@[hd1]@l2B〉)
1112     [ @conj try @conj try @refl whd
1113       [ 1: /2 by /
1114       | 2: >filter_append in ⊢ (???%); >filter_append in ⊢ (???%);
1115            whd in match (filter ?? [hd1]);
1116            elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1117            normalize nodelta <filter_append @refl ] ]
1118     #Hfiltered #Hind_aux lapply (Hind_aux Hfiltered) -Hind_aux
1119     cut (lset_eq A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1120     [ 1: lapply (lset_eq_filter_monotonic … Heq hd1)
1121          >filter_cons_unfold >filter_append >(filter_append … [hd1])
1122          whd in match (filter ?? [hd1]);
1123          elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
1124          normalize nodelta <filter_append #Hsol @Hsol ]
1125     #Hset_eq
1126     cut (head_shared A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
1127     [ 1: lapply Hset_eq cases (filter A (λx:A.¬x==hd1) tl1)
1128          [ 1: whd in ⊢ (% → ?); * #_ elim (filter A (λx:A.¬x==hd1) (l2A@l2B)) //
1129               #hd' #tl' normalize #Hind * @False_ind
1130          | 2: #hd' #tl' * #Hincl1 #Hincl2 whd elim Hincl1 #Hsol #_ @Hsol ] ]
1131     #Hshared #Hind_aux lapply (Hind_aux Hshared Hset_eq)
1132     #Hconcrete_set_eq
1133     >cons_to_append
1134     @(transitive_lset_eq_concrete ? ([hd1]@tl1) ([hd1]@l2A@l2B) (l2A@[hd1]@l2B))
1135     [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete ]
1136     lapply (lset_eq_concrete_cons … Hconcrete_set_eq hd1) #Hconcrete_cons_eq
1137     @(square_lset_eq_concrete … Hconcrete_cons_eq)
1138     [ 1: @(lset_eq_concrete_filter ? tl1 hd1)
1139     | 2: @(lset_eq_concrete_filter ? (l2A@l2B) hd1) ]
1140] qed.
1141
1142lemma lset_eq_to_lset_eq_concrete : ∀A,l1,l2. lset_eq (carr A) l1 l2 → lset_eq_concrete A l1 l2.
1143#A *
1144[ 1: #l2 #Heq >(lset_eq_empty_inv … (symmetric_lset_eq … Heq)) //
1145| 2: #hd1 #tl1 #l2 #Hincl lapply Hincl lapply (lset_eq_to_lset_eq_concrete_aux ? 〈hd1::tl1,l2〉) #H @H
1146     whd elim Hincl * //
1147] qed.
1148
1149
1150(* The concrete one implies the abstract one. *)
1151lemma lset_eq_concrete_to_lset_eq : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq A l1 l2.
1152#A #l1 #l2 #Hconcrete
1153elim Hconcrete try //
1154#a #b #c #Hstep #Heq_bc_concrete #Heq_bc
1155cut (lset_eq A a b)
1156[ 1: elim Hstep
1157     [ 1: #a' elim a'
1158          [ 2: #hda #tla #Hind #x #b' #y #c' >cons_to_append
1159               >(associative_append ? [hda] tla ?)
1160               >(associative_append ? [hda] tla ?)
1161               @cons_monotonic_eq >nil_append >nil_append @Hind
1162          | 1: #x #b' #y #c' >nil_append >nil_append
1163               elim b' try //
1164               #hdb #tlc #Hind >append_cons >append_cons in ⊢ (???%);
1165               >associative_append >associative_append
1166               lapply (cons_monotonic_eq … Hind hdb) #Hind'               
1167               @(transitive_lset_eq ? ([x]@[hdb]@tlc@[y]@c') ([hdb]@[x]@tlc@[y]@c'))
1168               /2 by transitive_lset_eq/ ]
1169     | 2: #a' elim a'
1170          [ 2: #hda #tla #Hind #x #b' >cons_to_append
1171               >(associative_append ? [hda] tla ?)
1172               >(associative_append ? [hda] tla ?)
1173               @cons_monotonic_eq >nil_append >nil_append @Hind
1174          | 1: #x #b' >nil_append >nil_append @conj normalize
1175               [ 1: @conj [ 1: %1 @refl ] elim b'
1176                    [ 1: @I
1177                    | 2: #hdb #tlb #Hind normalize @conj
1178                         [ 1: %2 %2 %1 @refl
1179                         | 2: @(All_mp … Hind) #a0 *
1180                              [ 1: #Heq %1 @Heq
1181                              | 2: * /2 by or_introl, or_intror/ ] ] ]
1182                    #H %2 %2 %2 @H
1183               | 2: @conj try @conj try /2 by or_introl, or_intror/ elim b'
1184                    [ 1: @I
1185                    | 2: #hdb #tlb #Hind normalize @conj
1186                         [ 1: %2 %1 @refl
1187                         | 2: @(All_mp … Hind) #a0 *
1188                              [ 1: #Heq %1 @Heq
1189                              | 2: #H %2 %2 @H ] ] ] ] ]
1190     | 3: #a #x #b elim a try @lset_eq_contract
1191          #hda #tla #Hind @cons_monotonic_eq @Hind ] ]
1192#Heq_ab @(transitive_lset_eq … Heq_ab Heq_bc)
1193qed.
1194
1195lemma lset_eq_fold :
1196  ∀A : DeqSet.
1197  ∀acctype : Type[0].
1198  ∀eqrel : acctype → acctype → Prop.
1199  ∀refl_eqrel  : reflexive ? eqrel.
1200  ∀trans_eqrel : transitive ? eqrel.
1201  ∀sym_eqrel   : symmetric ? eqrel.
1202  ∀f:carr A → acctype → acctype.
1203  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
1204  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
1205  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
1206  ∀l1,l2 : list (carr A).
1207  lset_eq A l1 l2 → 
1208  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
1209#A #acctype #eqrel #refl_eqrel #trans_eqrel #sym_eqrel #f #Hinj #Hsym #Hcontract #l1 #l2 #Heq #acc
1210lapply (lset_eq_to_lset_eq_concrete … Heq) #Heq_concrete
1211@(lset_eq_concrete_fold_ext A acctype eqrel refl_eqrel trans_eqrel sym_eqrel f Hinj Hsym Hcontract l1 l2 Heq_concrete acc)
1212qed.
1213
1214
1215
Note: See TracBrowser for help on using the repository browser.