# Library Matrices.vectors

Global Set Asymmetric Patterns.

Require Export Eqdep.
Require Export Eqdep_dec.
Require Export Peano_dec.
Require Export Omega.

Axiom proof_irr : (A : Prop) (p q : A), p = q.

Lemma two_step_ind :
P : nat Prop,
P 0 P 1 ( n : nat, P n P (S (S n))) n : nat, P n.
intros P h0 h1 hr n; cut (P n P (S n)).
intros H; elim H; trivial.
elim n.
split; trivial.
intros n0 H; try assumption.
elim H.
intros H0 H1; try assumption.
split; [ trivial | apply hr; trivial ].
Qed.

Section vect_def.
Variable A : Set.

Inductive vect : nat Set :=
| vnil : vect 0
| vcons : n : nat, A vect n vect (S n).

Lemma uniq : v : vect 0, v = vnil.
intros v.
change (v = eq_rec _ vect vnil _ (refl_equal 0)) in |- ×.
generalize (refl_equal 0).
change
((fun (n : nat) (v : vect n) ⇒
e : 0 = n, v = eq_rec _ vect vnil _ e) 0 v)
in |- ×.
case v; intros.
apply K_dec_set with (p := e).
exact eq_nat_dec.
reflexivity.
discriminate e.
Qed.

Definition eq_vect := eq_dep nat vect.

Lemma decompose_dep :
n m : nat,
m = S n
v : vect (S n),
{a : A & {v' : vect n | eq_vect (S n) v (S n) (vcons n a v')}}.
intros n m H v.
generalize H; clear H.
dependent inversion_clear v
with
(fun (n' : nat) (vl : vect n') ⇒
m = n' {a : A & {v' : vect n | eq_vect n' vl (S n) (vcons n a v')}}).
unfold eq_vect in |- ×.
intros H; a; v0.
apply eq_dep_intro.
Qed.

Lemma decompose :
(n : nat) (v : vect (S n)),
{a : A & {v' : vect n | v = vcons n a v'}}.
intros n v.
cut {a : A & {t : vect n | eq_vect (S n) v (S n) (vcons n a t)}}.
intros H; elim H; clear H.
intros a H; elim H; clear H.
intros v' H.
a; v'.
apply eq_dep_eq with (U := nat) (P := vect) (p := S n).
unfold eq_vect in H; trivial.
apply (decompose_dep n (S n)); trivial.
Qed.

Lemma eq_vect_vcons :
(c n : nat) (vc : vect c) (vn : vect n) (a a' : A),
a = a'
eq_vect c vc n vn eq_vect (S c) (vcons c a vc) (S n) (vcons n a' vn).
intros c n vc vn a a' H H'.
rewrite H.
cut (eq_vect (S c) (vcons c a' vc) (S c) (vcons c a' vc)).
intros Hcut.
unfold eq_vect in |- ×.
apply
(eq_dep_ind nat vect c vc
(fun (n0 : nat) (v0 : vect n0) ⇒
eq_dep nat vect (S c) (vcons c a' vc) (S n0) (vcons n0 a' v0)) Hcut n vn
H').
unfold eq_vect in |- *; apply eq_dep_intro.
Qed.

Lemma vcons_lemma :
(n : nat) (x y : A) (xs ys : vect n),
x = y xs = ys vcons n x xs = vcons n y ys.
intros n x y xs ys Hxy Hxsys.
rewrite Hxy.
rewrite Hxsys.
trivial.
Qed.

Lemma induc1 :
P : n : nat, vect n Prop,
P 0 vnil
( (n : nat) (v : vect n), P n v a : A, P (S n) (vcons n a v))
(n : nat) (v : vect n), P n v.
intros P Hnil Hvcons n.
elim n.
intros v.
replace v with vnil; [ idtac | rewrite uniq; auto ].
exact Hnil.
intros n0 HR v.
elim (decompose n0 v).
intros ve Hve; elim Hve; intros xe Heq.
rewrite Heq.
apply Hvcons.
apply HR.
Qed.

Lemma induc2 :
P : n : nat, vect n vect n Prop,
P 0 vnil vnil
( (n : nat) (v v' : vect n),
P n v v' a b : A, P (S n) (vcons n a v) (vcons n b v'))
(n : nat) (v v' : vect n), P n v v'.
intros P Hnil Hvcons n.
elim n.
intros v v'.
replace v with vnil; [ idtac | rewrite uniq; auto ].
replace v' with vnil; [ idtac | rewrite uniq; auto ].
exact Hnil.
intros n0 HR v v'.
elim (decompose n0 v).
intros ve Hve; elim Hve; intros xe Heq.
rewrite Heq.
elim (decompose n0 v').
intros ve' Hve'; elim Hve'; intros xe' Heq'.
rewrite Heq'.
apply Hvcons.
apply HR.
Qed.

Lemma induc3 :
P : n : nat, vect n vect n vect n Prop,
P 0 vnil vnil vnil
( (n : nat) (v v' v'' : vect n),
P n v v' v''
a b c : A, P (S n) (vcons n a v) (vcons n b v') (vcons n c v''))
(n : nat) (v v' v'' : vect n), P n v v' v''.
intros P Hvnil Hvcons n.
elim n.
intros v v' v''.
replace v with vnil; [ idtac | rewrite uniq; auto ].
replace v' with vnil; [ idtac | rewrite uniq; auto ].
replace v'' with vnil; [ idtac | rewrite uniq; auto ].
exact Hvnil.
intros n0 HR v v' v''.
elim (decompose n0 v).
intros ve Hve; elim Hve; intros xe Heq.
rewrite Heq.
elim (decompose n0 v').
intros ve' Hve'; elim Hve'; intros xe' Heq'.
rewrite Heq'.
elim (decompose n0 v'').
intros ve'' Hve''; elim Hve''; intros xe'' Heq''.
rewrite Heq''.
apply Hvcons.
apply HR.
Qed.

Definition head (n : nat) (v : vect n) :=
match v in (vect n) return (0 < n A) with
| vnilfun h : 0 < 0 ⇒ False_rec A (lt_irrefl 0 h)
| vcons p a v'fun h : 0 < S pa
end.

v v' : vect 1, v = v' head 1 v (le_n 1) = head 1 v' (le_n 1).
intros v v' H; rewrite H; trivial.
Qed.

Definition tail (n : nat) (v : vect n) :=
match v in (vect m) return (vect (pred m)) with
| vnilvnil
| vcons p a v'v'
end.

Lemma le_S_lt_O : n m : nat, S m n 0 < n.
intros; apply lt_le_trans with (S m); auto with arith.
Qed.

Lemma lt_le_pred : n m : nat, n < m n pred m.
simple induction n; simple induction m; auto with arith.
Qed.

Lemma le_Sn_le_n_pred : n m : nat, S n m n pred m.
intros; apply lt_le_pred; trivial.
Qed.

Theorem zerop : n : nat, {n = 0} + {0 < n}.
destruct n; auto with arith.
Defined.

Fixpoint nth (i : nat) : n : nat, vect n 0 < i i n A :=
fun (n : nat) (v : vect n) ⇒
match i as j return (0 < j j n A) with
| Ofun (h' : 0 < 0) h''False_rec A (lt_irrefl 0 h')
| S p
fun (h' : 0 < S p) (h'' : S p n) ⇒
match zerop p with
| left _head n v (le_S_lt_O _ _ h'')
| right hnth p (pred n) (tail n v) h (le_Sn_le_n_pred _ _ h'')
end
end.

Remark nth_lemma_aux : (i n : nat) (Hi2 : S i S n), i n.
intros; apply le_S_n; trivial.
Qed.

Lemma nth_lemma :
(i n : nat) (a : A) (v : vect n) (Hi1 : 0 < S (S i))
(Hi2 : S (S i) S n) (Hi1' : 0 < S i),
nth (S (S i)) (S n) (vcons n a v) Hi1 Hi2 =
nth (S i) n v Hi1' (le_Sn_le_n_pred (S i) (S n) Hi2).
intros i; elim i using two_step_ind.
intros n a v Hi1 Hi2 Hi1'; simpl in |- *; trivial.
intros i' a v Hi1 Hi2 Hi1'; simpl in |- *; trivial.
intros i' HR n' a v Hi1 Hi2 Hi1'; simpl in |- *; trivial.
Qed.

Lemma nth_lemma' :
(c n : nat) (w : vect n) (a : A) (H1 : 0 < S c)
(H2 : S c S n) (H1' : 0 < c),
nth (S c) (S n) (vcons n a w) H1 H2 =
nth c n w H1' (le_Sn_le_n_pred c (S n) H2).
intros c; elim c.
intros n w a H1 H2 H1'; inversion H1'.
intros c' HR.
simpl in |- *; trivial.
Qed.

Lemma last_o1 : n c' : nat, S c' n 0 < n - c'.
intros; omega.
Qed.

Lemma last_o2 : n c' : nat, n - c' n.
intros; omega.
Qed.

Lemma last_o3 : c' : nat, 0 c'.
intros; omega.
Qed.

Lemma last_o4 : c' n : nat, S c' n c' n.
intros; omega.
Qed.

Definition last :
(n : nat) (v : vect n) (c : nat), 0 c c n vect c.
intros n v; fix 1.
intros c; case c.
intros; apply vnil.
intros c' Hc1' Hc2'.
apply vcons.
apply (nth (n - c') n v).
apply last_o1; assumption.
apply last_o2; assumption.
apply last.
apply last_o3; assumption.
apply last_o4; assumption.
Defined.

Lemma last_vcons :
(n : nat) (w : vect n) (c : nat) (H1 : 0 < n - c)
(H2 : n - c n) (H1c' : 0 S c) (H2c' : S c n)
(H1c : 0 c) (H2c : c n),
vcons c (nth (n - c) n w H1 H2) (last n w c H1c H2c) =
last n w (S c) H1c' H2c'.
intros n w c H1 H2 H1c' H2c' H1c H2c.
unfold last at 2 in |- ×.
apply vcons_lemma.
rewrite (proof_irr _ H1 (last_o1 n c H2c')).
rewrite (proof_irr _ H2 (last_o2 n c)).
trivial.
rewrite (proof_irr _ H1c (last_o3 c)).
rewrite (proof_irr _ H2c (last_o4 c n H2c')).
trivial.
Qed.

Lemma last_S :
(c n : nat) (a : A) (v : vect n) (H1 : 0 c)
(H2 : c n) (H2' : c S n),
last n v c H1 H2 = last (S n) (vcons n a v) c H1 H2'.
intros c; elim c.
intros n a v H1 H2 H2'; try assumption.
rewrite (uniq (last n v 0 H1 H2)).
rewrite (uniq (last (S n) (vcons n a v) 0 H1 H2')); trivial.
intros c' HR.
intros n a v H1 H2 H2'.
unfold last in |- ×.
apply vcons_lemma.
generalize (last_o1 (S n) c' H2') (last_o2 (S n) c').
rewrite <- minus_Sn_m.
intros Hcut1 Hcut2.
symmetry in |- ×.
rewrite (nth_lemma' (n - c') n v a Hcut1 Hcut2 (last_o1 n c' H2)).
rewrite (proof_irr _ (le_Sn_le_n_pred (n - c') (S n) Hcut2) (last_o2 n c')).
trivial.
replace
(fix last (c0 : nat) : 0 c0 c0 n vect c0 :=
match c0 as c1 return (0 c1 c1 n vect c1) with
| Ofun (_ : 0 0) (_ : 0 n) ⇒ vnil
| S c'0
fun (_ : 0 S c'0) (Hc2' : S c'0 n) ⇒
vcons c'0 (nth (n - c'0) n v (last_o1 n c'0 Hc2') (last_o2 n c'0))
(last c'0 (last_o3 c'0) (last_o4 c'0 n Hc2'))
end) with (last n v); [ idtac | trivial ].
replace
(fix last (c0 : nat) : 0 c0 c0 S n vect c0 :=
match c0 as c1 return (0 c1 c1 S n vect c1) with
| Ofun (_ : 0 0) (_ : 0 S n) ⇒ vnil
| S c'0
fun (_ : 0 S c'0) (Hc2' : S c'0 S n) ⇒
vcons c'0
(nth (S n - c'0) (S n) (vcons n a v) (last_o1 (S n) c'0 Hc2')
(last_o2 (S n) c'0))
(last c'0 (last_o3 c'0) (last_o4 c'0 (S n) Hc2'))
end) with (last (S n) (vcons n a v)); [ idtac | trivial ].
omega.
apply (HR n a v (last_o3 c') (last_o4 c' n H2) (last_o4 c' (S n) H2')).
Qed.

Lemma last_vcons' :
(n : nat) (w : vect n) (c : nat) (a : A) (H1 : 0 < n - c)
(H2 : n - c n) (H1c' : 0 S c) (H2c' : S c S n)
(H1c : 0 c) (H2c : c n),
vcons c (nth (n - c) n w H1 H2) (last n w c H1c H2c) =
last (S n) (vcons n a w) (S c) H1c' H2c'.
intros n; elim n.
intros w c a H1 H2 H1c' H2c' H1c H2c; cut (c = 0).
intros Hrew; generalize w a H1 H2 H1c' H2c' H1c H2c;
clear w a H1 H2 H1c' H2c' H1c H2c.
rewrite Hrew.
intros w a H1; simpl in H1; inversion H1.
omega.
intros n0 HR v c.
intros a H1 H2 H1c' H2c' H1c H2c.
cut (c n0).
intros Hcut; generalize a H1 H2 H1c' H2c' H1c H2c;
clear a H1 H2 H1c' H2c' H1c H2c.
rewrite <- (minus_Sn_m _ _ Hcut).
2: omega.
intros a H1 H2 H1c' H2c' H1c H2c.
unfold last at 2 in |- ×.
apply vcons_lemma.
generalize (last_o1 (S (S n0)) c H2c') (last_o2 (S (S n0)) c).
replace (S (S n0) - c) with (S (S (n0 - c))); [ idtac | omega ].
intros Hcut1 Hcut2.
symmetry in |- ×.
rewrite (nth_lemma' (S (n0 - c)) (S n0) v a Hcut1 Hcut2 H1).
rewrite (proof_irr _ H2 (le_Sn_le_n_pred (S (n0 - c)) (S (S n0)) Hcut2)).
trivial.
replace
(fix last (c : nat) : 0 c c S (S n0) vect c :=
match c as c1 return (0 c1 c1 S (S n0) vect c1) with
| Ofun (_ : 0 0) (_ : 0 S (S n0)) ⇒ vnil
| S c'
fun (_ : 0 S c') (Hc2' : S c' S (S n0)) ⇒
vcons c'
(nth (S (S n0) - c') (S (S n0)) (vcons (S n0) a v)
(last_o1 (S (S n0)) c' Hc2') (last_o2 (S (S n0)) c'))
(last c' (last_o3 c') (last_o4 c' (S (S n0)) Hc2'))
end) with (last (S (S n0)) (vcons (S n0) a v));
[ idtac | trivial ].
generalize (last_S c (S n0) a v H1c H2c (last_o4 c (S (S n0)) H2c')).
rewrite (proof_irr _ H1c (last_o3 c)).
trivial.
Qed.

Lemma last_n :
(c n : nat) (v : vect n) (H : c = n) (H1 : 0 c) (H2 : c n),
eq_vect c (last n v c H1 H2) n v.
intros c; elim c.
intros n v H; simpl in |- ×.
intros H1 H2.
generalize H v; case n.
intros; rewrite uniq.
unfold eq_vect in |- *; apply eq_dep_intro.
intros n' Hd; discriminate Hd.
intros c' HR n; case n.
intros v Hd; discriminate Hd.
intros n' v' Heq H1 H2.
cut (0 < S n' - c'); [ intros Hcut1 | omega ].
cut (S n' - c' S n'); [ intros Hcut2 | omega ].
cut (0 S c'); [ intros Hcut3 | omega ].
cut (S c' S n'); [ intros Hcut4 | omega ].
cut (0 c'); [ intros Hcut5 | omega ].
cut (c' S n'); [ intros Hcut6 | omega ].
elim (decompose _ v').
intros x0 Hx; elim Hx; clear Hx; intros v0 Heq'.
rewrite Heq'.
rewrite <-
(last_vcons (S n') (vcons n' x0 v0) c' Hcut1 Hcut2 H1 H2 Hcut5 Hcut6)
.
apply
(eq_vect_vcons c' n' (last (S n') (vcons n' x0 v0) c' Hcut5 Hcut6) v0
(nth (S n' - c') (S n') (vcons n' x0 v0) Hcut1 Hcut2) x0).
cut (S n' - c' = 1); [ intros Hcut'' | omega ].
generalize Hcut1 Hcut2; rewrite Hcut''.
simpl in |- *; trivial.
rewrite <- (last_S c' n' x0 v0 Hcut5 (le_S_n _ _ Hcut4) Hcut6).
apply HR.
omega.
Qed.

Lemma last_n' :
(n : nat) (v : vect n) (H1 : 0 n) (H2 : n n),
last n v n H1 H2 = v.
intros; apply (eq_dep_eq nat vect n (last n v n H1 H2) v).
apply last_n.
trivial.
Qed.

End vect_def.

Fixpoint map (A B : Set) (f : A B) (n : nat) (v : vect A n) {struct v} :
vect B n :=
match v in (vect _ p) return (vect B p) with
| vnilvnil B
| vcons p x v'vcons B p (f x) (map A B f p v')
end.

Lemma map_2 :
(A B : Set) (n : nat) (t : vect A n) (f : A B)
(g : B A) (H : x : A, g (f x) = x),
map B A g n (map A B f n t) = map A A (fun x : Ag (f x)) n t.
intros A2 B n; elim n.
intros t f g H; rewrite (uniq A2).
rewrite (uniq B (map A2 B f 0 t)).
simpl in |- *; trivial.
intros n0 H t f g H0; try assumption.
elim (decompose A2 n0 t).
intros x Hx; elim Hx; intros v Hvx; rewrite Hvx; clear Hx Hvx.
simpl in |- ×.
rewrite H.
trivial.
apply H0.
Qed.

Lemma map_2' :
(A B : Set) (n : nat) (t : vect A n) (f : A B)
(g : B A) (H : x : A, g (f x) = x),
map B A g n (map A B f n t) = t.
intros A2 B n; elim n.
intros t f g H; rewrite (uniq A2).
rewrite (uniq B (map A2 B f 0 t)).
simpl in |- *; trivial.
intros n0 H t f g H0; try assumption.
elim (decompose A2 n0 t).
intros x Hx; elim Hx; intros v Hvx; rewrite Hvx; clear Hx Hvx.
simpl in |- ×.
rewrite H.
rewrite H0; trivial.
apply H0.
Qed.