source: src/utilities/lists.ma @ 1651

Last change on this file since 1651 was 1647, checked in by tranquil, 8 years ago
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File size: 2.2 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
59include "utilities/monad.ma".
60
61definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
62// qed.
63
64definition List ≝ MakeMonadProps
65  list
66  (λX,x.[x])
67  (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
68  ???. normalize
69[ / by /
70| #X#m elim m normalize //
71| #X#Y#Z #m #f#g
72  elim m normalize [//]
73  #x#l' #Hi
74  <(fold_sum ?? (f x) ? [ ] (Append ?))
75  >Hi //
76] qed.
77
78unification hint 0 ≔ X ;
79N ≟ max_def List, M ≟ m_def N
80(*---------------------------*)⊢
81list X ≡ monad M X.
Note: See TracBrowser for help on using the repository browser.