Changeset 231
 Timestamp:
 Nov 11, 2010, 12:27:04 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r230 r231 31 31 λc: BitVector n. 32 32 zip Bool Bool Bool n exclusive_disjunction b c. 33 34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝ 35 
Deliverables/D4.1/Matita/Nat.ma
r230 r231 50 50 interpretation "Nat multiplication" 'times n m = (multiplication n m). 51 51 52 nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝ 53 match n with 54 [ Z ⇒ True 55  S o ⇒ 56 match m with 57 [ Z ⇒ False 58  S p ⇒ less_than_or_equal o p 59 ] 60 ]. 61 62 notation "n break ≤ m" 63 non associative with precedence 47 64 for @{ 'less_than_or_equal $n $m }. 65 66 interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m). 67 52 68 nlemma plus_zero: 53 69 ∀n: Nat. 
Deliverables/D4.1/Matita/Vector.ma
r230 r231 10 10 include "logic/pts.ma". 11 11 include "Plogic/equality.ma". 12 13 (* ===================================== *) 14 (* The datatype. *) 15 (* ===================================== *) 12 16 13 17 ninductive Vector (A: Type[0]): Nat → Type[0] ≝ … … 21 25 interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl). 22 26 27 (* ===================================== *) 28 (* Lookup. *) 29 (* ===================================== *) 30 31 (* ===================================== *) 32 (* Folds and builds. *) 33 (* ===================================== *) 34 35 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat) 36 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 37 match v with 38 [ Empty ⇒ x 39  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 40 ]. 41 42 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) 43 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 44 match v with 45 [ Empty ⇒ x 46  Cons n hd tl ⇒ f (fold_left A B n f x tl) hd 47 ]. 48 49 (* ===================================== *) 50 (* Maps and zips. *) 51 (* ===================================== *) 52 23 53 nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat) 24 54 (f: A → B) (v: Vector A n) on v ≝ … … 27 57  Cons n hd tl ⇒ (f hd) :: (map A B n f tl) 28 58 ]. 29 30 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat) 31 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 32 match v with 33 [ Empty ⇒ x 34  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 35 ]. 36 37 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) 38 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 39 match v with 40 [ Empty ⇒ x 41  Cons n hd tl ⇒ f (fold_left A B n f x tl) hd 42 ]. 43 44 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝ 45 match v with 46 [ Empty ⇒ Z 47  Cons n hd tl ⇒ S $ length A n tl 48 ]. 49 50 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝ 51 match n return λn. Vector A n with 52 [ Z ⇒ Empty A 53  S m ⇒ h :: (replicate A m h) 54 ]. 55 59 60 (* Should be moved into Plogic/equality.ma at some point. Only Type[2] version 61 currently in there. 62 *) 56 63 nlemma eq_rect_Type0_r : 57 64 ∀A: Type[0]. … … 88 95 nqed. 89 96 97 (* ===================================== *) 98 (* Building vectors from scratch *) 99 (* ===================================== *) 100 101 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝ 102 match n return λn. Vector A n with 103 [ Z ⇒ Empty A 104  S m ⇒ h :: (replicate A m h) 105 ]. 106 90 107 nlet rec append (A: Type[0]) (n: Nat) (m: Nat) 91 108 (v: Vector A n) (q: Vector A m) on v ≝ … … 94 111  Cons o hd tl ⇒ hd :: (append A o m tl q) 95 112 ]. 113 114 notation "v break @ q" 115 right associative with precedence 47 116 for @{ 'append $v $q }. 117 118 interpretation "Vector append" 'append hd tl = (append ? ? hd tl). 119 120 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat) 121 (f: A → B → A) (a: A) (v: Vector B n) on v ≝ 122 a :: 123 (match v with 124 [ Empty ⇒ Empty A 125  Cons o hd tl ⇒ scan_left A B o f (f a hd) tl 126 ]). 127 128 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat) 129 (f: A → B → A) (b: B) (v: Vector A n) on v ≝ 130 match v with 131 [ Empty ⇒ ? 132  Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl) 133 ]. 134 //. 135 nqed. 136 137 (* ===================================== *) 138 (* Other manipulations. *) 139 (* ===================================== *) 140 141 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝ 142 match v with 143 [ Empty ⇒ Z 144  Cons n hd tl ⇒ S $ length A n tl 145 ]. 96 146 97 147 nlet rec reverse (A: Type[0]) (n: Nat) … … 104 154 nqed. 105 155 156 (* ===================================== *) 157 (* Conversions to and from lists. *) 158 (* ===================================== *) 159 106 160 nlet rec to_list (A: Type[0]) (n: Nat) 107 161 (v: Vector A n) on v ≝ … … 110 164  Cons o hd tl ⇒ hd :: (to_list A o tl) 111 165 ]. 112 113 nlet rec rotate_left (A: Type[0]) (n: Nat) (v: Vector A n) 114 (m: Nat) on m: Vector A n ≝ 166 167 nlet rec from_list (A: Type[0]) (l: List A) on l ≝ 168 match l return λl. Vector A (length A l) with 169 [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A 170  Cons hd tl ⇒ ? (hd :: (from_list A tl)) 171 ]. 172 //. 173 nqed. 174 175 (* ===================================== *) 176 (* Rotates and shifts. *) 177 (* ===================================== *) 178 179 nlet rec rotate_left (A: Type[0]) (n: Nat) 180 (m: Nat) (v: Vector A n) on m: Vector A n ≝ 115 181 match m with 116 182 [ Z ⇒ v … … 119 185 [ Empty ⇒ Empty A 120 186  Cons p hd tl ⇒ 121 rotate_left A (S p) (? (append A p ? tl (Cons A ? hd (Empty A)))) o187 rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A)))) 122 188 ] 123 189 ]. 124 190 //. 125 191 nqed. 192 193 ndefinition rotate_right ≝ 194 λA: Type[0]. 195 λn, m: Nat. 196 λv: Vector A n. 197 reverse A n (rotate_left A n m (reverse A n v)). 198 199 (* ===================================== *) 200 (* Lemmas. *) 201 (* ===================================== *) 126 202 127 203 nlemma map_fusion: … … 172 248 @. 173 249 nqed. 250 251 nlemma from_list_to_list_left_inverse: 252 ∀A: Type[0]. 253 ∀l: List A. 254 to_list A (length A l) (from_list A l) = l.
Note: See TracChangeset
for help on using the changeset viewer.