(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Vector.ma: Fixed length polymorphic vectors, and routine operations on *) (* them. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) include "Cartesian.ma". include "Nat.ma". include "Util.ma". include "List.ma". include "logic/pts.ma". include "Plogic/equality.ma". (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* The datatype. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 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). (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Lookup. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Folds and builds. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 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 ]. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Maps and zips. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 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) ]. (* Should be moved into Plogic/equality.ma at some point. Only Type[2] version currently in there. *) 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 hd' tl' ⇒ λe: S n = S m. (f hd hd') :: (zip A B C n f tl ?) ] ]) (refl ? n). ## [ #e; ndestruct(e); ## | ndestruct(e); napply tl' ## ] nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Building vectors from scratch *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 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) ]. nlet rec append (A: Type[0]) (n: Nat) (m: Nat) (v: Vector A n) (q: Vector A m) on v ≝ match v return (λn.λv. Vector A (n + m)) with [ Empty ⇒ q | Cons o hd tl ⇒ hd :: (append A o m tl q) ]. notation "v break @ q" right associative with precedence 47 for @{ 'append \$v \$q }. interpretation "Vector append" 'append hd tl = (append ? ? hd tl). nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat) (f: A → B → A) (a: A) (v: Vector B n) on v ≝ a :: (match v with [ Empty ⇒ Empty A | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl ]). nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat) (f: A → B → A) (b: B) (v: Vector A n) on v ≝ match v with [ Empty ⇒ ? | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl) ]. //. nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Other manipulations. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 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 reverse (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝ match v return (λm.λv. Vector A m) with [ Empty ⇒ Empty A | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A))) ]. //. nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Conversions to and from lists. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec to_list (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝ match v with [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A | Cons o hd tl ⇒ hd :: (to_list A o tl) ]. (* nlet rec from_list (A: Type[0]) (l: List A) on l ≝ match l return λl. Vector A (length A l) with [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A | Cons hd tl ⇒ ? (hd :: (from_list A tl)) ]. //. nqed. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Rotates and shifts. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec rotate_left (A: Type[0]) (n: Nat) (m: Nat) (v: Vector A n) on m: Vector A n ≝ match m with [ Z ⇒ v | S o ⇒ match v with [ Empty ⇒ Empty A | Cons p hd tl ⇒ rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A)))) ] ]. //. nqed. ndefinition rotate_right ≝ λA: Type[0]. λn, m: Nat. λv: Vector A n. reverse A n (rotate_left A n m (reverse A n v)). (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Lemmas. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlemma map_fusion: ∀A, B, C: Type[0]. ∀n: Nat. ∀v: Vector A n. ∀f: A → B. ∀g: B → C. map B C n g (map A B n f v) = map A C n (λx. g (f x)) v. #A B C n v f g. nelim v. nnormalize. @. #N H V H2. nnormalize. nrewrite > H2. @. nqed. nlemma length_correct: ∀A: Type[0]. ∀n: Nat. ∀v: Vector A n. length A n v = n. #A n v. nelim v. nnormalize. @. #N H V H2. nnormalize. nrewrite > H2. @. nqed. nlemma map_length: ∀A, B: Type[0]. ∀n: Nat. ∀v: Vector A n. ∀f: A → B. length A n v = length B n (map A B n f v). #A B n v f. nelim v. nnormalize. @. #N H V H2. nnormalize. nrewrite > H2. @. nqed.