Changeset 230
 Timestamp:
 Nov 10, 2010, 5:26:08 PM (11 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r228 r230 4 4 5 5 ndefinition BitVector ≝ λn: Nat. Vector Bool n. 6 ndefinition Bit ≝ BitVector (S Z). 7 ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). 8 ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). 9 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). 10 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). 6 11 7 12 ndefinition zero ≝ … … 26 31 λc: BitVector n. 27 32 zip Bool Bool Bool n exclusive_disjunction b c. 28 29 
Deliverables/D4.1/Matita/List.ma
r229 r230 2 2 include "Nat.ma". 3 3 include "Util.ma". 4 5 include "Plogic/equality.ma". 4 6 5 7 ninductive List (A: Type[0]): Type[0] ≝ … … 11 13 for @{ 'Cons $hd $tl }. 12 14 13 interpretation " Empty" 'Empty = (Empty ?).14 interpretation " Cons" 'Cons = (Cons ?).15 interpretation "List empty" 'Empty = (Empty ?). 16 interpretation "List cons" 'Cons = (Cons ?). 15 17 16 18 notation "[ list0 x sep ; ]" … … 27 29 match l with 28 30 [ Empty ⇒ m 29  Cons hd tl ⇒ hd :: (append A tl l)31  Cons hd tl ⇒ hd :: (append A tl m) 30 32 ]. 31 33 … … 34 36 for @{ 'append $l $r }. 35 37 36 interpretation " Append" 'append = (append ?).38 interpretation "List append" 'append = (append ?). 37 39 38 40 nlet rec fold_right (A: Type[0]) (B: Type[0]) … … 90 92  S o ⇒ a :: replicate A o a 91 93 ]. 94 95 nlemma append_empty: 96 ∀A: Type[0]. 97 ∀l: List A. 98 l @ (Empty A) = l. 99 #A l. 100 nelim l. 101 nnormalize. 102 @. 103 #H L H2. 104 nnormalize. 105 nrewrite > H2. 106 @. 107 nqed. 108 109 nlemma append_associative: 110 ∀A: Type[0]. 111 ∀l,m,n: List A. 112 l @ (m @ n) = (l @ m) @ n. 113 #A l m n. 114 nelim l. 115 nnormalize. 116 @. 117 #H L H2. 118 nnormalize. 119 nrewrite > H2. 120 @. 121 nqed. 122 123 nlemma reverse_append: 124 ∀A: Type[0]. 125 ∀l, m: List A. 126 reverse A (l @ m) = reverse A m @ reverse A l. 127 #A l m. 128 nelim l. 129 nnormalize. 130 napplyS append_empty. 131 #H L A. 132 nnormalize. 133 nrewrite > A. 134 napplyS append_associative. 135 nqed. 136 137 nlemma length_append: 138 ∀A: Type[0]. 139 ∀l, m: List A. 140 length A (l @ m) = length A l + length A m. 141 #A l m. 142 nelim l. 143 nnormalize. 144 @. 145 #H L H2. 146 nnormalize. 147 nrewrite > H2. 148 @. 149 nqed. 150 151 (* 152 nlemma length_reverse: 153 ∀A: Type[0]. 154 ∀l: List A. 155 length A (reverse A l) = length A l. 156 #A l. 157 nelim l. 158 nnormalize. 159 @. 160 #H L H2. 161 nnormalize. 162 napplyS length_append. 163 164 nlemma reverse_reverse: 165 ∀A: Type[0]. 166 ∀l: List A. 167 reverse A (reverse A l) = l. 168 #A l. 169 nelim l. 170 nnormalize. 171 @. 172 #H L H2. 173 nnormalize. 174 *) 
Deliverables/D4.1/Matita/Nat.ma
r228 r230 108 108 nqed. 109 109 110 nlemma multiplication_zero :110 nlemma multiplication_zero_right_neutral: 111 111 ∀m: Nat. 112 112 m * Z = Z. … … 151 151 napplyS multiplication_succ. 152 152 nqed. 153 153 154 nlemma multiplication_succ_zero_left_neutral: 155 ∀m: Nat. 156 (S Z) * m = m. 157 #m. 158 nelim m. 159 nnormalize. 160 @. 161 #N H. 162 nnormalize. 163 napplyS succ_plus. 164 nqed. 165 166 nlemma multiplication_succ_zero_right_neutral: 167 ∀m: Nat. 168 m * (S Z) = m. 169 #m. 170 nelim m. 171 nnormalize. 172 @. 173 #N H. 174 nnormalize. 175 nrewrite > H. 176 @. 177 nqed. 178 179 nlemma multiplication_distributes_right_plus: 180 ∀m, n, o: Nat. 181 (m + n) * o = m * o + n * o. 182 #m n o. 183 nelim m. 184 nnormalize. 185 @. 186 #N H. 187 nnormalize. 188 nrewrite > H. 189 napplyS plus_associative. 190 nqed. 191 192 nlemma multiplication_distributes_left_plus: 193 ∀m, n, o: Nat. 194 o * (m + n) = o * m + o * n. 195 #m n o. 196 napplyS multiplication_symmetrical. 197 nqed. 198 199 nlemma mutliplication_associative: 200 ∀m, n, o: Nat. 201 m * (n * o) = (m * n) * o. 202 #m n o. 203 nelim m. 204 nnormalize. 205 @. 206 #N H. 207 nnormalize. 208 nrewrite > H. 209 napplyS multiplication_distributes_right_plus. 210 nqed. 211 212 nlemma minus_minus: 213 ∀n: Nat. 214 n  n = Z. 215 #n. 216 nelim n. 217 nnormalize. 218 @. 219 #N H. 220 nnormalize. 221 nrewrite > H. 222 @. 223 nqed. 224 225 (* 226 nlemma succ_injective: 227 ∀m, n: Nat. 228 S m = S n → m = n. 229 #m n. 230 nelim m. 231 #H. 232 ninversion H. 233 #H. 234 ndestruct 235 236 nlemma plus_minus_associate: 237 ∀m, n, o: Nat. 238 (m + n)  o = m + (n  o). 239 #m n o. 240 nelim m. 241 nnormalize. 242 @. 243 #N H. 244 245 246 nlemma plus_minus_inverses: 247 ∀m, n: Nat. 248 (m + n)  n = m. 249 #m n. 250 nelim m. 251 nnormalize. 252 napply minus_minus. 253 #N H. 254 *) 
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.