Changeset 222
 Timestamp:
 Nov 8, 2010, 1:53:17 PM (9 years ago)
 File:

 1 moved
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vectors.ma
r221 r222 1 (* ===================================== *) 2 (* Vectors.ma: Fixed length bitvectors, and routine operations on them. *) 3 (* ===================================== *) 4 5 include "logic/pts.ma". 6 include "basics/eq.ma". 7 include "basics/bool.ma". 8 include "arithmetics/nat.ma". 9 include "nat/plus.ma". 10 include "nat/minus.ma". 11 12 ninductive Vector (A: Type[0]): nat → Type[0] ≝ 13 Empty: Vector A 0 14  Cons: ∀n: nat. A → Vector A n → Vector A (n + 1). 15 16 nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝ 17 match v with 18 [ Empty ⇒ Empty B 19  Cons n hd tl ⇒ Cons B n (f hd) (map A B n f tl) 20 ]. 21 22 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat) 23 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 24 match v with 25 [ Empty ⇒ x 26  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 27 ]. 28 29 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat) 30 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 31 match v with 32 [ Empty ⇒ x 33  Cons n hd tl ⇒ f (fold_left A B n f x tl) hd 34 ]. 35 36 nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ 37 match v with 38 [ Empty ⇒ 0 39  Cons n hd tl ⇒ 1 + length A n tl 40 ]. 41 42 nlet rec append (A: Type[0]) (n: nat) (m: nat) 43 (v: Vector A n) (q: Vector A m) on v ≝ 44 match v with 45 [ Empty ⇒ q 46  Cons n hd tl ⇒ Cons n hd (append A n m tl q) 47 ]. 48 49 (* 50 nlet rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ 51 match v with 52 [ Empty ⇒ Empty A 53  Cons n hd tl ⇒ append 54 55 nlemma length_correct: 56 ∀A: Type[0]. 57 ∀n: nat. 58 ∀v: Vector A n. 59 length A n v = n. 60 #A n v; 61 nelim v. 62 nnormalize. 63 @. 64 #n0 H V H. 65 nnormalize. 66 nrewrite > H. 67 *)
Note: See TracChangeset
for help on using the changeset viewer.