Changeset 2386


Ignore:
Timestamp:
Oct 3, 2012, 1:26:48 PM (7 years ago)
Author:
garnier
Message:

Implementation of constructive finite sets based on lists. Various other stuff.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2332 r2386  
    1 (* Various small results used in at least two files in the front-end. *)
     1(* Various small homeless results. *)
    22
    33include "Clight/TypeComparison.ma".
    44include "common/Pointers.ma".
     5include "basics/jmeq.ma".
     6include "basics/star.ma". (* well-founded relations *)
     7include "basics/lists/listb.ma".
     8include "basics/lists/list.ma".
     9
     10
     11(* --------------------------------------------------------------------------- *)
     12(* Misc. *)
     13(* --------------------------------------------------------------------------- *)
    514
    615lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
     
    2231| 2: #Hneq' normalize // ] qed.
    2332
    24 (* useful facts on various boolean operations *)
     33lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
     34
     35(* --------------------------------------------------------------------------- *)
     36(* Useful facts on various boolean operations. *)
     37(* --------------------------------------------------------------------------- *)
     38 
    2539lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
    2640lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
     
    3044lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
    3145
    32 (* useful facts on block *)
    33 lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
    34 #b1 #b2 #Hneq
    35 @(eq_block_elim … b1 b2)
    36 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
    37 | 2: #_ @refl ] qed.
    38 
    39 lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false.
    40 #b1 #b2 #Hneq
    41 @(eq_block_elim … b1 b2)
    42 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
    43 | 2: #_ @refl ] qed.
    44 
    45 (* useful facts on Z *)
     46(* --------------------------------------------------------------------------- *)
     47(* Useful facts on Z. *)
     48(* --------------------------------------------------------------------------- *)
     49
    4650lemma Zltb_to_Zleb_true : ∀a,b. Zltb a b = true → Zleb a b = true.
    4751#a #b #Hltb lapply (Zltb_true_to_Zlt … Hltb) #Hlt @Zle_to_Zleb_true
     
    126130/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
    127131qed.
     132
     133(* follows from (0 ≤ a < b → mod a b = a) *)
     134axiom Z_of_unsigned_bitvector_of_small_Z :
     135  ∀z. OZ ≤ z → z < Z_two_power_nat 16 → Z_of_unsigned_bitvector 16 (bitvector_of_Z 16 z) = z.
     136
     137theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p.
     138#n #m #p #Hle #Hlt /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle, transitive_Zle/
     139qed.
     140
     141(* --------------------------------------------------------------------------- *)
     142(* Useful facts on blocks. *)
     143(* --------------------------------------------------------------------------- *)
     144
     145lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
     146#b1 #b2 #Hneq
     147@(eq_block_elim … b1 b2)
     148[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
     149| 2: #_ @refl ] qed.
     150
     151lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false.
     152#b1 #b2 #Hneq
     153@(eq_block_elim … b1 b2)
     154[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
     155| 2: #_ @refl ] qed.
     156
     157definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_block ?.
     158* #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2)
     159[ 1: #Heq >Heq cases r1 cases r2 normalize
     160     >eqZb_z_z normalize try // @conj #H destruct (H)
     161     try @refl
     162| 2: #Hneq cases r1 cases r2 normalize
     163     >(eqZb_false … Hneq) normalize @conj
     164     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
     165] qed.
     166
     167(* --------------------------------------------------------------------------- *)
     168(* General results on lists. *)
     169(* --------------------------------------------------------------------------- *)
     170
     171(* If mem succeeds in finding an element, then the list can be partitioned around this element. *)
     172lemma list_mem_split : ∀A. ∀l : list A. ∀x : A. mem … x l → ∃l1,l2. l = l1 @ [x] @ l2.
     173#A #l elim l
     174[ 1: normalize #x @False_ind
     175| 2: #hd #tl #Hind #x whd in ⊢ (% → ?); *
     176     [ 1: #Heq %{(nil ?)} %{tl} destruct @refl
     177     | 2: #Hmem lapply (Hind … Hmem) * #l1 * #l2 #Heq_tl >Heq_tl
     178          %{(hd :: l1)} %{l2} @refl
     179     ]
     180] qed.
     181
     182lemma cons_to_append : ∀A. ∀hd : A. ∀l : list A. hd :: l = [hd] @ l. #A #hd #l @refl qed.
     183
     184lemma fold_append :
     185  ∀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.
     186#A #B #l1 elim l1 //
     187#hd #tl #Hind #l2 #f #seed normalize >Hind @refl
     188qed.
     189
     190lemma filter_append : ∀A:Type[0]. ∀l1,l2 : list A. ∀f. filter ? f (l1 @ l2) = (filter ? f l1) @ (filter ? f l2).
     191#A #l1 elim l1 //
     192#hd #tl #Hind #l2 #f
     193>cons_to_append >associative_append
     194normalize cases (f hd) normalize
     195<Hind @refl
     196qed.
     197
     198lemma filter_cons_unfold : ∀A:Type[0]. ∀f. ∀hd,tl.
     199  filter ? f (hd :: tl) =
     200  if f hd then
     201    (hd :: filter A f tl)
     202  else
     203    (filter A f tl).
     204#A #f #hd #tl elim tl // qed.
     205
     206
     207lemma filter_elt_empty : ∀A:DeqSet. ∀elt,l. filter (carr A) (λx.¬(x==elt)) l = [ ] → All (carr A) (λx. x = elt) l.
     208#A #elt #l elim l
     209[ 1: //
     210| 2: #hd #tl #Hind >filter_cons_unfold
     211     lapply (eqb_true A hd elt)
     212     cases (hd==elt) normalize nodelta
     213     [ 2: #_ #Habsurd destruct
     214     | 1: * #H1 #H2 #Heq lapply (Hind Heq) #Hall whd @conj //
     215          @H1 @refl
     216     ]
     217] qed.
     218
     219lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed.
     220
     221lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2).
     222#A #elt #l1 elim l1
     223[ 1: #l2 normalize @conj [ 1: #H %2 @H | 2: * [ 1: @False_ind | 2: #H @H ] ]
     224| 2: #hd #tl #Hind #l2 @conj
     225     [ 1: whd in match (mem ???); *
     226          [ 1: #Heq >Heq %1 normalize %1 @refl
     227          | 2: #H1 lapply (Hind l2) * #HA #HB normalize
     228               elim (HA H1)
     229               [ 1: #H %1 %2 assumption | 2: #H %2 assumption ]
     230          ]
     231     | 2: normalize *
     232          [ 1: * /2 by or_introl, or_intror/
     233               #H %2 elim (Hind l2) #_ #H' @H' %1 @H
     234          | 2: #H %2 elim (Hind l2) #_ #H' @H' %2 @H ]
     235     ]
     236] qed.
     237
     238lemma mem_append_forward : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) → (mem … elt l1) ∨ (mem … elt l2).
     239#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #H' #_ @H' @H qed.
     240
     241lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) .
     242#A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed.
     243
     244(* --------------------------------------------------------------------------- *)
     245(* Generic properties of equivalence relations *)
     246(* --------------------------------------------------------------------------- *)
     247
     248lemma triangle_diagram :
     249  ∀acctype : Type[0].
     250  ∀eqrel : acctype → acctype → Prop.
     251  ∀refl_eqrel  : reflexive ? eqrel.
     252  ∀trans_eqrel : transitive ? eqrel.
     253  ∀sym_eqrel   : symmetric ? eqrel.
     254  ∀a,b,c. eqrel a b → eqrel a c → eqrel b c.
     255#acctype #eqrel #R #T #S #a #b #c
     256#H1 #H2 @(T … (S … H1) H2)
     257qed.
     258
     259lemma cotriangle_diagram :
     260  ∀acctype : Type[0].
     261  ∀eqrel : acctype → acctype → Prop.
     262  ∀refl_eqrel  : reflexive ? eqrel.
     263  ∀trans_eqrel : transitive ? eqrel.
     264  ∀sym_eqrel   : symmetric ? eqrel.
     265  ∀a,b,c. eqrel b a → eqrel c a → eqrel b c.
     266#acctype #eqrel #R #T #S #a #b #c
     267#H1 #H2 @S @(T … H2 (S … H1))
     268qed.
     269
     270(* --------------------------------------------------------------------------- *)
     271(* Quick and dirty implementation of finite sets relying on lists. The
     272 * implementation is split in two: an abstract equivalence defined using inclusion
     273 * of lists, and a concrete one where equivalence is defined as the closure of
     274 * duplication, contraction and transposition of elements. We rely on the latter
     275 * to prove stuff on folds over sets.  *)
     276(* --------------------------------------------------------------------------- *)
     277
     278definition lset ≝ λA:Type[0]. list A.
     279
     280(* The empty set. *)
     281definition empty_lset ≝ λA:Type[0]. nil A.
     282
     283(* Standard operations. *)
     284definition lset_union ≝ λA:Type[0].λl1,l2 : lset A. l1 @ l2.
     285
     286definition lset_remove ≝ λA:DeqSet.λl:lset (carr A).λelt:carr A. (filter … (λx.¬x==elt) l).
     287
     288definition lset_difference ≝ λA:DeqSet.λl1,l2:lset (carr A). (filter … (λx.¬ (memb ? x l2)) l1).
     289
     290(* Standard predicates on sets *)
     291definition lset_in ≝ λA:Type[0].λx : A. λl : lset A. mem … x l.
     292
     293definition lset_disjoint ≝ λA:Type[0].λl1, l2 : lset A.
     294  ∀x,y. mem … x l1 → mem … y l2 → x ≠ y.
     295 
     296definition lset_inclusion ≝ λA:Type[0].λl1,l2.
     297  All A (λx1. mem … x1 l2) l1.
     298
     299(* Definition of abstract set equivalence. *)
     300definition lset_eq ≝ λA:Type[0].λl1,l2.
     301  lset_inclusion A l1 l2 ∧
     302  lset_inclusion A l2 l1.
     303
     304(* Properties of inclusion. *) 
     305lemma reflexive_lset_inclusion : ∀A. ∀l. lset_inclusion A l l.
     306#A #l elim l try //
     307#hd #tl #Hind whd @conj
     308[ 1: %1 @refl
     309| 2: whd in Hind; @(All_mp … Hind)
     310     #a #H whd %2 @H
     311] qed.
     312
     313lemma transitive_lset_inclusion : ∀A. ∀l1,l2,l3. lset_inclusion A l1 l2 → lset_inclusion A l2 l3 → lset_inclusion A l1 l3 .
     314#A #l1 #l2 #l3
     315#Hincl1 #Hincl2 @(All_mp … Hincl1)
     316whd in Hincl2;
     317#a elim l2 in Hincl2;
     318[ 1: normalize #_ @False_ind
     319| 2: #hd #tl #Hind whd in ⊢ (% → ?);
     320     * #Hmem #Hincl_tl whd in ⊢ (% → ?);
     321     * [ 1: #Heq destruct @Hmem
     322       | 2: #Hmem_tl @Hind assumption ]
     323] qed.
     324
     325lemma cons_preserves_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A l1 (x::l2).
     326#A #l1 #l2 #Hincl #x @(All_mp … Hincl) #a #Hmem whd %2 @Hmem qed.
     327
     328lemma cons_monotonic_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A (x::l1) (x::l2).
     329#A #l1 #l2 #Hincl #x whd @conj
     330[ 1: /2 by or_introl/
     331| 2: @(All_mp … Hincl) #a #Hmem whd %2 @Hmem ] qed.
     332
     333lemma lset_inclusion_concat : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A l1 (l3 @ l2).
     334#A #l1 #l2 #Hincl #l3 elim l3
     335try /2 by cons_preserves_inclusion/
     336qed.
     337
     338lemma lset_inclusion_concat_monotonic : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A (l3 @ l1) (l3 @ l2).
     339#A #l1 #l2 #Hincl #l3 elim l3
     340try @Hincl #hd #tl #Hind @cons_monotonic_inclusion @Hind
     341qed.
     342 
     343(* lset_eq is an equivalence relation. *)
     344lemma reflexive_lset_eq : ∀A. ∀l. lset_eq A l l. /2 by conj/ qed.
     345
     346lemma transitive_lset_eq : ∀A. ∀l1,l2,l3. lset_eq A l1 l2 → lset_eq A l2 l3 → lset_eq A l1 l3.
     347#A #l1 #l2 #l3 * #Hincl1 #Hincl2 * #Hincl3 #Hincl4
     348@conj @(transitive_lset_inclusion ??l2) assumption
     349qed.
     350
     351lemma symmetric_lset_eq : ∀A. ∀l1,l2. lset_eq A l1 l2 → lset_eq A l2 l1.
     352#A #l1 #l2 * #Hincl1 #Hincl2 @conj assumption
     353qed.
     354
     355(* Properties of inclusion vs union and equality. *)
     356lemma lset_union_inclusion : ∀A:Type[0]. ∀a,b,c. 
     357  lset_inclusion A a c → lset_inclusion ? b c → lset_inclusion ? (lset_union ? a b) c.
     358#A #a #b #c #H1 #H2 whd whd in match (lset_union ???);
     359@All_append assumption qed.
     360
     361lemma lset_inclusion_union : ∀A:Type[0]. ∀a,b,c. 
     362  lset_inclusion A a b ∨ lset_inclusion A a c → lset_inclusion ? a (lset_union ? b c).
     363#A #a #b #c *
     364[ 1: @All_mp #elt #Hmem @mem_append_backwards %1 @Hmem
     365| 2: @All_mp #elt #Hmem @mem_append_backwards %2 @Hmem
     366] qed.
     367
     368lemma lset_inclusion_eq : ∀A : Type[0]. ∀a,b,c : lset A.
     369  lset_eq ? a b → lset_inclusion ? b c → lset_inclusion ? a c.
     370#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H1 H3)
     371qed.
     372
     373lemma lset_inclusion_eq2 : ∀A : Type[0]. ∀a,b,c : lset A.
     374  lset_eq ? b c → lset_inclusion ? a b → lset_inclusion ? a c.
     375#A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H3 H1)
     376qed.
     377
     378(* Properties of lset_eq and mem *)
     379lemma lset_eq_mem :
     380  ∀A:Type[0].
     381  ∀s1,s2 : lset A.
     382  lset_eq ? s1 s2 →
     383  ∀b.mem ? b s1 → mem ? b s2.
     384#A #s1 #s2 * #Hincl12 #_ #b
     385whd in Hincl12; elim s1 in Hincl12;
     386[ 1: normalize #_ *
     387| 2: #hd #tl #Hind whd in ⊢ (% → % → ?); * #Hmem' #Hall * #Heq
     388     [ 1: destruct (Heq) assumption
     389     | 2: @Hind assumption ]
     390] qed.
     391
     392lemma lset_eq_memb :
     393  ∀A : DeqSet.
     394  ∀s1,s2 : lset (carr A).
     395  lset_eq ? s1 s2 →
     396  ∀b.memb ? b s1 = true → memb ? b s2 = true.
     397#A #s1 #s2 #Heq #b
     398lapply (memb_to_mem A s1 b) #H1 #H2
     399lapply (H1 H2) #Hmem lapply (lset_eq_mem … Heq ? Hmem) @mem_to_memb
     400qed.
     401
     402lemma lset_eq_memb_eq :
     403  ∀A : DeqSet.
     404  ∀s1,s2 : lset (carr A).
     405  lset_eq ? s1 s2 →
     406  ∀b.memb ? b s1 = memb ? b s2.
     407#A #s1 #s2 #Hlset_eq #b
     408lapply (lset_eq_memb … Hlset_eq b)
     409lapply (lset_eq_memb … (symmetric_lset_eq … Hlset_eq) b) 
     410cases (b∈s1)
     411[ 1: #_ #H lapply (H (refl ??)) #Hmem >H @refl
     412| 2: cases (b∈s2) // #H lapply (H (refl ??)) #Habsurd destruct
     413] qed.
     414
     415lemma lset_eq_filter_eq :
     416  ∀A : DeqSet.
     417  ∀s1,s2 : lset (carr A).
     418  lset_eq ? s1 s2 → 
     419  ∀l.
     420     (filter ? (λwb.¬wb∈s1) l) =
     421     (filter ? (λwb.¬wb∈s2) l).
     422#A #s1 #s2 #Heq #l elim l
     423[ 1: @refl
     424| 2: #hd #tl #Hind >filter_cons_unfold >filter_cons_unfold
     425      >(lset_eq_memb_eq … Heq) cases (hd∈s2)
     426      normalize in match (notb ?); normalize nodelta
     427      try @Hind >Hind @refl
     428] qed.
     429
     430lemma cons_monotonic_eq : ∀A. ∀l1,l2 : lset A. lset_eq A l1 l2 → ∀x. lset_eq A (x::l1) (x::l2).
     431#A #l1 #l2 #Heq #x cases Heq #Hincl1 #Hincl2
     432@conj
     433[ 1: @cons_monotonic_inclusion
     434| 2: @cons_monotonic_inclusion ]
     435assumption
     436qed.
     437
     438(* Properties of difference and remove *)
     439lemma lset_difference_unfold :
     440  ∀A : DeqSet.
     441  ∀s1, s2 : lset (carr A).
     442  ∀hd. lset_difference A (hd :: s1) s2 =
     443    if hd∈s2 then
     444      lset_difference A s1 s2
     445    else
     446      hd :: (lset_difference A s1 s2).
     447#A #s1 #s2 #hd normalize
     448cases (hd∈s2) @refl
     449qed.
     450
     451lemma lset_difference_unfold2 :
     452  ∀A : DeqSet.
     453  ∀s1, s2 : lset (carr A).
     454  ∀hd. lset_difference A s1 (hd :: s2) =
     455       lset_difference A (lset_remove ? s1 hd) s2.
     456#A #s1
     457elim s1
     458[ 1: //
     459| 2: #hd1 #tl1 #Hind #s2 #hd
     460     whd in match (lset_remove ???);
     461     whd in match (lset_difference A ??);
     462     whd in match (memb ???);
     463     lapply (eqb_true … hd1 hd)
     464     cases (hd1==hd) normalize nodelta
     465     [ 1: * #H #_ lapply (H (refl ??)) -H #H
     466           @Hind
     467     | 2: * #_ #Hguard >lset_difference_unfold
     468          cases (hd1∈s2) normalize in match (notb ?); normalize nodelta
     469          <Hind @refl ]
     470] qed.         
     471
     472lemma lset_difference_disjoint :
     473 ∀A : DeqSet.
     474 ∀s1,s2 : lset (carr A).
     475  lset_disjoint A s1 (lset_difference A s2 s1).
     476#A #s1 elim s1
     477[ 1: #s2 normalize #x #y *
     478| 2: #hd1 #tl1 #Hind #s2 >lset_difference_unfold2 #x #y
     479     whd in ⊢ (% → ?); *
     480     [ 2: @Hind
     481     | 1: #Heq >Heq elim s2
     482          [ 1: normalize *
     483          | 2: #hd2 #tl2 #Hind2 whd in match (lset_remove ???);
     484               lapply (eqb_true … hd2 hd1)
     485               cases (hd2 == hd1) normalize in match (notb ?); normalize nodelta * #H1 #H2
     486               [ 1: @Hind2
     487               | 2: >lset_difference_unfold cases (hd2 ∈ tl1) normalize nodelta try @Hind2
     488                     whd in ⊢ (% → ?); *
     489                     [ 1: #Hyhd2 destruct % #Heq lapply (H2 … (sym_eq … Heq)) #Habsurd destruct
     490                     | 2: @Hind2 ]
     491               ]
     492          ]
     493    ]
     494] qed.
     495
     496
     497lemma lset_remove_split : ∀A : DeqSet. ∀l1,l2 : lset A. ∀elt. lset_remove A (l1 @ l2) elt = (lset_remove … l1 elt) @ (lset_remove … l2 elt).
     498#A #l1 #l2 #elt /2 by filter_append/ qed.
     499
     500lemma lset_inclusion_remove :
     501  ∀A : DeqSet.
     502  ∀s1, s2 : lset A.
     503  lset_inclusion ? s1 s2 →
     504  ∀elt. lset_inclusion ? (lset_remove ? s1 elt) (lset_remove ? s2 elt).
     505#A #s1 elim s1
     506[ 1: normalize //
     507| 2: #hd1 #tl1 #Hind1 #s2 * #Hmem #Hincl
     508     elim (list_mem_split ??? Hmem) #s2A * #s2B #Hs2_eq destruct #elt
     509     whd in match (lset_remove ???);
     510     @(match (hd1 == elt)
     511       return λx. (hd1 == elt = x) → ?
     512       with
     513       [ true ⇒ λH. ?
     514       | false ⇒ λH. ? ] (refl ? (hd1 == elt))) normalize in match (notb ?);
     515     normalize nodelta
     516     [ 1:  @Hind1 @Hincl
     517     | 2: whd @conj
     518          [ 2: @(Hind1 … Hincl)
     519          | 1: >lset_remove_split >lset_remove_split
     520               normalize in match (lset_remove A [hd1] elt);
     521               >H normalize nodelta @mem_append_backwards %2
     522               @mem_append_backwards %1 normalize %1 @refl ]
     523     ]
     524] qed.
     525
     526lemma lset_difference_lset_eq :
     527  ∀A : DeqSet. ∀a,b,c.
     528   lset_eq A b c →
     529   lset_eq A (lset_difference A a b) (lset_difference A a c).
     530#A #a #b #c #Heq
     531whd in match (lset_difference ???) in ⊢ (??%%);   
     532elim a
     533[ 1: normalize @conj @I
     534| 2: #hda #tla #Hind whd in match (foldr ?????) in ⊢ (??%%);
     535     >(lset_eq_memb_eq … Heq hda) cases (hda∈c)
     536     normalize in match (notb ?); normalize nodelta
     537     try @Hind @cons_monotonic_eq @Hind
     538] qed.
     539
     540lemma lset_difference_lset_remove_commute :
     541  ∀A:DeqSet.
     542  ∀elt,s1,s2.
     543  (lset_difference A (lset_remove ? s1 elt) s2) =
     544  (lset_remove A (lset_difference ? s1 s2) elt).
     545#A #elt #s1 #s2
     546elim s1 try //
     547#hd #tl #Hind
     548>lset_difference_unfold
     549whd in match (lset_remove ???);
     550@(match (hd==elt) return λx. (hd==elt) = x → ?
     551  with
     552  [ true ⇒ λHhd. ?
     553  | false ⇒ λHhd. ?
     554  ] (refl ? (hd==elt)))
     555@(match (hd∈s2) return λx. (hd∈s2) = x → ?
     556  with
     557  [ true ⇒ λHmem. ?
     558  | false ⇒ λHmem. ?
     559  ] (refl ? (hd∈s2)))
     560>notb_true >notb_false normalize nodelta try //
     561try @Hind
     562[ 1:  whd in match (lset_remove ???) in ⊢ (???%); >Hhd
     563     elim (eqb_true ? elt elt) #_ #H >(H (refl ??))
     564     normalize in match (notb ?); normalize nodelta @Hind
     565| 2: >lset_difference_unfold >Hmem @Hind
     566| 3: whd in match (lset_remove ???) in ⊢ (???%);
     567     >lset_difference_unfold >Hhd >Hmem
     568     normalize in match (notb ?);
     569     normalize nodelta >Hind @refl
     570] qed.
     571
     572(* Inversion lemma on emptyness *)
     573lemma lset_eq_empty_inv : ∀A. ∀l. lset_eq A l [ ] → l = [ ].
     574#A #l elim l //
     575#hd' #tl' normalize #Hind * * @False_ind
     576qed.
     577
     578(* Inversion lemma on singletons *)
     579lemma lset_eq_singleton_inv : ∀A,hd,l. lset_eq A [hd] (hd::l) → All ? (λx.x=hd) l.
     580#A #hd #l
     581* #Hincl1 whd in ⊢ (% → ?); * #_ @All_mp
     582normalize #a * [ 1: #H @H | 2: @False_ind ]
     583qed.
     584
     585(* Permutation of two elements on top of the list is ok. *)
     586lemma lset_eq_permute : ∀A,l,x1,x2. lset_eq A (x1 :: x2 :: l) (x2 :: x1 :: l).
     587#A #l #x1 #x2 @conj normalize
     588[ 1: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
     589| 2: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/
     590] qed.
     591
     592(* "contraction" of an element. *)
     593lemma lset_eq_contract : ∀A,l,x. lset_eq A (x :: x :: l) (x :: l).
     594#A #l #x @conj
     595[ 1: /5 by or_introl, conj, transitive_lset_inclusion/
     596| 2: /5 by cons_preserves_inclusion, cons_monotonic_inclusion/ ]
     597qed.
     598
     599(* We don't need more than one instance of each element. *)
     600lemma lset_eq_filter : ∀A:DeqSet.∀tl.∀hd.
     601  lset_eq A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
     602#A #tl elim tl
     603[ 1: #hd normalize /4 by or_introl, conj, I/
     604| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
     605     lapply (eqb_true A hd' hd) cases (hd'==hd)
     606     [ 2: #_ normalize in match (notb ?); normalize nodelta
     607          lapply (cons_monotonic_eq … (Hind hd) hd') #H
     608          lapply (lset_eq_permute ? tl' hd' hd) #H'
     609          @(transitive_lset_eq ? ? (hd'::hd::tl') ? … H')
     610          @(transitive_lset_eq ? ?? (hd'::hd::tl') … H)
     611          @lset_eq_permute
     612     | 1: * #Heq #_ >(Heq (refl ??)) normalize in match (notb ?); normalize nodelta
     613          lapply (Hind hd) #H
     614          @(transitive_lset_eq ? ? (hd::tl') (hd::hd::tl') H)
     615          @conj
     616          [ 1: whd @conj /2 by or_introl/ @cons_preserves_inclusion @cons_preserves_inclusion
     617               @reflexive_lset_inclusion
     618          | 2: whd @conj /2 by or_introl/ ]
     619     ]
     620] qed.
     621
     622lemma lset_inclusion_filter_self :
     623  ∀A:DeqSet.∀l,pred.
     624    lset_inclusion A (filter ? pred l) l.
     625#A #l #pred elim l
     626[ 1: normalize @I
     627| 2: #hd #tl #Hind whd in match (filter ???);
     628     cases (pred hd) normalize nodelta
     629     [ 1: @cons_monotonic_inclusion @Hind
     630     | 2: @cons_preserves_inclusion @Hind ]
     631] qed.   
     632
     633lemma lset_inclusion_filter_monotonic :
     634  ∀A:DeqSet.∀l1,l2. lset_inclusion (carr A) l1 l2 →
     635  ∀elt. lset_inclusion A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
     636#A #l1 elim l1
     637[ 1: #l2 normalize //
     638| 2: #hd1 #tl1 #Hind #l2 whd in ⊢ (% → ?); * #Hmem1 #Htl1_incl #elt
     639     whd >filter_cons_unfold
     640     lapply (eqb_true A hd1 elt) cases (hd1==elt)
     641     [ 1: * #H1 #_ lapply (H1 (refl ??)) #H1_eq >H1_eq in Hmem1; #Hmem
     642          normalize in match (notb ?); normalize nodelta @Hind assumption
     643     | 2: * #_ #Hneq normalize in match (notb ?); normalize nodelta
     644          whd @conj
     645          [ 1: elim l2 in Hmem1; try //
     646               #hd2 #tl2 #Hincl whd in ⊢ (% → ?); *
     647               [ 1: #Heq >Heq in Hneq; normalize
     648                    lapply (eqb_true A hd2 elt) cases (hd2==elt)
     649                    [ 1: * #H #_ #H2 lapply (H2 (H (refl ??))) #Habsurd destruct (Habsurd)
     650                    | 2: #_ normalize nodelta #_ /2 by or_introl/ ]
     651               | 2: #H lapply (Hincl H) #Hok
     652                    normalize cases (hd2==elt) normalize nodelta
     653                    [ 1: @Hok
     654                    | 2: %2 @Hok ] ]
     655          | 2: @Hind assumption ] ] ]
     656qed.
     657
     658(* removing an element of two equivalent sets conserves equivalence. *)
     659lemma lset_eq_filter_monotonic :
     660  ∀A:DeqSet.∀l1,l2. lset_eq (carr A) l1 l2 →
     661  ∀elt. lset_eq A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2).
     662#A #l1 #l2 * #Hincl1 #Hincl2 #elt @conj
     663/2 by lset_inclusion_filter_monotonic/
     664qed.
     665
     666(* ---------------- Concrete implementation of sets --------------------- *)
     667
     668(* We can give an explicit characterization of equivalent sets: they are permutations with repetitions, i,e.
     669   a composition of transpositions and duplications. We restrict ourselves to DeqSets. *)
     670inductive iso_step_lset (A : DeqSet) : lset A → lset A → Prop ≝
     671| lset_transpose : ∀a,x,b,y,c. iso_step_lset A (a @ [x] @ b @ [y] @ c) (a @ [y] @ b @ [x] @ c)
     672| lset_weaken : ∀a,x,b. iso_step_lset A (a @ [x] @ b) (a @ [x] @ [x] @ b)
     673| lset_contract : ∀a,x,b. iso_step_lset A (a @ [x] @ [x] @ b) (a @ [x] @ b).
     674
     675(* The equivalence is the reflexive, transitive and symmetric closure of iso_step_lset *)
     676inductive lset_eq_concrete (A : DeqSet) : lset A → lset A → Prop ≝
     677| lset_trans : ∀a,b,c. iso_step_lset A a b → lset_eq_concrete A b c → lset_eq_concrete A a c
     678| lset_refl  : ∀a. lset_eq_concrete A a a.
     679
     680(* lset_eq_concrete is symmetric and transitive *)
     681lemma 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.
     682#A #l1 #l2 #l3 #Hequiv
     683elim Hequiv //
     684#a #b #c #Hstep #Hequiv #Hind #Hcl3 lapply (Hind Hcl3) #Hbl3
     685@(lset_trans ???? Hstep Hbl3)
     686qed.
     687
     688lemma symmetric_step : ∀A,l1,l2. iso_step_lset A l1 l2 → iso_step_lset A l2 l1.
     689#A #l1 #l2 * /2/ qed.
     690
     691lemma symmetric_lset_eq_concrete : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l1.
     692#A #l1 #l2 #H elim H //
     693#a #b #c #Hab #Hbc #Hcb
     694@(transitive_lset_eq_concrete ???? Hcb ?)
     695@(lset_trans … (symmetric_step ??? Hab) (lset_refl …))
     696qed.
     697 
     698(* lset_eq_concrete is conserved by cons. *)
     699lemma equivalent_step_cons : ∀A,l1,l2. iso_step_lset A l1 l2 → ∀x. iso_step_lset A (x :: l1) (x :: l2).
     700#A #l1 #l2 * // qed. (* That // was impressive. *)
     701
     702lemma lset_eq_concrete_cons : ∀A,l1,l2. lset_eq_concrete A l1 l2 → ∀x. lset_eq_concrete A (x :: l1) (x :: l2).
     703#A #l1 #l2 #Hequiv elim Hequiv try //
     704#a #b #c #Hab #Hbc #Hind #x %1{(equivalent_step_cons ??? Hab x) (Hind x)}
     705qed.
     706
     707lemma absurd_list_eq_append : ∀A.∀x.∀l1,l2:list A. [ ] = l1 @ [x] @ l2 → False.
     708#A #x #l1 #l2 elim l1 normalize
     709[ 1: #Habsurd destruct
     710| 2: #hd #tl #_ #Habsurd destruct
     711] qed.
     712
     713(* Inversion lemma for emptyness, step case *)
     714lemma equivalent_iso_step_empty_inv : ∀A,l. iso_step_lset A l [] → l = [ ].
     715#A #l elim l //
     716#hd #tl #Hind #H inversion H
     717[ 1: #a #x #b #y #c #_ #Habsurd
     718      @(False_ind … (absurd_list_eq_append ? y … Habsurd))
     719| 2: #a #x #b #_ #Habsurd
     720      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
     721| 3: #a #x #b #_ #Habsurd
     722      @(False_ind … (absurd_list_eq_append ? x … Habsurd))
     723] qed.
     724
     725(* Same thing for non-emptyness *)
     726lemma equivalent_iso_step_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → iso_step_lset A l1 l2 → l2 ≠ [ ].
     727#A #l1 elim l1
     728[ 1: #l2 * #H @(False_ind … (H (refl ??)))
     729| 2: #hd #tl #H #l2 #_ #Hstep % #Hl2 >Hl2 in Hstep; #Hstep
     730     lapply (equivalent_iso_step_empty_inv … Hstep) #Habsurd destruct
     731] qed.
     732
     733lemma lset_eq_concrete_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → lset_eq_concrete A l1 l2 → l2 ≠ [ ].
     734#A #l1 #l2 #Hl1 #H lapply Hl1 elim H
     735[ 2: #a #H @H
     736| 1: #a #b #c #Hab #Hbc #H #Ha lapply (equivalent_iso_step_cons_inv … Ha Hab) #Hb @H @Hb
     737] qed.
     738
     739lemma lset_eq_concrete_empty_inv : ∀A,l1,l2. l1 = [ ] → lset_eq_concrete A l1 l2 → l2 = [ ].
     740#A #l1 #l2 #Hl1 #H lapply Hl1 elim H //
     741#a #b #c #Hab #Hbc #Hbc_eq #Ha >Ha in Hab; #H_b lapply (equivalent_iso_step_empty_inv … ?? (symmetric_step … H_b))
     742#Hb @Hbc_eq @Hb
     743qed.
     744
     745(* Square equivalence diagram *)
     746lemma square_lset_eq_concrete :
     747  ∀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'.
     748#A #a #b #a' #b' #H1 #H2 #H3
     749@(transitive_lset_eq_concrete ???? (symmetric_lset_eq_concrete … H2))
     750@(transitive_lset_eq_concrete ???? H1)
     751@H3
     752qed.
     753
     754(* Make the transposition of elements visible at top-level *)
     755lemma transpose_lset_eq_concrete :
     756  ∀A. ∀x,y,a,b,c,a',b',c'.
     757  lset_eq_concrete A (a @ [x] @ b @ [y] @ c) (a' @ [x] @ b' @ [y] @ c') →
     758  lset_eq_concrete A (a @ [y] @ b @ [x] @ c) (a' @ [y] @ b' @ [x] @ c').
     759#A #x #y #a #b #c #a' #b' #c
     760#H @(square_lset_eq_concrete ????? H) /2 by lset_trans, lset_refl, lset_transpose/
     761qed.
     762
     763lemma switch_lset_eq_concrete :
     764  ∀A. ∀a,b,c. lset_eq_concrete A (a@[b]@c) ([b]@a@c).
     765#A #a elim a //
     766#hda #tla #Hind #b #c lapply (Hind hda c) #H
     767lapply (lset_eq_concrete_cons … H b)
     768#H' normalize in H' ⊢ %; @symmetric_lset_eq_concrete
     769/3 by lset_transpose, lset_trans, symmetric_lset_eq_concrete/
     770qed.
     771
     772(* Folding a commutative and idempotent function on equivalent sets yields the same result. *)
     773lemma lset_eq_concrete_fold :
     774  ∀A : DeqSet.
     775  ∀acctype : Type[0].
     776  ∀l1,l2 : list (carr A).
     777  lset_eq_concrete A l1 l2 →
     778  ∀f:carr A → acctype → acctype.
     779  (∀x1,x2. ∀acc. f x1 (f x2 acc) = f x2 (f x1 acc)) →
     780  (∀x.∀acc. f x (f x acc) = f x acc) →
     781  ∀acc. foldr ?? f acc l1 = foldr ?? f acc l2.
     782#A #acctype #l1 #l2 #Heq #f #Hcomm #Hidem
     783elim Heq
     784try //
     785#a' #b' #c' #Hstep #Hbc #H #acc <H -H
     786elim Hstep
     787[ 1: #a #x #b #y #c
     788     >fold_append >fold_append >fold_append >fold_append
     789     >fold_append >fold_append >fold_append >fold_append
     790     normalize
     791     cut (f x (foldr A acctype f (f y (foldr A acctype f acc c)) b) =
     792          f y (foldr A acctype f (f x (foldr A acctype f acc c)) b)) [   
     793     elim c
     794     [ 1: normalize elim b
     795          [ 1: normalize >(Hcomm x y) @refl
     796          | 2: #hdb #tlb #Hind normalize
     797               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ]
     798     | 2: #hdc #tlc #Hind normalize elim b
     799          [ 1: normalize >(Hcomm x y) @refl
     800          | 2: #hdb #tlb #Hind normalize
     801               >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] ]
     802     ]
     803     #Hind >Hind @refl
     804| 2: #a #x #b
     805     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
     806     normalize >Hidem @refl
     807| 3: #a #x #b
     808     >fold_append  >(fold_append ?? ([x]@[x])) >fold_append >fold_append
     809     normalize >Hidem @refl
     810] qed.
     811
     812(* Folding over equivalent sets yields equivalent results, for any equivalence. *)
     813lemma inj_to_fold_inj :
     814  ∀A,acctype : Type[0].
     815  ∀eqrel : acctype → acctype → Prop.
     816  ∀refl_eqrel  : reflexive ? eqrel.
     817  ∀trans_eqrel : transitive ? eqrel.
     818  ∀sym_eqrel   : symmetric ? eqrel.
     819  ∀f           : A → acctype → acctype.
     820  (∀x:A.∀acc1:acctype.∀acc2:acctype.eqrel acc1 acc2→eqrel (f x acc1) (f x acc2)) →
     821  ∀l : list A. ∀acc1, acc2 : acctype. eqrel acc1 acc2 → eqrel (foldr … f acc1 l) (foldr … f acc2 l).
     822#A #acctype #eqrel #R #T #S #f #Hinj #l elim l
     823//
     824#hd #tl #Hind #acc1 #acc2 #Heq normalize @Hinj @Hind @Heq
     825qed.
     826
     827(* We need to extend the above proof to arbitrary equivalence relation instead of
     828   just standard equality. *)
     829lemma lset_eq_concrete_fold_ext :
     830  ∀A : DeqSet.
     831  ∀acctype : Type[0].
     832  ∀eqrel : acctype → acctype → Prop.
     833  ∀refl_eqrel  : reflexive ? eqrel.
     834  ∀trans_eqrel : transitive ? eqrel.
     835  ∀sym_eqrel   : symmetric ? eqrel.
     836  ∀f:carr A → acctype → acctype.
     837  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
     838  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
     839  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
     840  ∀l1,l2 : list (carr A).
     841  lset_eq_concrete A l1 l2 → 
     842  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
     843#A #acctype #eqrel #R #T #S #f #Hinj #Hcomm #Hidem #l1 #l2 #Heq
     844elim Heq
     845try //
     846#a' #b' #c' #Hstep #Hbc #H inversion Hstep
     847[ 1: #a #x #b #y #c #HlA #HlB #_ #acc
     848     >HlB in H; #H @(T … ? (H acc))
     849     >fold_append >fold_append >fold_append >fold_append
     850     >fold_append >fold_append >fold_append >fold_append
     851     normalize
     852     cut (eqrel (f x (foldr ? acctype f (f y (foldr ? acctype f acc c)) b))
     853                (f y (foldr ? acctype f (f x (foldr ? acctype f acc c)) b)))
     854     [ 1:
     855     elim c
     856     [ 1: normalize elim b
     857          [ 1: normalize @(Hcomm x y)
     858          | 2: #hdb #tlb #Hind normalize
     859               lapply (Hinj hdb ?? Hind) #Hind'
     860               lapply (T … Hind' (Hcomm ???)) #Hind''
     861               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
     862     | 2: #hdc #tlc #Hind normalize elim b
     863          [ 1: normalize @(Hcomm x y)
     864          | 2: #hdb #tlb #Hind normalize
     865               lapply (Hinj hdb ?? Hind) #Hind'
     866               lapply (T … Hind' (Hcomm ???)) #Hind''
     867               @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ]
     868     ] ]
     869     #Hind @(inj_to_fold_inj … eqrel R T S ? Hinj … Hind)
     870| 2: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
     871     >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x]))
     872     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @S @Hidem
     873| 3: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc))
     874     >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append
     875     normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @Hidem
     876] qed.
     877
     878(* Prepare some well-founded induction principles on lists. The idea is to perform
     879   an induction on the sequence of filterees of a list : taking the first element,
     880   filtering it out of the tail, etc. We give such principles for pairs of lists
     881   and isolated lists.  *)
     882
     883(* The two lists [l1,l2] share at least the head of l1. *)
     884definition head_shared ≝ λA. λl1,l2 : list A.
     885match l1 with
     886[ nil ⇒ l2 = (nil ?)
     887| cons hd _ ⇒  mem … hd l2
     888].
     889
     890(* Relation on pairs of lists, as described above. *)
     891definition filtered_lists : ∀A:DeqSet. relation (list (carr A)×(list (carr A))) ≝
     892λA:DeqSet. λll1,ll2.
     893let 〈la1,lb1〉 ≝ ll1 in
     894let 〈la2,lb2〉 ≝ ll2 in
     895match la2 with
     896[ nil ⇒ False
     897| cons hda2 tla2 ⇒
     898    head_shared ? la2 lb2 ∧
     899    la1 = filter … (λx.¬(x==hda2)) tla2 ∧
     900    lb1 = filter … (λx.¬(x==hda2)) lb2
     901].
     902
     903(* Notice the absence of plural : this relation works on a simple list, not a pair. *)
     904definition filtered_list : ∀A:DeqSet. relation (list (carr A)) ≝
     905λA:DeqSet. λl1,l2.
     906match l2 with
     907[ nil ⇒ False
     908| cons hd2 tl2 ⇒
     909    l1 = filter … (λx.¬(x==hd2)) l2
     910].
     911
     912(* Relation on lists based on their lengths. We know this one is well-founded. *)
     913definition length_lt : ∀A:DeqSet. relation (list (carr A)) ≝
     914λA:DeqSet. λl1,l2. lt (length ? l1) (length ? l2).
     915
     916(* length_lt can be extended on pairs by just measuring the first component *)
     917definition length_fst_lt : ∀A:DeqSet. relation (list (carr A) × (list (carr A))) ≝
     918λA:DeqSet. λll1,ll2. lt (length ? (\fst ll1)) (length ? (\fst ll2)).
     919
     920lemma filter_length : ∀A. ∀l. ∀f. |filter A f l| ≤ |l|.
     921#A #l #f elim l //
     922#hd #tl #Hind whd in match (filter ???); cases (f hd) normalize nodelta
     923[ 1: /2 by le_S_S/
     924| 2: @le_S @Hind
     925] qed.
     926
     927(* The order on lists defined by their length is wf *)
     928lemma length_lt_wf : ∀A. ∀l. WF (list (carr A)) (length_lt A) l.
     929#A #l % elim l
     930[ 1: #a normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
     931| 2: #hd #tl #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
     932@(transitive_le … Hlt') @(monotonic_pred … Hlt)
     933qed.
     934
     935(* Order on pairs of list by measuring the first proj *)
     936lemma length_fst_lt_wf : ∀A. ∀ll. WF ? (length_fst_lt A) ll.
     937#A * #l1 #l2 % elim l1
     938[ 1: * #a1 #a2 normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind
     939| 2: #hd1 #tl1 #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd
     940@(transitive_le … Hlt') @(monotonic_pred … Hlt)
     941qed.
     942
     943lemma length_to_filtered_lists : ∀A. subR ? (filtered_lists A) (length_fst_lt A).
     944#A whd * #a1 #a2 * #b1 #b2 elim b1
     945[ 1: @False_ind
     946| 2: #hd1 #tl1 #Hind whd in ⊢ (% → ?); * * #Hmem #Ha1 #Ha2 whd
     947     >Ha1 whd in match (length ??) in ⊢ (??%); @le_S_S @filter_length
     948] qed.
     949
     950lemma length_to_filtered_list : ∀A. subR ? (filtered_list A) (length_lt A).
     951#A whd #a #b elim b
     952[ 1: @False_ind
     953| 2: #hd #tl #Hind whd in ⊢ (% → ?); whd in match (filter ???);
     954     lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?);
     955     normalize nodelta #Ha whd @le_S_S >Ha @filter_length ]
     956qed.
     957
     958(* Prove well-foundedness by embedding in lt *)
     959lemma filtered_lists_wf : ∀A. ∀ll. WF ? (filtered_lists A) ll.
     960#A #ll @(WF_antimonotonic … (length_to_filtered_lists A)) @length_fst_lt_wf
     961qed.
     962
     963lemma filtered_list_wf : ∀A. ∀l. WF ? (filtered_list A) l.
     964#A #l @(WF_antimonotonic … (length_to_filtered_list A)) @length_lt_wf
     965qed.
     966
     967definition Acc_elim : ∀A,R,x. WF A R x → (∀a. R a x → WF A R a) ≝
     968λA,R,x,acc.
     969match acc with
     970[ wf _ a0 ⇒ a0 ].
     971
     972(* Stolen from Coq. Warped to avoid prop-to-type restriction. *)
     973let rec WF_rect
     974  (A : Type[0])
     975  (R : A → A → Prop)
     976  (P : A → Type[0])
     977  (f : ∀ x : A.
     978       (∀ y : A. R y x → WF ? R y) →
     979       (∀ y : A. R y x → P y) → P x)
     980  (x : A)
     981  (a : WF A R x) on a : P x ≝
     982f x (Acc_elim … a) (λy:A. λRel:R y x. WF_rect A R P f y ((Acc_elim … a) y Rel)).
     983
     984lemma lset_eq_concrete_filter : ∀A:DeqSet.∀tl.∀hd.
     985  lset_eq_concrete A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl).
     986#A #tl elim tl
     987[ 1: #hd //
     988| 2: #hd' #tl' #Hind #hd >filter_cons_unfold
     989     lapply (eqb_true A hd' hd)
     990     cases (hd'==hd)
     991     [ 2: #_ normalize in match (notb false); normalize nodelta
     992          >cons_to_append >(cons_to_append … hd')
     993          >cons_to_append in ⊢ (???%); >(cons_to_append … hd') in ⊢ (???%);
     994          @(transpose_lset_eq_concrete ? hd' hd [ ] [ ] (filter A (λy:A.¬y==hd) tl') [ ] [ ] tl')
     995          >nil_append >nil_append >nil_append >nil_append
     996          @lset_eq_concrete_cons >nil_append >nil_append
     997          @Hind
     998    | 1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta
     999         >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));
     1000         @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))
     1001         [ 1: @Hind
     1002         | 2: %2
     1003         | 3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]
     1004    ]
     1005] qed.
     1006
     1007
     1008(* The "abstract", observational definition of set equivalence implies the concrete one. *)
     1009
     1010lemma lset_eq_to_lset_eq_concrete_aux :
     1011  ∀A,ll.
     1012    head_shared … (\fst ll) (\snd ll) →
     1013    lset_eq (carr A) (\fst ll) (\snd ll) →
     1014    lset_eq_concrete A (\fst ll) (\snd ll).
     1015#A #ll @(WF_ind ????? (filtered_lists_wf A ll))
     1016* *
     1017[ 1: #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hb2 >Hb2 #_ %2
     1018| 2: #hd1 #tl1 #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hmem
     1019     lapply (list_mem_split ??? Hmem) * #l2A * #l2B #Hb2 #Heq
     1020     destruct
     1021     lapply (Hind_wf 〈filter … (λx.¬x==hd1) tl1,filter … (λx.¬x==hd1) (l2A@l2B)〉)
     1022     cut (filtered_lists A 〈filter A (λx:A.¬x==hd1) tl1,filter A (λx:A.¬x==hd1) (l2A@l2B)〉 〈hd1::tl1,l2A@[hd1]@l2B〉)
     1023     [ @conj try @conj try @refl whd
     1024       [ 1: /2 by /
     1025       | 2: >filter_append in ⊢ (???%); >filter_append in ⊢ (???%);
     1026            whd in match (filter ?? [hd1]);
     1027            elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
     1028            normalize nodelta <filter_append @refl ] ]
     1029     #Hfiltered #Hind_aux lapply (Hind_aux Hfiltered) -Hind_aux
     1030     cut (lset_eq A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
     1031     [ 1: lapply (lset_eq_filter_monotonic … Heq hd1)
     1032          >filter_cons_unfold >filter_append >(filter_append … [hd1])
     1033          whd in match (filter ?? [hd1]);
     1034          elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?);
     1035          normalize nodelta <filter_append #Hsol @Hsol ]
     1036     #Hset_eq
     1037     cut (head_shared A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B)))
     1038     [ 1: lapply Hset_eq cases (filter A (λx:A.¬x==hd1) tl1)
     1039          [ 1: whd in ⊢ (% → ?); * #_ elim (filter A (λx:A.¬x==hd1) (l2A@l2B)) //
     1040               #hd' #tl' normalize #Hind * @False_ind
     1041          | 2: #hd' #tl' * #Hincl1 #Hincl2 whd elim Hincl1 #Hsol #_ @Hsol ] ]
     1042     #Hshared #Hind_aux lapply (Hind_aux Hshared Hset_eq)
     1043     #Hconcrete_set_eq
     1044     >cons_to_append
     1045     @(transitive_lset_eq_concrete ? ([hd1]@tl1) ([hd1]@l2A@l2B) (l2A@[hd1]@l2B))
     1046     [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete ]
     1047     lapply (lset_eq_concrete_cons … Hconcrete_set_eq hd1) #Hconcrete_cons_eq
     1048     @(square_lset_eq_concrete … Hconcrete_cons_eq)
     1049     [ 1: @(lset_eq_concrete_filter ? tl1 hd1)
     1050     | 2: @(lset_eq_concrete_filter ? (l2A@l2B) hd1) ]
     1051] qed.
     1052
     1053lemma lset_eq_to_lset_eq_concrete : ∀A,l1,l2. lset_eq (carr A) l1 l2 → lset_eq_concrete A l1 l2.
     1054#A *
     1055[ 1: #l2 #Heq >(lset_eq_empty_inv … (symmetric_lset_eq … Heq)) //
     1056| 2: #hd1 #tl1 #l2 #Hincl lapply Hincl lapply (lset_eq_to_lset_eq_concrete_aux ? 〈hd1::tl1,l2〉) #H @H
     1057     whd elim Hincl * //
     1058] qed.
     1059
     1060
     1061(* The concrete one implies the abstract one. *)
     1062lemma lset_eq_concrete_to_lset_eq : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq A l1 l2.
     1063#A #l1 #l2 #Hconcrete
     1064elim Hconcrete try //
     1065#a #b #c #Hstep #Heq_bc_concrete #Heq_bc
     1066cut (lset_eq A a b)
     1067[ 1: elim Hstep
     1068     [ 1: #a' elim a'
     1069          [ 2: #hda #tla #Hind #x #b' #y #c' >cons_to_append
     1070               >(associative_append ? [hda] tla ?)
     1071               >(associative_append ? [hda] tla ?)
     1072               @cons_monotonic_eq >nil_append >nil_append @Hind
     1073          | 1: #x #b' #y #c' >nil_append >nil_append
     1074               elim b' try //
     1075               #hdb #tlc #Hind >append_cons >append_cons in ⊢ (???%);
     1076               >associative_append >associative_append
     1077               lapply (cons_monotonic_eq … Hind hdb) #Hind'               
     1078               @(transitive_lset_eq ? ([x]@[hdb]@tlc@[y]@c') ([hdb]@[x]@tlc@[y]@c'))
     1079               /2 by transitive_lset_eq/ ]
     1080     | 2: #a' elim a'
     1081          [ 2: #hda #tla #Hind #x #b' >cons_to_append
     1082               >(associative_append ? [hda] tla ?)
     1083               >(associative_append ? [hda] tla ?)
     1084               @cons_monotonic_eq >nil_append >nil_append @Hind
     1085          | 1: #x #b' >nil_append >nil_append @conj normalize
     1086               [ 1: @conj [ 1: %1 @refl ] elim b'
     1087                    [ 1: @I
     1088                    | 2: #hdb #tlb #Hind normalize @conj
     1089                         [ 1: %2 %2 %1 @refl
     1090                         | 2: @(All_mp … Hind) #a0 *
     1091                              [ 1: #Heq %1 @Heq
     1092                              | 2: * /2 by or_introl, or_intror/ ] ] ]
     1093                    #H %2 %2 %2 @H
     1094               | 2: @conj try @conj try /2 by or_introl, or_intror/ elim b'
     1095                    [ 1: @I
     1096                    | 2: #hdb #tlb #Hind normalize @conj
     1097                         [ 1: %2 %1 @refl
     1098                         | 2: @(All_mp … Hind) #a0 *
     1099                              [ 1: #Heq %1 @Heq
     1100                              | 2: #H %2 %2 @H ] ] ] ] ]
     1101     | 3: #a #x #b elim a try @lset_eq_contract
     1102          #hda #tla #Hind @cons_monotonic_eq @Hind ] ]
     1103#Heq_ab @(transitive_lset_eq … Heq_ab Heq_bc)
     1104qed.
     1105
     1106lemma lset_eq_fold :
     1107  ∀A : DeqSet.
     1108  ∀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:carr A → acctype → acctype.
     1114  (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) →
     1115  (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) →
     1116  (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) →
     1117  ∀l1,l2 : list (carr A).
     1118  lset_eq A l1 l2 → 
     1119  ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2).
     1120#A #acctype #eqrel #refl_eqrel #trans_eqrel #sym_eqrel #f #Hinj #Hsym #Hcontract #l1 #l2 #Heq #acc
     1121lapply (lset_eq_to_lset_eq_concrete … Heq) #Heq_concrete
     1122@(lset_eq_concrete_fold_ext A acctype eqrel refl_eqrel trans_eqrel sym_eqrel f Hinj Hsym Hcontract l1 l2 Heq_concrete acc)
     1123qed.
     1124
     1125
     1126
Note: See TracChangeset for help on using the changeset viewer.