source: Papers/polymorphic-variants-2012/infrastructure.ma @ 2549

Last change on this file since 2549 was 2522, checked in by sacerdot, 7 years ago

Generic stuff moved to infrastructure.

File size: 2.8 KB
Line 
1include "basics/lists/listb.ma".
2
3definition bool_to_Prop : bool → Prop ≝
4 λb. match b with [ true ⇒ True | false ⇒ False ].
5
6coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
7
8lemma 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.
14P (match b return λx.Q x → B with [ true ⇒ λprf.c1 prf | false ⇒ λprf.c2 prf ] prf).
15* // qed.
16
17definition defined : ∀T:Type[0]. option T → bool ≝
18 λT,x. match x with [ None ⇒ false | Some _ ⇒ true ].
19
20let 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
25lemma 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/]]
36qed.
37
38let 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
44lemma 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 //
48qed.
49
50lemma 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
54qed.
55
56lemma 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 ???) // ]
63qed.
64
65lemma 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
74qed.
75
76lemma 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 ???) //
84qed.
85
86lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l.
87 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) //
88qed.
Note: See TracBrowser for help on using the repository browser.