source: src/utilities/lists.ma @ 1949

Last change on this file since 1949 was 1949, checked in by tranquil, 8 years ago
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File size: 8.6 KB
Line 
1include "basics/lists/list.ma".
2include "ASM/Util.ma". (* coercion from bool to Prop *)
3
4lemma All_map : ∀A,B,P,Q,f,l.
5All A P l →
6(∀a.P a → Q (f a)) →
7All B Q (map A B f l).
8#A #B #P #Q #f #l elim l //
9#h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed.
10
11lemma Exists_map : ∀A,B,P,Q,f,l.
12Exists A P l →
13(∀a.P a → Q (f a)) →
14Exists B Q (map A B f l).
15#A #B #P #Q #f #l elim l //
16#h #t #IH * #H #F
17[ %1 @(F ? H) | %2 @(IH H F) ]
18qed.
19
20lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r).
21#A #P #l elim l
22[ //
23| #hd #tl #IH #r * #H1 #H2 #H3 % // @IH //
24] qed.
25
26lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l.
27#A #P #l elim l
28[ //
29| #hd #tl #IH #r * #H1 #H2 % /2/
30] qed.
31
32lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r.
33#A #P #l elim l
34[ //
35| #h #t #IH #r * /2/
36] qed.
37
38(* An alternative form of All that can be easier to use sometimes. *)
39lemma All_alt : ∀A,P,l.
40  (∀a,pre,post. l = pre@a::post → P a) →
41  All A P l.
42#A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?);
43generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %);
44[ #pre #E %
45| #a #tl #IH #pre #E %
46  [ @(H a pre tl E)
47  | @(IH (pre@[a])) >associative_append @E
48  ]
49] qed.
50
51lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x.
52#A #P #l elim l
53[ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS)
54| #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ)
55  [ @(IH Ptl … (refl …))
56  | @Phd
57  ]
58]
59qed.
60
61let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
62match la with
63[ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ]
64| cons ha ta ⇒
65    match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ]
66].
67
68lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|.
69#A #B #P #la elim la
70[ * [ // | #x #y * ]
71| #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl
72] qed.
73
74lemma All2_mp : ∀A,B,P,Q,la,lb. (∀a,b. P a b → Q a b) → All2 A B P la lb → All2 A B Q la lb.
75#A #B #P #Q #la elim la
76[ * [ // | #h #t #_ * ]
77| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
78] qed.
79
80let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝
81match l return λl. All A P l → ? with
82[ nil ⇒ λ_. nil B
83| cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H))
84] H.
85
86lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l).
87#A#P#l elim l //
88#h #t #Hi * #Ph #Pt normalize
89>rev_append_def
90@All_append
91[ @(Hi Pt)
92| %{Ph I}
93]
94qed.
95
96lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l).
97#A#P#l elim l //
98#h #t #Hi normalize >rev_append_def
99* [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)]
100qed.
101
102include "utilities/option.ma".
103
104lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) →
105  ∀l. All ? P l → opt_All ? Q (find … f l).
106#A#B#P#Q#f#H#l elim l [#_%]
107#x #l' #Hi
108* #Px #AllPl'
109whd in ⊢ (???%);
110lapply (H x Px)
111lapply (refl ? (f x))
112generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//]
113#_ whd in ⊢ (???%); @(Hi AllPl')
114qed.
115
116include "utilities/monad.ma".
117
118definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
119// qed.
120
121definition List ≝ MakeMonadProps
122  list
123  (λX,x.[x])
124  (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l)
125  ????. normalize
126[ / by /
127| #X#m elim m normalize //
128| #X#Y#Z #m #f#g
129  elim m normalize [//]
130  #x#l' #Hi elim (f x)
131  [@Hi] normalize #hd #tl #IH >associative_append >IH %
132|#X#Y#m #f #g #H elim m normalize [//]
133  #hd #tl #IH >H >IH %
134] qed.
135
136alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
137unification hint 0 ≔ X ;
138N ≟ max_def List
139(*---------------------------*)⊢
140list X ≡ monad N X.
141
142definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.
143
144lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
145#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
146#x' * #EQx' >EQx' //
147qed.
148
149lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
150#A#P#l elim l
151[#_ %
152|#x #l' #IH #H %
153  [ @H % %
154  | @IH #y #G @H %2 @G
155  ]
156]
157qed.
158
159
160lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
161#A#l1 elim l1 normalize
162[ #l2 #n #ABS elim (absurd ? ABS ?) //
163| #x #l' #IH #l2 #n cases n normalize
164  [//
165  | #n #H @IH @le_S_S_to_le assumption
166  ]
167]
168qed.
169
170lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
171#A#l1 elim l1
172[#l2 #n #_ <minus_n_O %
173|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
174  cases n -n
175  [  #ABS elim (absurd ? ABS ?) //
176  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
177  ]
178]
179qed.
180
181lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
182  nth_opt A n (l1 @ l2) = Some ? x.
183#A #l1 elim l1 normalize
184[ #l2 #n #x #ABS destruct
185| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
186]
187qed.
188
189lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
190  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
191#A #l1 elim l1 normalize
192[ #l2 #n #_ <minus_n_O %
193| #hd #tl #IH #l2 * [2: #n] normalize
194  [ @IH
195  | #ABS destruct(ABS)
196  ]
197]
198qed.
199
200 
201(* count occurrences satisfying a test *)
202let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
203  match l with
204  [ nil ⇒ 0
205  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
206  ].
207 
208theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
209#A #f #l1 elim l1
210[ #l2 %
211| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
212]
213qed.
214
215
216include "utilities/option.ma".
217
218lemma position_of_from_aux : ∀A,test,l,n.
219  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
220#A #test #l elim l
221[ normalize #_ %
222| #hd #tl #IH #n
223  normalize in ⊢ (??%?); >IH
224  normalize elim (test hd) normalize
225  [ <plus_n_O %
226  | >(IH 1) whd in match (position_of ???);
227    elim (position_of_aux ??? 0) normalize
228    [ % | #x <plus_n_Sm % ]
229  ]
230]
231qed.
232
233definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
234  opt_safe ? (position_of A test l) ?.
235  lapply prf -prf elim l normalize
236  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
237  |#hd #tl #IH elim (test hd) normalize
238    [2: >position_of_from_aux #H
239      change with (position_of_aux ????) in match (position_of ???);
240      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
241    #_ % #ABS destruct(ABS)
242qed.
243
244definition index_of ≝
245  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
246  lapply prf -prf @eqb_elim #EQ * >EQ %
247qed.
248
249lemma position_of_append_hit : ∀A,test,l1,l2,x.
250  position_of A test (l1@l2) = Some ? x →
251    position_of A test l1 = Some ? x ∨
252      (position_of A test l1 = None ? ∧
253        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
254#A#test#l1 elim l1
255[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
256  % %
257| #hd #tl #IH #l2 #x
258  normalize elim (test hd) normalize
259  [#H %{H}
260  | >position_of_from_aux
261    lapply (refl … (position_of A test (tl@l2)))
262    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
263    normalize #EQ destruct(EQ)
264    elim (IH … Heq) -IH
265    [ #G %
266    | * #G #H
267     lapply (refl … (position_of A test l2))
268     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
269     #EQ destruct (EQ) %2 %]
270    >position_of_from_aux
271    [1,2: >G % | >H' %]
272  ]
273]
274qed.
275
276lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
277  count A test l ≥ 1.
278#A#test#l elim l normalize
279[#x #ABS destruct(ABS)
280|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
281  >position_of_from_aux
282  lapply (refl … (position_of ? test tl))
283  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
284  #EQ destruct(EQ) @(IH … Heq)
285]
286qed.
287
288lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
289  count A test l = 0.
290#A#test#l elim l normalize
291[ #_ %
292|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
293  >position_of_from_aux
294  lapply (refl … (position_of ? test tl))
295  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
296  #EQ destruct(EQ) @(IH … Heq)
297]
298qed.
299
300
301lemma position_of_append_miss : ∀A,test,l1,l2.
302  position_of A test (l1@l2) = None ? →
303    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
304#A#test#l1 elim l1
305[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
306| #hd #tl #IH #l2
307  normalize elim (test hd) normalize
308  [#H destruct(H)
309  | >position_of_from_aux
310    lapply (refl … (position_of A test (tl@l2)))
311    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
312    normalize #EQ destruct(EQ)
313    elim (IH … Heq) #H1 #H2
314    >position_of_from_aux
315    >position_of_from_aux
316    >H1 >H2 normalize % %
317  ]
318]
319qed.
320
321
Note: See TracBrowser for help on using the repository browser.