include "basics/lists/listb.ma". definition bool_to_Prop : bool → Prop ≝ λb. match b with [ true ⇒ True | false ⇒ False ]. coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. lemma dep_bool_match_elim : ∀b.∀B : Type[0].∀P : B → Prop.∀Q : bool → Prop. ∀c1,c2. (∀prf : Q true.P (c1 prf)) → (∀prf : Q false.P (c2 prf)) → ∀prf : Q b. P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf). * // qed. definition defined : ∀T:Type[0]. option T → bool ≝ λT,x. match x with [ None ⇒ false | Some _ ⇒ true ]. let rec for_each (T:Type[0]) (f: T → bool) (l: list T) on l : bool ≝ match l with [ nil ⇒ true | cons hd tl ⇒ for_each T f tl ∧ f hd ]. lemma for_each_to_memb_to_true: ∀T:DeqSet. ∀f: T → bool. ∀t:T. ∀l: list T. memb T t l → for_each T f l = true → f t = true. #T #f #t #l elim l [ #abs cases abs | #hd #tl #IH normalize in ⊢ (% → ?); inversion (t == hd) #H normalize [ #_ cases (for_each ???) normalize [ <(\P H) // | #abs destruct ] | cases (t ∈ tl) in IH; normalize [2: #_ #abs cases abs | cases (for_each ???) normalize /2/]] qed. let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝ match l1 with [ nil ⇒ true | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ]. lemma sublist_hd_tl_to_memb: ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. sublist S (hd::tl) l2 → memb S hd l2. #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // qed. lemma sublist_hd_tl_to_sublist: ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. sublist S (hd::tl) l2 → sublist S tl l2. #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H qed. lemma memb_to_sublist_to_memb: ∀T:DeqSet. ∀x:T. ∀l1,l2: list T. memb … x l1 → sublist … l1 l2 → memb … x l2. #T #x #l1 elim l1 [ #l2 #abs cases abs | #hd #tl #IH #l2 whd in match (memb ???); inversion (x==hd) /3/ #H #_ whd in match (sublist ???); <(\P H) cases (memb ???) // ] qed. lemma sublist_insert_snd_pos: ∀S:DeqSet. ∀x,y:S. ∀l1,l2:list S. sublist S l1 (x::l2) → sublist S l1 (x::y::l2). #S #x #y #l1 elim l1 [//] #hd #tl #IH #l2 #H lapply (sublist_hd_tl_to_sublist … H) #K whd in match (sublist ???); >(?:hd∈x::y::l2 = true) /2/ lapply (sublist_hd_tl_to_memb … H) normalize cases (hd==x) normalize // cases (hd==y) normalize // cases (hd∈l2) // #H cases H qed. lemma sublist_tl_hd_tl: ∀S:DeqSet. ∀hd:S. ∀tl:list S. sublist S tl (hd::tl). #S #hd #tl elim tl try % #hd' #tl' #IH whd in match (sublist ???); whd in match (hd' ∈ hd::?::?); cases (hd'==hd) whd in match (hd' ∈ ?::?); >(\b ?) try % normalize lapply (sublist_insert_snd_pos … hd' … IH) cases (sublist ???) // qed. lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l. #S #l elim l [//] #hd #tl #IH normalize >(\b ?) // qed.