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 ]).