source: src/utilities/lists.ma @ 1921

Last change on this file since 1921 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 8.5 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
136unification hint 0 ≔ X ;
137N ≟ max_def List
138(*---------------------------*)⊢
139list X ≡ monad N X.
140
141definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.
142
143lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
144#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
145#x' * #EQx' >EQx' //
146qed.
147
148lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
149#A#P#l elim l
150[#_ %
151|#x #l' #IH #H %
152  [ @H % %
153  | @IH #y #G @H %2 @G
154  ]
155]
156qed.
157
158
159lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
160#A#l1 elim l1 normalize
161[ #l2 #n #ABS elim (absurd ? ABS ?) //
162| #x #l' #IH #l2 #n cases n normalize
163  [//
164  | #n #H @IH @le_S_S_to_le assumption
165  ]
166]
167qed.
168
169lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
170#A#l1 elim l1
171[#l2 #n #_ <minus_n_O %
172|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
173  cases n -n
174  [  #ABS elim (absurd ? ABS ?) //
175  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
176  ]
177]
178qed.
179
180lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
181  nth_opt A n (l1 @ l2) = Some ? x.
182#A #l1 elim l1 normalize
183[ #l2 #n #x #ABS destruct
184| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
185]
186qed.
187
188lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
189  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
190#A #l1 elim l1 normalize
191[ #l2 #n #_ <minus_n_O %
192| #hd #tl #IH #l2 * [2: #n] normalize
193  [ @IH
194  | #ABS destruct(ABS)
195  ]
196]
197qed.
198
199 
200(* count occurrences satisfying a test *)
201let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
202  match l with
203  [ nil ⇒ 0
204  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
205  ].
206 
207theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
208#A #f #l1 elim l1
209[ #l2 %
210| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
211]
212qed.
213
214
215include "utilities/option.ma".
216
217lemma position_of_from_aux : ∀A,test,l,n.
218  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
219#A #test #l elim l
220[ normalize #_ %
221| #hd #tl #IH #n
222  normalize in ⊢ (??%?); >IH
223  normalize elim (test hd) normalize
224  [ <plus_n_O %
225  | >(IH 1) whd in match (position_of ???);
226    elim (position_of_aux ??? 0) normalize
227    [ % | #x <plus_n_Sm % ]
228  ]
229]
230qed.
231
232definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
233  opt_safe ? (position_of A test l) ?.
234  lapply prf -prf elim l normalize
235  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
236  |#hd #tl #IH elim (test hd) normalize
237    [2: >position_of_from_aux #H
238      change with (position_of_aux ????) in match (position_of ???);
239      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
240    #_ % #ABS destruct(ABS)
241qed.
242
243definition index_of ≝
244  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
245  lapply prf -prf @eqb_elim #EQ * >EQ %
246qed.
247
248lemma position_of_append_hit : ∀A,test,l1,l2,x.
249  position_of A test (l1@l2) = Some ? x →
250    position_of A test l1 = Some ? x ∨
251      (position_of A test l1 = None ? ∧
252        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
253#A#test#l1 elim l1
254[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
255  % %
256| #hd #tl #IH #l2 #x
257  normalize elim (test hd) normalize
258  [#H %{H}
259  | >position_of_from_aux
260    lapply (refl … (position_of A test (tl@l2)))
261    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
262    normalize #EQ destruct(EQ)
263    elim (IH … Heq) -IH
264    [ #G %
265    | * #G #H
266     lapply (refl … (position_of A test l2))
267     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
268     #EQ destruct (EQ) %2 %]
269    >position_of_from_aux
270    [1,2: >G % | >H' %]
271  ]
272]
273qed.
274
275lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
276  count A test l ≥ 1.
277#A#test#l elim l normalize
278[#x #ABS destruct(ABS)
279|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
280  >position_of_from_aux
281  lapply (refl … (position_of ? test tl))
282  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
283  #EQ destruct(EQ) @(IH … Heq)
284]
285qed.
286
287lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
288  count A test l = 0.
289#A#test#l elim l normalize
290[ #_ %
291|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
292  >position_of_from_aux
293  lapply (refl … (position_of ? test tl))
294  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
295  #EQ destruct(EQ) @(IH … Heq)
296]
297qed.
298
299
300lemma position_of_append_miss : ∀A,test,l1,l2.
301  position_of A test (l1@l2) = None ? →
302    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
303#A#test#l1 elim l1
304[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
305| #hd #tl #IH #l2
306  normalize elim (test hd) normalize
307  [#H destruct(H)
308  | >position_of_from_aux
309    lapply (refl … (position_of A test (tl@l2)))
310    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
311    normalize #EQ destruct(EQ)
312    elim (IH … Heq) #H1 #H2
313    >position_of_from_aux
314    >position_of_from_aux
315    >H1 >H2 normalize % %
316  ]
317]
318qed.
319
320
Note: See TracBrowser for help on using the repository browser.