| 1 | include "basics/lists/listb.ma". |
|---|
| 2 | |
|---|
| 3 | definition bool_to_Prop : bool → Prop ≝ |
|---|
| 4 | λb. match b with [ true ⇒ True | false ⇒ False ]. |
|---|
| 5 | |
|---|
| 6 | coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. |
|---|
| 7 | |
|---|
| 8 | lemma dep_bool_match_elim : |
|---|
| 9 | ∀b.∀B : Type[0].∀P : B → Prop.∀Q : bool → Prop. |
|---|
| 10 | ∀c1,c2. |
|---|
| 11 | (∀prf : Q true.P (c1 prf)) → |
|---|
| 12 | (∀prf : Q false.P (c2 prf)) → |
|---|
| 13 | ∀prf : Q b. |
|---|
| 14 | P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf). |
|---|
| 15 | * // qed. |
|---|
| 16 | |
|---|
| 17 | definition defined : ∀T:Type[0]. option T → bool ≝ |
|---|
| 18 | λT,x. match x with [ None ⇒ false | Some _ ⇒ true ]. |
|---|
| 19 | |
|---|
| 20 | let rec for_each (T:Type[0]) (f: T → bool) (l: list T) on l : bool ≝ |
|---|
| 21 | match l with |
|---|
| 22 | [ nil ⇒ true |
|---|
| 23 | | cons hd tl ⇒ for_each T f tl ∧ f hd ]. |
|---|
| 24 | |
|---|
| 25 | lemma for_each_to_memb_to_true: |
|---|
| 26 | ∀T:DeqSet. ∀f: T → bool. ∀t:T. ∀l: list T. |
|---|
| 27 | memb T t l → for_each T f l = true → f t = true. |
|---|
| 28 | #T #f #t #l elim l |
|---|
| 29 | [ #abs cases abs |
|---|
| 30 | | #hd #tl #IH normalize in ⊢ (% → ?); inversion (t == hd) #H normalize |
|---|
| 31 | [ #_ cases (for_each ???) normalize |
|---|
| 32 | [ <(\P H) // | #abs destruct ] |
|---|
| 33 | | cases (t ∈ tl) in IH; normalize |
|---|
| 34 | [2: #_ #abs cases abs |
|---|
| 35 | | cases (for_each ???) normalize /2/]] |
|---|
| 36 | qed. |
|---|
| 37 | |
|---|
| 38 | let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝ |
|---|
| 39 | match l1 with |
|---|
| 40 | [ nil ⇒ true |
|---|
| 41 | | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ]. |
|---|
| 42 | |
|---|
| 43 | |
|---|
| 44 | lemma sublist_hd_tl_to_memb: |
|---|
| 45 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. |
|---|
| 46 | sublist S (hd::tl) l2 → memb S hd l2. |
|---|
| 47 | #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // |
|---|
| 48 | qed. |
|---|
| 49 | |
|---|
| 50 | lemma sublist_hd_tl_to_sublist: |
|---|
| 51 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. |
|---|
| 52 | sublist S (hd::tl) l2 → sublist S tl l2. |
|---|
| 53 | #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H |
|---|
| 54 | qed. |
|---|
| 55 | |
|---|
| 56 | lemma memb_to_sublist_to_memb: |
|---|
| 57 | ∀T:DeqSet. ∀x:T. ∀l1,l2: list T. |
|---|
| 58 | memb … x l1 → sublist … l1 l2 → memb … x l2. |
|---|
| 59 | #T #x #l1 elim l1 |
|---|
| 60 | [ #l2 #abs cases abs |
|---|
| 61 | | #hd #tl #IH #l2 whd in match (memb ???); inversion (x==hd) /3/ |
|---|
| 62 | #H #_ whd in match (sublist ???); <(\P H) cases (memb ???) // ] |
|---|
| 63 | qed. |
|---|
| 64 | |
|---|
| 65 | lemma sublist_insert_snd_pos: |
|---|
| 66 | ∀S:DeqSet. ∀x,y:S. ∀l1,l2:list S. |
|---|
| 67 | sublist S l1 (x::l2) → sublist S l1 (x::y::l2). |
|---|
| 68 | #S #x #y #l1 elim l1 [//] |
|---|
| 69 | #hd #tl #IH #l2 #H |
|---|
| 70 | lapply (sublist_hd_tl_to_sublist … H) #K |
|---|
| 71 | whd in match (sublist ???); >(?:hd∈x::y::l2 = true) /2/ |
|---|
| 72 | lapply (sublist_hd_tl_to_memb … H) normalize cases (hd==x) normalize // |
|---|
| 73 | cases (hd==y) normalize // cases (hd∈l2) // #H cases H |
|---|
| 74 | qed. |
|---|
| 75 | |
|---|
| 76 | lemma sublist_tl_hd_tl: |
|---|
| 77 | ∀S:DeqSet. ∀hd:S. ∀tl:list S. sublist S tl (hd::tl). |
|---|
| 78 | #S #hd #tl elim tl try % |
|---|
| 79 | #hd' #tl' #IH whd in match (sublist ???); |
|---|
| 80 | whd in match (hd' ∈ hd::?::?); cases (hd'==hd) |
|---|
| 81 | whd in match (hd' ∈ ?::?); >(\b ?) try % normalize |
|---|
| 82 | lapply (sublist_insert_snd_pos … hd' … IH) |
|---|
| 83 | cases (sublist ???) // |
|---|
| 84 | qed. |
|---|
| 85 | |
|---|
| 86 | lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l. |
|---|
| 87 | #S #l elim l [//] #hd #tl #IH normalize >(\b ?) // |
|---|
| 88 | qed. |
|---|
