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.