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. |
---|