# Library vector

``` Require Export Arith. Section le_pirr.   Axiom le_pirr: forall i j (h h': i<=j), h=h'.   Theorem lt_pirr: forall i j (h h': i<j), h=h'.   Hint Immediate lt_pirr le_pirr. End le_pirr. Ltac lt_eq_lt x y H := destruct (lt_eq_lt_dec x y) as [H|H]; [ destruct H as [H|H] | idtac ]. Ltac gclear x := generalize x; clear x. Ltac gclear2 x y := generalize x y; clear x y. Ltac gclear3 x y z := generalize x y z; clear x y z. Ltac gclear4 x y z t := generalize x y z t; clear x y z t. Ltac vauto := autorewrite with vector; auto with arith. Section Vector.   Variable A: Set.   Inductive vector: nat -> Set :=     | nnil: vector 0     | ncons: forall (n: nat) (a: A), vector n -> vector (S n).   Definition head (n: nat) (l: vector (S n)): A :=     match l in vector k return 0<k -> A with     | nnil => fun h => False_rec A (lt_n_O _ h)     | ncons _ a _ => fun _ => a     end (lt_O_Sn n).   Definition tail (n: nat) (l: vector (S n)): vector n :=     match l in vector k return 0<k -> vector (pred k) with     | nnil => fun h => False_rec (vector (pred 0)) (lt_n_O _ h)     | ncons _ _ q => fun _ => q     end (lt_O_Sn n).   Fixpoint get (n: nat) (l: vector n) (k: nat) {struct l}: k<n -> A :=     match l in vector n return k < n -> A with     | nnil => fun h => False_rec _ (lt_n_O _ h)     | ncons n a q =>         match k return k < S n -> A with         | 0 => fun _ => a         | S k => fun h => get q (lt_S_n _ _ h)         end     end.   Implicit Arguments get [n].   Fixpoint append (n: nat) (l: vector n) {struct l}: forall m: nat, vector m -> vector (n+m) :=     match l in vector n return forall m: nat, vector m -> vector (n+m) with     | nnil => fun _ l' => l'     | ncons _ a q => fun _ l => ncons a (append q l)     end.   Fixpoint split1 (n: nat): forall (k: nat) (l: vector (n+k)), vector n :=     match n return forall k (l: vector (n+k)), vector n with     | 0 => fun k l => nnil     | S n => fun k l => ncons (head l) (split1 n k (tail l))     end.   Fixpoint split2 (n: nat): forall (k: nat) (l: vector (n+k)), vector k :=     match n return forall k (l: vector (n+k)), vector k with     | 0 => fun k l => l     | S n => fun k l => split2 n k (tail l)     end.   Fixpoint overwrite (k n: nat) (l: vector k) (l': vector n) {struct l}: vector n :=     match l, l' with     | nnil, l' => l'     | ncons _ _ _, nnil => nnil     | ncons _ a q, ncons _ a' q' => ncons a (overwrite q q')     end.   Fixpoint truncate (k: nat): forall n, vector n -> k<=n -> vector k :=     match k return forall n, vector n -> k<=n -> vector k with     | 0 => fun n l h => nnil     | S k => fun n l =>       match l in vector n return S k<=n -> vector (S k) with       | nnil => fun h => False_rec _ (le_Sn_O _ h)       | ncons _ a q => fun h => ncons a (truncate q (le_S_n _ _ h))       end     end.   Fixpoint rev_init (n: nat) (f: nat -> A) {struct n}: vector n :=     match n return vector n with     | 0 => nnil     | S m => ncons (f n) (rev_init m f)     end.   Definition init (n: nat) (f: nat -> A) := rev_init n (fun m => f (n-m)).   Definition fill(k n: nat) (l: vector k) (a: A) :=     init n (fun i => match le_lt_dec k i with                      | right h => get l i h                      | _ => a                      end).   Fixpoint change (n: nat) (l: vector n) (i: nat) (a: A) {struct l}: vector n :=     match l in vector n, i return vector n with     | nnil, _ => nnil     | ncons _ a' q, 0 => ncons a q     | ncons _ a' q, S i => ncons a' (change q i a)     end.   Lemma empty_nnil: forall l: vector 0, l=nnil.   Lemma nempty_ncons: forall n (l: vector (S n)), exists x, exists q, l=ncons x q.   Theorem head_tail: forall (n: nat) (l: vector (S n)), l = ncons (head l) (tail l).   Theorem vector_eq: forall (n: nat) (l l': vector n),         (forall (i: nat) (h: i<n), get l i h = get l' i h) -> l=l'.   Lemma get_cons: forall (n: nat) (a: A) (l: vector n) (i : nat) (h: i<n),                    get (ncons a l) (S i) (lt_n_S _ _ h) = get l i h.   Lemma head_get: forall (n: nat) (l: vector (S n)), head l = get l 0 (lt_O_Sn n).   Definition eq_from(k n: nat) (l l': vector n): Prop := forall i (h h': i<n), k<=i -> get l i h = get l' i h'.   Definition eq_until(k n: nat) (l l': vector n): Prop := forall i (h h': i<n), i<k -> get l i h = get l' i h'.   Definition eq_between(k k' n: nat) (l l': vector n): Prop := forall i (h h': i<n), k<=i -> i<k' -> get l i h = get l' i h'.   Theorem eq_from_sym: forall k n (l l': vector n), eq_from k l l' -> eq_from k l' l.   Theorem eq_until_sym: forall k n (l l': vector n), eq_until k l l' -> eq_until k l' l.   Theorem eq_between_sym: forall k k' n (l l': vector n), eq_between k k' l l' -> eq_between k k' l' l. End Vector. Implicit Arguments get [A n]. Implicit Arguments truncate [A n]. Lemma get_pirr: forall i n (h h': i<n) A (l: vector A n), get l i h = get l i h'. Hint Immediate get_pirr. Lemma get_pirr': forall i j n (h: i<n) (h': j<n) A (l: vector A n), i=j -> get l i h = get l j h'. Theorem get_tail: forall A (n: nat) (l: vector A (S n)) (i : nat) (h: i<n), get (tail l) i h = get l (S i) (lt_n_S _ _ h). Theorem get_append_1: forall i n (h: i<n) A (l: vector A n) m (l': vector A m) (h': i<n+m),                 get (append l l') i h' = get l i h. Lemma lt_minus: forall i j k (ij: i<=j) (jik: j<i+k), j-i<k. Theorem get_append_2: forall i n (h: i>=n) A (l: vector A n) m (l': vector A m) (h': i<n+m),               get (append l l') i h' = get l' (i-n) (lt_minus m h h'). Theorem get_append_2': forall i m n (h: m+i<m+n) A (l: vector A m) (l': vector A n),               get (append l l') (m+i) h = get l' i (plus_lt_reg_l _ _ _ h). Hint Rewrite get_append_2': vector. Theorem get_split1: forall n k i (h: i<n) A (l: vector A (n+k)), get (split1 n k l) i h = get l i (lt_plus_trans _ _ _ h). Hint Rewrite get_split1: vector. Theorem get_split2: forall n k i (h: i<k) A (l: vector A (n+k)), get (split2 n k l) i h = get l (n+i) (plus_lt_compat_l _ _ _ h). Hint Rewrite get_split2: vector. Theorem split: forall A n k (l: vector A (n+k)), l = append (split1 n k l) (split2 n k l). Hint Immediate split. Theorem split1_append: forall m n A (l: vector A m) (l': vector A n), split1 m n (append l l') = l. Hint Rewrite split1_append: vector. Theorem split2_append: forall m n A (l: vector A m) (l': vector A n), split2 m n (append l l') = l'. Hint Rewrite split2_append: vector. Theorem split_eq: forall m n A (l l': vector A (m+n)), split1 m n l = split1 m n l' -> split2 m n l = split2 m n l' -> l = l'. Ltac split_eq m n := match goal with |- ?l = ?l' => rewrite (split m n l); rewrite (split m n l'); apply split_eq end. Theorem get_overwrite_1: forall i k (h': i<k) n (h: i<n) A (l : vector A k) (l': vector A n), get (overwrite l l') i h = get l i h'. Theorem get_overwrite_2: forall i k (h': k<=i) n (h: i<n) A (l : vector A k) (l': vector A n), get (overwrite l l') i h = get l' i h. Theorem split1_overwrite: forall m n A (l: vector A m) (l': vector A (m+n)), split1 m n (overwrite l l') = l. Hint Rewrite split1_overwrite: vector. Theorem split1_overwrite': forall k m n A (l: vector A k) (l': vector A (m+n)), split1 m n (overwrite l l') = (overwrite l (split1 _ _ l')). Hint Rewrite split1_overwrite: vector. Theorem split2_overwrite: forall m n A (l: vector A m) (l': vector A (m+n)), split2 m n (overwrite l l') = split2 m n l'. Hint Rewrite split2_overwrite: vector. Theorem split2_overwrite': forall k m n A (l: vector A (m+k)) (l': vector A (m+n)), split2 m n (overwrite l l') = (overwrite (split2 m k l) (split2 m n l')). Hint Rewrite split2_overwrite': vector. Theorem overwrite_nothing: forall n A (l: vector A 0) (l': vector A n), overwrite l l' = l'. Hint Rewrite overwrite_nothing: vector. Theorem overwrite_full: forall n A (l l': vector A n), overwrite l l' = l. Hint Rewrite overwrite_full: vector. Theorem overwrite_empty: forall n A (l: vector A n) (l': vector A 0), overwrite l l' = nnil _. Hint Rewrite overwrite_empty: vector. Theorem get_truncate: forall A k i n (l: vector A n) (h: k<=n) (h': i<k), get (truncate k l h) i h' = get l i (lt_le_trans _ _ _ h' h). Hint Rewrite get_truncate: vector. Theorem truncate_id: forall A n (l: vector A n) (h: n<=n), truncate n l h = l. Hint Rewrite truncate_id: vector. Theorem truncate_overwrite_id: forall A k n (l': vector A k) (l: vector A n) (h: k<=n), truncate k (overwrite l' l) h = l'. Hint Rewrite truncate_overwrite_id: vector. Theorem change_append_1: forall A m n (l: vector A m) (l': vector A n) i a, i<m -> change (append l l') i a = append (change l i a) l'. Theorem change_append_2: forall A m n (l: vector A m) (l': vector A n) i a, change (append l l') (m+i) a = append l (change l' i a). Hint Rewrite change_append_2: vector. Theorem get_change_ii: forall i n (h: i<n) A (l: vector A n) a,                          get (change l i a) i h = a. Hint Rewrite get_change_ii: vector. Theorem get_change_ij: forall i j (d: i<>j) A n (h: j<n) (l: vector A n) a,                          get (change l i a) j h = get l j h. Theorem change_ii_invol: forall A i a a' n (l: vector A n),                          change (change l i a') i a = change l i a. Hint Rewrite change_ii_invol: vector. Theorem change_ij_comm: forall i j (d: i<>j) A ai aj n (l: vector A n),                          change (change l i ai) j aj = change (change l j aj) i ai. Theorem change_id: forall i n (h: i<n) A (l: vector A n) a, a=get l i h -> change l i a = l. Theorem change_id': forall i j n (hj: j<n) A (l: vector A n) a, i=j -> a=get l j hj -> change l i a = l. Theorem change_id_out: forall i n A (l: vector A n) a, change l (n+i) a = l. Hint Rewrite change_id_out: vector. Theorem head_change_O: forall A n (l: vector A (S n)) a, head (change l 0 a) = a. Hint Rewrite head_change_O: vector. Theorem head_change_S: forall A n (l: vector A (S n)) i a, head (change l (S i) a) = head l. Hint Rewrite head_change_S: vector. Theorem split1_change: forall m n A (l: vector A (m+n)) i a, split1 m n (change l i a) = change (split1 m n l) i a. Hint Rewrite split1_change: vector. Theorem split1_change': forall m n A (l: vector A (m+n)) i a, split1 m n (change l (m+i) a) = split1 m n l. Hint Rewrite split1_change': vector. Theorem split2_change: forall m n A (l: vector A (m+n)) i a, split2 m n (change l (m+i) a) = change (split2 m n l) i a. Hint Rewrite split2_change: vector. Theorem split2_change': forall m n A (l: vector A (m+n)) i a, i<m -> split2 m n (change l i a) = split2 m n l. Lemma get_rev_init: forall i n (h: i<n) (A: Set) (f: nat -> A),                      get (rev_init n f) i h = f (n-i). Hint Rewrite get_rev_init: vector. Theorem get_init: forall i n (h: i<n) (A: Set) (f: nat -> A),                      get (init n f) i h = f i. Hint Rewrite get_init: vector. Theorem get_fill_1: forall i k (h': i<k) A n (h: i<n) (l: vector A k) a, get (fill n l a) i h = get l i h'. Theorem get_fill_2: forall A i k n (h: i<n) (l: vector A k) a, k<=i -> get (fill n l a) i h = a. Theorem change_fill: forall A i k (h: i<k) n (l: vector A k) a a', change (fill n l a) i a' = fill n (change l i a') a. Theorem append_fill_O: forall A (l l': vector A 0) m n a, append (fill m l a) (fill n l' a) = fill (m+n) (nnil _) a. Hint Rewrite append_fill_O: vector. Theorem split1_fill: forall A k (l: vector A k) m n a, split1 m n (fill (m+n) l a) = fill m l a. Hint Rewrite split1_fill: vector. Theorem split2_fill: forall A k (l: vector A k) m n a, k<=m -> split2 m n (fill (m+n) l a) = fill n (nnil _) a. Theorem fill_overwrite: forall m n (h: m<=n) k A (l: vector A m) (l': vector A n) a, fill k (overwrite l l') a = overwrite l (fill k l' a). Theorem overwrite_invol: forall A m (l: vector A m) n (l': vector A n), overwrite l (overwrite l l') = overwrite l l'. Hint Rewrite overwrite_invol: vector. Theorem change_overwrite_1: forall i k (h: i<k) A n (l: vector A k) (l': vector A n) a, change (overwrite l l') i a = overwrite (change l i a) l'. Theorem overwrite_append_1: forall m k (h: k<=m) A n (l: vector A k) (l1: vector A m) (l2: vector A n), overwrite l (append l1 l2) = append (overwrite l l1) l2. Hint Rewrite overwrite_append_1: vector. Theorem change_overwrite_2: forall i k (h: k<=i) A n (l: vector A k) (l': vector A n) a, change (overwrite l l') i a = overwrite l (change l' i a). Theorem truncate_append: forall A m n (l: vector A m) (l': vector A n) (h: m<=m+n), truncate m (append l l') h = l. Hint Rewrite truncate_append: vector. Theorem truncate_change: forall A n (l: vector A n) i k a (h: k<=n), truncate k (change l i a) h = change (truncate k l h) i a. Hint Rewrite truncate_change: vector. Theorem truncate_overwrite: forall A m (l: vector A m) n (l': vector A n) k (h:k<=n), truncate k (overwrite l l') h = overwrite l (truncate k l' h). Hint Rewrite truncate_overwrite: vector. Theorem truncate_eq_from_eq: forall k m (h: k<=m) A (l l': vector A m), truncate k l h = truncate k l' h -> eq_from k l l' -> l = l'. Theorem eq_from_change: forall k m (h: k<=m) A i (l l': vector A m) a, i<k -> eq_from k l l' -> eq_from k (change l i a) l'. Theorem eq_from_overwrite': forall A m n (l: vector A m) (l': vector A n), eq_from m (overwrite l l') l'. Hint Immediate eq_from_overwrite'. Theorem eq_from_overwrite: forall A m n (l: vector A m) (l1 l2: vector A n), eq_from m l1 l2 -> eq_from m (overwrite l l1) l2. Theorem eq_from_append: forall A m n (l1 l2: vector A m) (l: vector A n), eq_from m (append l1 l) (append l2 l). Hint Immediate eq_from_append. Lemma nki_n: forall i k n, k<=n -> i < k -> n-k+i < n. Definition etruncate k n (l: vector nat n) (h: k<=n): vector nat k :=   init k (fun i => match le_lt_dec k i with left _ => 0 | right h' => get l (n-k+i) (nki_n h h') end). Implicit Arguments etruncate [n]. Theorem get_etruncate: forall k n (l: vector nat n) (h: k<=n) i (h': i<k), get (etruncate k l h) i h' = get l (n-k+i) (nki_n h h'). Hint Rewrite get_etruncate: vector. Theorem etruncate_change: forall n (l: vector nat n) i k a (h: k<=n), etruncate k (change l ((n-k)+i) a) h = change (etruncate k l h) i a. Hint Rewrite etruncate_change: vector. Theorem etruncate_append: forall m n (l: vector nat m) (l': vector nat n) (h: n<=m+n), etruncate n (append l l') h = l'. Hint Rewrite etruncate_append: vector. Theorem etruncate_append_cons: forall m n (l: vector nat m) (l': vector nat n) a (h: n<=m+S n), etruncate n (append l (ncons a l')) h = l'. Hint Rewrite etruncate_append_cons: vector. Theorem etruncate_eq_until_eq: forall k m (h: k<=m) (l l': vector nat m), etruncate k l h = etruncate k l' h -> eq_until (m-k) l l' -> l = l'. Theorem eq_until_change: forall k m (h: k<=m) A i (l l': vector A m) a, k<=i -> eq_until k l l' -> eq_until k (change l i a) l'. Lemma eq_le: forall m n, m=n -> m<=n. Definition coerce m n (h: n=m) (l: vector nat m) := etruncate n l (eq_le h). Implicit Arguments coerce [m]. Theorem get_coerce: forall m n (h: n=m) (l: vector nat m) i (h': i<n), get (coerce n h l) i h' = get l i (lt_le_trans _ _ _ h' (eq_le h)). Hint Rewrite get_coerce: vector. Section Map.   Variables A B: Set.   Variable f: A -> B.   Fixpoint map(n: nat) (l: vector A n) {struct l}: vector B n :=   match l in vector _ n return vector B n with   | nnil => nnil B   | ncons _ a q => ncons (f a) (map q)   end.   Theorem get_map: forall (n: nat) (l: vector A n) (i: nat) (h: i<n), get (map l) i h = f (get l i h).   Hint Rewrite get_map: vector. End Map. Infix "::" := ncons (at level 60, right associativity). Infix "@" := append (at level 61, left associativity). Ltac finite_list l := rewrite (empty_nnil l) || ( rewrite (head_tail l); finite_list (tail l) ). Ltac get_change := rewrite get_change_ii || (rewrite get_change_ij; [ get_change | assumption || auto with arith ]). ```