(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Vectors.ma: Fixed length bitvectors, and routine operations on them. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) include "Cartesian.ma". include "Nat.ma". (* include "List.ma". *) include "logic/pts.ma". include "Plogic/equality.ma". ninductive Vector (A: Type[0]): Nat → Type[0] ≝ Empty: Vector A Z | Cons: ∀n: Nat. A → Vector A n → Vector A (S n). notation "hvbox(hd break :: tl)" right associative with precedence 52 for @{ 'Cons \$hd \$tl }. interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl). 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 ⇒ (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 ⇒ Z | Cons n hd tl ⇒ S (length A n tl) ]. nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝ match n return λn. Vector A n with [ Z ⇒ Empty A | S m ⇒ h :: (replicate A m h) ]. nlemma eq_rect_Type0_r : ∀A: Type[0]. ∀a:A. ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. #A; #a; #P; #H; #x; #p; ngeneralize in match H; ngeneralize in match P; ncases p; //; nqed. nlet rec zip (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ (match v return (λx.λr. x = n → Vector C x) with [ Empty ⇒ λ_. Empty C | Cons n hd tl ⇒ match q return (λy.λr. S n = y → Vector C (S n)) with [ Empty ⇒ ? | Cons m hd2 tl2 ⇒ λe: S n = S m. Cons C n (f hd hd2) (zip A B C n f tl ?) ] ]) (refl ? n). ## [ #e; ndestruct (e); ## | ndestruct (e); napply tl2 ## ] nqed.