source: src/utilities/lists.ma @ 3081

Last change on this file since 3081 was 3081, checked in by campbell, 7 years ago

Tidy up recent work a little.

File size: 10.9 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
61(* Boolean predicate version of All *)
62
63let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝
64match l with
65[ nil ⇒ true
66| cons h t ⇒ P h ∧ all A P t
67].
68
69lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l.
70#A #P #l elim l
71[ % //
72| #h #t * #IH #IH' %
73  [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ]
74  | * #p #H whd in ⊢ (?%); >p /2/
75  ]
76] qed.
77
78lemma all_append : ∀A,p,l1,l2.
79  all A p (l1@l2) →
80  all A p l1 ∧ all A p l2.
81#A #p #l1 elim l1
82[ //
83| #h #t #IH #l2
84  whd in ⊢ (?% → ?(?%?));
85  cases (p h) //
86  @IH
87] qed.
88
89
90let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
91match la with
92[ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ]
93| cons ha ta ⇒
94    match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ]
95].
96
97lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|.
98#A #B #P #la elim la
99[ * [ // | #x #y * ]
100| #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl
101] qed.
102
103lemma 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.
104#A #B #P #Q #la elim la
105[ * [ // | #h #t #_ * ]
106| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
107] qed.
108
109lemma All2_left : ∀A,B,P,la,lb.
110  All2 A B P la lb → All A (λa.∃b.P a b) la.
111#A #B #P #la elim la
112[ //
113| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hdb} // | /2/ ]
114] qed.
115
116lemma All2_right : ∀A,B,P,la,lb.
117  All2 A B P la lb → All B (λb.∃a.P a b) lb.
118#A #B #P #la elim la
119[ * // #h #t *
120| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ]
121] qed.
122
123lemma All2_tail : ∀A,B,P,a,b.
124  All2 A B P a b →
125  All2 A B P (tail A a) (tail B b).
126#A #B #P * [2: #ah #at] * [2,4: #bh #bt]
127* //
128qed.
129
130let 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 ≝
131match l return λl. All A P l → ? with
132[ nil ⇒ λ_. nil B
133| cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H))
134] H.
135
136lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l).
137#A#P#l elim l //
138#h #t #Hi * #Ph #Pt normalize
139>rev_append_def
140@All_append
141[ @(Hi Pt)
142| %{Ph I}
143]
144qed.
145
146lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l).
147#A#P#l elim l //
148#h #t #Hi normalize >rev_append_def
149* [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)]
150qed.
151
152include "utilities/option.ma".
153
154lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) →
155  ∀l. All ? P l → opt_All ? Q (find … f l).
156#A#B#P#Q#f#H#l elim l [#_%]
157#x #l' #Hi
158* #Px #AllPl'
159whd in ⊢ (???%);
160lapply (H x Px)
161lapply (refl ? (f x))
162generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//]
163#_ whd in ⊢ (???%); @(Hi AllPl')
164qed.
165
166include "utilities/monad.ma".
167
168definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
169// qed.
170
171definition List ≝ MakeMonadProps
172  list
173  (λX,x.[x])
174  (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l)
175  ????. normalize
176[ / by /
177| #X#m elim m normalize //
178| #X#Y#Z #m #f#g
179  elim m normalize [//]
180  #x#l' #Hi elim (f x)
181  [@Hi] normalize #hd #tl #IH >associative_append >IH %
182|#X#Y#m #f #g #H elim m normalize [//]
183  #hd #tl #IH >H >IH %
184] qed.
185
186alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
187unification hint 0 ≔ X ;
188N ≟ max_def List
189(*---------------------------*)⊢
190list X ≡ monad N X.
191
192definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.
193
194lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
195#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
196#x' * #EQx' >EQx' //
197qed.
198
199lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
200#A#P#l elim l
201[#_ %
202|#x #l' #IH #H %
203  [ @H % %
204  | @IH #y #G @H %2 @G
205  ]
206]
207qed.
208
209
210lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
211#A#l1 elim l1 normalize
212[ #l2 #n #ABS elim (absurd ? ABS ?) //
213| #x #l' #IH #l2 #n cases n normalize
214  [//
215  | #n #H @IH @le_S_S_to_le assumption
216  ]
217]
218qed.
219
220lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
221#A#l1 elim l1
222[#l2 #n #_ <minus_n_O %
223|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
224  cases n -n
225  [  #ABS elim (absurd ? ABS ?) //
226  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
227  ]
228]
229qed.
230
231lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
232  nth_opt A n (l1 @ l2) = Some ? x.
233#A #l1 elim l1 normalize
234[ #l2 #n #x #ABS destruct
235| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
236]
237qed.
238
239lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
240  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
241#A #l1 elim l1 normalize
242[ #l2 #n #_ <minus_n_O %
243| #hd #tl #IH #l2 * [2: #n] normalize
244  [ @IH
245  | #ABS destruct(ABS)
246  ]
247]
248qed.
249
250 
251(* count occurrences satisfying a test *)
252let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
253  match l with
254  [ nil ⇒ 0
255  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
256  ].
257 
258theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
259#A #f #l1 elim l1
260[ #l2 %
261| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
262]
263qed.
264
265
266
267lemma flatten_append : ∀A,l1,l2.
268  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
269#A #l1 #l2
270elim l1
271[ %
272| #h #t #IH whd in ⊢ (??%(??%?));
273  change with (flatten ??) in match (foldr ?????); >IH
274  change with (flatten ??) in match (foldr ?????);
275  >associative_append %
276] qed.
277
278
279include "utilities/option.ma".
280
281lemma position_of_from_aux : ∀A,test,l,n.
282  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
283#A #test #l elim l
284[ normalize #_ %
285| #hd #tl #IH #n
286  normalize in ⊢ (??%?); >IH
287  normalize elim (test hd) normalize
288  [ <plus_n_O %
289  | >(IH 1) whd in match (position_of ???);
290    elim (position_of_aux ??? 0) normalize
291    [ % | #x <plus_n_Sm % ]
292  ]
293]
294qed.
295
296definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
297  opt_safe ? (position_of A test l) ?.
298  lapply prf -prf elim l normalize
299  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
300  |#hd #tl #IH elim (test hd) normalize
301    [2: >position_of_from_aux #H
302      change with (position_of_aux ????) in match (position_of ???);
303      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
304    #_ % #ABS destruct(ABS)
305qed.
306
307definition index_of ≝
308  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
309  lapply prf -prf @eqb_elim #EQ * >EQ %
310qed.
311
312lemma position_of_append_hit : ∀A,test,l1,l2,x.
313  position_of A test (l1@l2) = Some ? x →
314    position_of A test l1 = Some ? x ∨
315      (position_of A test l1 = None ? ∧
316        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
317#A#test#l1 elim l1
318[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
319  % %
320| #hd #tl #IH #l2 #x
321  normalize elim (test hd) normalize
322  [#H %{H}
323  | >position_of_from_aux
324    lapply (refl … (position_of A test (tl@l2)))
325    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
326    normalize #EQ destruct(EQ)
327    elim (IH … Heq) -IH
328    [ #G %
329    | * #G #H
330     lapply (refl … (position_of A test l2))
331     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
332     #EQ destruct (EQ) %2 %]
333    >position_of_from_aux
334    [1,2: >G % | >H' %]
335  ]
336]
337qed.
338
339lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
340  count A test l ≥ 1.
341#A#test#l elim l normalize
342[#x #ABS destruct(ABS)
343|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
344  >position_of_from_aux
345  lapply (refl … (position_of ? test tl))
346  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
347  #EQ destruct(EQ) @(IH … Heq)
348]
349qed.
350
351lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
352  count A test l = 0.
353#A#test#l elim l normalize
354[ #_ %
355|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
356  >position_of_from_aux
357  lapply (refl … (position_of ? test tl))
358  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
359  #EQ destruct(EQ) @(IH … Heq)
360]
361qed.
362
363
364lemma position_of_append_miss : ∀A,test,l1,l2.
365  position_of A test (l1@l2) = None ? →
366    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
367#A#test#l1 elim l1
368[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
369| #hd #tl #IH #l2
370  normalize elim (test hd) normalize
371  [#H destruct(H)
372  | >position_of_from_aux
373    lapply (refl … (position_of A test (tl@l2)))
374    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
375    normalize #EQ destruct(EQ)
376    elim (IH … Heq) #H1 #H2
377    >position_of_from_aux
378    >position_of_from_aux
379    >H1 >H2 normalize % %
380  ]
381]
382qed.
383
384
385(* A not terribly efficient sort for testing purposes *)
386
387let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝
388match l with
389[ nil ⇒ [a]
390| cons h t ⇒ if lt a h then a::h::t else h::(ordered_insert A lt a t)
391].
392
393let rec insert_sort (A:Type[0]) (lt:A → A → bool) (l:list A) on l : list A ≝
394match l with
395[ nil ⇒ [ ]
396| cons h t ⇒ ordered_insert A lt h (insert_sort A lt t)
397].
398
399(* range from 0 to n excluded with proof of minoration *)
400
401let rec range_strong_internal (index, how_many, end : ℕ) on how_many :
402  index + how_many = end →
403  list (Σn.n<end) ≝
404  match how_many return λhow_many.index + how_many = end → ? with
405  [ O ⇒ λ_.[ ]
406  | S k ⇒ λprf.«index, ?» :: range_strong_internal (S index) k end ?
407  ].
408<prf
409[ >(plus_n_O index) in ⊢ (?%?); @monotonic_lt_plus_r @le_S_S @le_O_n
410| @plus_n_Sm
411]
412qed.
413
414definition range_strong : ∀end.list (Σn.n < end) ≝
415λend.range_strong_internal 0 ? end (refl …).
Note: See TracBrowser for help on using the repository browser.