source: src/utilities/lists.ma @ 1631

Last change on this file since 1631 was 1631, checked in by campbell, 10 years ago

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

File size: 1.7 KB
Line 
1include "basics/lists/list.ma".
2
3lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r).
4#A #P #l elim l
5[ //
6| #hd #tl #IH #r * #H1 #H2 #H3 % // @IH //
7] qed.
8
9lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l.
10#A #P #l elim l
11[ //
12| #hd #tl #IH #r * #H1 #H2 % /2/
13] qed.
14
15lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r.
16#A #P #l elim l
17[ //
18| #h #t #IH #r * /2/
19] qed.
20
21(* An alternative form of All that can be easier to use sometimes. *)
22lemma All_alt : ∀A,P,l.
23  (∀a,pre,post. l = pre@a::post → P a) →
24  All A P l.
25#A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?);
26generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %);
27[ #pre #E %
28| #a #tl #IH #pre #E %
29  [ @(H a pre tl E)
30  | @(IH (pre@[a])) >associative_append @E
31  ]
32] qed.
33
34let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
35match la with
36[ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ]
37| cons ha ta ⇒
38    match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ]
39].
40
41lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|.
42#A #B #P #la elim la
43[ * [ // | #x #y * ]
44| #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl
45] qed.
46
47lemma 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.
48#A #B #P #Q #la elim la
49[ * [ // | #h #t #_ * ]
50| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
51] qed.
52
53let 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 ≝
54match l return λl. All A P l → ? with
55[ nil ⇒ λ_. nil B
56| cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H))
57] H.
58
Note: See TracBrowser for help on using the repository browser.