# Changeset 222 for Deliverables/D4.1/Matita

Ignore:
Timestamp:
Nov 8, 2010, 1:53:17 PM (10 years ago)
Message:

Datatype for fixed length lists (vectors) as well as some recursive functions over them (folds, etc.)

File:
1 moved

Unmodified
Removed
• ## Deliverables/D4.1/Matita/Vectors.ma

 r221 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Vectors.ma: Fixed length bitvectors, and routine operations on them.       *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) include "logic/pts.ma". include "basics/eq.ma". include "basics/bool.ma". include "arithmetics/nat.ma". include "nat/plus.ma". include "nat/minus.ma". ninductive Vector (A: Type[0]): nat → Type[0] ≝ Empty: Vector A 0 | Cons: ∀n: nat. A → Vector A n → Vector A (n + 1). nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝ match v with [ Empty ⇒ Empty B | Cons n hd tl ⇒ Cons B n (f hd) (map A B n f tl) ]. nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B → B) (x: B) (v: Vector A n) on v ≝ match v with [ Empty ⇒ x | Cons n hd tl ⇒ f hd (fold_right A B n f x tl) ]. nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B → A) (x: A) (v: Vector B n) on v ≝ match v with [ Empty ⇒ x | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd ]. nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ match v with [ Empty ⇒ 0 | Cons n hd tl ⇒ 1 + length A n tl ]. nlet rec append (A: Type[0]) (n: nat) (m: nat) (v: Vector A n) (q: Vector A m) on v ≝ match v with [ Empty ⇒ q | Cons n hd tl ⇒ Cons n hd (append A n m tl q) ]. (* nlet rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ match v with [ Empty ⇒ Empty A | Cons n hd tl ⇒ append nlemma length_correct: ∀A: Type[0]. ∀n: nat. ∀v: Vector A n. length A n v = n. #A n v; nelim v. nnormalize. @. #n0 H V H. nnormalize. nrewrite > H. *)
Note: See TracChangeset for help on using the changeset viewer.