Changeset 230 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Nov 10, 2010, 5:26:08 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r229 r230 6 6 include "Nat.ma". 7 7 include "Util.ma". 8 (* include "List.ma". *) 8 include "List.ma". 9 9 10 10 include "logic/pts.ma". … … 58 58 ∀a:A. 59 59 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 60 #A; 61 #a; 62 #P; 63 #H; 64 #x; 65 #p; 66 ngeneralize in match H; 67 ngeneralize in match P; 68 ncases p; 69 //; 60 #A a P H x p. 61 ngeneralize in match H. 62 ngeneralize in match P. 63 ncases p. 64 //. 70 65 nqed. 71 66 … … 92 87 ] 93 88 nqed. 89 90 nlet rec append (A: Type[0]) (n: Nat) (m: Nat) 91 (v: Vector A n) (q: Vector A m) on v ≝ 92 match v return (λn.λv. Vector A (n + m)) with 93 [ Empty ⇒ q 94  Cons o hd tl ⇒ hd :: (append A o m tl q) 95 ]. 96 97 nlet rec reverse (A: Type[0]) (n: Nat) 98 (v: Vector A n) on v ≝ 99 match v return (λm.λv. Vector A m) with 100 [ Empty ⇒ Empty A 101  Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A))) 102 ]. 103 //. 104 nqed. 105 106 nlet rec to_list (A: Type[0]) (n: Nat) 107 (v: Vector A n) on v ≝ 108 match v with 109 [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A 110  Cons o hd tl ⇒ hd :: (to_list A o tl) 111 ]. 112 113 nlet rec rotate_left (A: Type[0]) (n: Nat) (v: Vector A n) 114 (m: Nat) on m: Vector A n ≝ 115 match m with 116 [ Z ⇒ v 117  S o ⇒ 118 match v with 119 [ Empty ⇒ Empty A 120  Cons p hd tl ⇒ 121 rotate_left A (S p) (? (append A p ? tl (Cons A ? hd (Empty A)))) o 122 ] 123 ]. 124 //. 125 nqed. 126 127 nlemma map_fusion: 128 ∀A, B, C: Type[0]. 129 ∀n: Nat. 130 ∀v: Vector A n. 131 ∀f: A → B. 132 ∀g: B → C. 133 map B C n g (map A B n f v) = map A C n (λx. g (f x)) v. 134 #A B C n v f g. 135 nelim v. 136 nnormalize. 137 @. 138 #N H V H2. 139 nnormalize. 140 nrewrite > H2. 141 @. 142 nqed. 143 144 nlemma length_correct: 145 ∀A: Type[0]. 146 ∀n: Nat. 147 ∀v: Vector A n. 148 length A n v = n. 149 #A n v. 150 nelim v. 151 nnormalize. 152 @. 153 #N H V H2. 154 nnormalize. 155 nrewrite > H2. 156 @. 157 nqed. 158 159 nlemma map_length: 160 ∀A, B: Type[0]. 161 ∀n: Nat. 162 ∀v: Vector A n. 163 ∀f: A → B. 164 length A n v = length B n (map A B n f v). 165 #A B n v f. 166 nelim v. 167 nnormalize. 168 @. 169 #N H V H2. 170 nnormalize. 171 nrewrite > H2. 172 @. 173 nqed.
Note: See TracChangeset
for help on using the changeset viewer.