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

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

All .ma files committed: some of them are just in-progress.

File size: 2.6 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
8definition defined : ∀T:Type[0]. option T → bool ≝
9 λT,x. match x with [ None ⇒ false | Some _ ⇒ true ].
10
11let rec for_each (T:Type[0]) (f: T → bool) (l: list T) on l : bool ≝
12 match l with
13 [ nil ⇒ true
14 | cons hd tl ⇒ for_each T f tl ∧ f hd ].
15
16lemma for_each_to_memb_to_true:
17 ∀T:DeqSet. ∀f: T → bool. ∀t:T. ∀l: list T.
18  memb T t l → for_each T f l = true → f t = true.
19 #T #f #t #l elim l
20 [ #abs cases abs
21 | #hd #tl #IH normalize in ⊢ (% → ?); inversion (t == hd) #H normalize
22   [ #_ cases (for_each ???) normalize
23     [ <(\P H) // | #abs destruct ]
24   | cases (t ∈ tl) in IH; normalize
25     [2: #_ #abs cases abs
26     | cases (for_each ???) normalize /2/]]
27qed.
28
29let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝
30 match l1 with
31 [ nil ⇒ true
32 | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ].
33
34
35lemma sublist_hd_tl_to_memb:
36 ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2.
37  sublist S (hd::tl) l2 → memb S hd l2.
38 #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize //
39qed.
40
41lemma sublist_hd_tl_to_sublist:
42 ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2.
43  sublist S (hd::tl) l2 → sublist S tl l2.
44 #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H
45qed.
46
47lemma memb_to_sublist_to_memb:
48 ∀T:DeqSet. ∀x:T. ∀l1,l2: list T.
49  memb … x l1 → sublist … l1 l2 → memb … x l2.
50 #T #x #l1 elim l1
51 [ #l2 #abs cases abs
52 | #hd #tl #IH #l2 whd in match (memb ???); inversion (x==hd) /3/
53   #H #_ whd in match (sublist ???); <(\P H) cases (memb ???) // ]
54qed.
55
56lemma sublist_insert_snd_pos:
57 ∀S:DeqSet. ∀x,y:S. ∀l1,l2:list S.
58  sublist S l1 (x::l2) → sublist S l1 (x::y::l2).
59 #S #x #y #l1 elim l1 [//]
60 #hd #tl #IH #l2 #H
61 lapply (sublist_hd_tl_to_sublist … H) #K
62 whd in match (sublist ???); >(?:hd∈x::y::l2 = true) /2/
63 lapply (sublist_hd_tl_to_memb … H) normalize cases (hd==x) normalize //
64 cases (hd==y) normalize // cases (hd∈l2) // #H cases H
65qed.
66
67lemma sublist_tl_hd_tl:
68 ∀S:DeqSet. ∀hd:S. ∀tl:list S. sublist S tl (hd::tl).
69 #S #hd #tl elim tl try %
70 #hd' #tl' #IH whd in match (sublist ???);
71 whd in match (hd' ∈ hd::?::?); cases (hd'==hd)
72 whd in match (hd' ∈ ?::?); >(\b ?) try % normalize
73 lapply (sublist_insert_snd_pos … hd' … IH)
74 cases (sublist ???) //
75qed.
76
77lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l.
78 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) //
79qed.
Note: See TracBrowser for help on using the repository browser.