[1626] | 1 | include "basics/lists/list.ma". |
---|
| 2 | |
---|
[1630] | 3 | lemma 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 // |
---|
[1631] | 7 | ] qed. |
---|
[1630] | 8 | |
---|
[1631] | 9 | lemma 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 | |
---|
| 15 | lemma 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 | |
---|
[1628] | 21 | (* An alternative form of All that can be easier to use sometimes. *) |
---|
| 22 | lemma 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 ⊢ (???% → ?); |
---|
| 26 | generalize 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 | |
---|
[1626] | 34 | let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ |
---|
| 35 | match 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 | |
---|
| 41 | lemma 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 | |
---|
| 47 | lemma 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. |
---|
[1630] | 52 | |
---|
| 53 | let 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 ≝ |
---|
| 54 | match 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 | |
---|
[1647] | 59 | include "utilities/monad.ma". |
---|
| 60 | |
---|
| 61 | definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?. |
---|
| 62 | // qed. |
---|
| 63 | |
---|
| 64 | definition 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 | |
---|
| 78 | unification hint 0 ≔ X ; |
---|
| 79 | N ≟ max_def List, M ≟ m_def N |
---|
| 80 | (*---------------------------*)⊢ |
---|
| 81 | list X ≡ monad M X. |
---|