Set Implicit Arguments.

Require Import Program.
Require Import LogicUtil.
Require Vector.
Require Import NatUtil.
Require Import EqUtil.
Require Import RelMidex.
Require Import ListUtil.
Require Import BoolUtil.

Implicit Arguments Vector.nil [A].
Implicit Arguments Vector.cons.
Implicit Arguments Vector.hd.
Implicit Arguments Vector.tl.
Implicit Arguments Vector.const.

Require Export ListUtil.

Implicit Arguments refl_equal [A].

Ltac Veqtac := repeat
  match goal with
    | H : Vector.cons ?x ?v = Vector.cons ?x ?w |- _ ⇒
      let h := fresh in
      (injection H; intro h; ded (inj_pairT2 eq_nat_dec h);
        clear h; clear H)
    | H : Vector.cons ?x ?v = Vector.cons ?y ?w |- _ ⇒
      let h1 := fresh in let h2 := fresh in
      (injection H; intros h1 h2; ded (inj_pairT2 eq_nat_dec h1);
        clear h1; clear H)
  end.

Section S.

Variable A : Type.

Notation vec := (Vector.t A).

Definition Vid n : vec n → vec n :=
  match n with
    | O ⇒ fun _ ⇒ Vector.nil
    | _ ⇒ fun v ⇒ Vector.cons (Vector.hd v) (Vector.tl v)
  end.

Lemma Vid_eq : ∀ n (v : vec n), v = Vid v.

Proof.
destruct v; auto.
Defined.

Lemma VSn_eq: ∀ n (v : vec (S n)), v = Vector.cons (Vector.hd v) (Vector.tl v).

Proof.
intros. change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid v).
apply Vid_eq.
Defined.

Ltac VSntac y :=
  match type of y with
    | Vector.t _ (S _) ⇒ let H := fresh in
      (assert (H : y = Vector.cons (Vector.hd y) (Vector.tl y));
        [apply VSn_eq | rewrite H])
  end.

Lemma Vcons_eq : ∀ a1 a2 n (v1 v2 : vec n),
  a1 = a2 → v1 = v2 → Vector.cons a1 v1 = Vector.cons a2 v2.

Proof.
intros. subst a1. subst v1. reflx.
Qed.

Lemma Vtail_eq : ∀ a n (v1 v2 : vec n), v1 = v2 →
  Vector.cons a v1 = Vector.cons a v2.

Proof.
intros. apply Vcons_eq. reflx. assumption.
Qed.

Program Fixpoint Vcast m (v : vec m) n (mn : m = n) {struct v} : vec n :=
  match v with
  | Vector.nil ⇒
      match n with
      | 0 ⇒ Vector.nil
      | _ ⇒ !
      end
  | Vector.cons x m' v' ⇒
      match n with
      | 0 ⇒ !
      | S n' ⇒ Vector.cons x (Vcast v' _)
      end
  end.

Lemma Vcast_refl_eq : ∀ n (v : vec n) (H : n=n), Vcast v H = v.

Proof.
induction v; simpl; intros. reflx.
match goal with
| |- Vector.cons h ?v' = _ ⇒ assert (E : v' = v)
end.
apply IHv.
simpl in E. rewrite E. reflx.
Defined.

Lemma Vcast_refl : ∀ n (v : vec n), Vcast v (refl_equal n) = v.

Proof.
intros. apply Vcast_refl_eq.
Defined.

Lemma Vcast_eq_elim : ∀ n (v1 v2 : vec n) m (h : n = m),
  Vcast v1 h = Vcast v2 h → v1 = v2.

Proof.
intros until v1. destruct v1; intros; destruct m.
simpl in H. rewrite <- (Vcast_refl_eq v2 h). assumption.
discriminate. discriminate.
assert (n = m). apply eq_add_S. assumption. subst n.
assert (h0 = refl_equal (S m)). apply (UIP eq_nat_dec). subst h0.
simpl in H. do 2 rewrite Vcast_refl_eq in H. assumption.
Qed.

Lemma Vcast_cast_eq :
  ∀ n (v : vec n) m (h1 : n=m) p (h2 : m=p) (h3 : n=p),
  Vcast (Vcast v h1) h2 = Vcast v h3.

Proof.
induction v; intro m; case m; intros until p; case p; simpl; intros;
  (discriminate || auto).
apply Vtail_eq. apply IHv.
Qed.

Lemma Vcast_cast : ∀ n (v : vec n) m (h1 : n=m) p (h2 : m=p),
  Vcast (Vcast v h1) h2 = Vcast v (trans_eq h1 h2).

Proof.
intros. apply Vcast_cast_eq.
Qed.

Lemma Vcast_eq_intror : ∀ n1 (v1 : vec n1) n0 (h1 : n1=n0)
  n2 (v2 : vec n2) (h2 : n2=n0) (h : n1=n2),
  Vcast v1 h = v2 → Vcast v1 h1 = Vcast v2 h2.

Proof.
induction v1; intros until n0; case n0; intros until v2; case v2; simpl;
  intros; (discriminate || auto). Veqtac. subst h. apply Vtail_eq.
eapply IHv1. apply H2.
Qed.

Lemma Vcast_eq : ∀ n (v1 v2 : vec n) p (e : n=p),
  v1 = v2 → Vcast v1 e = Vcast v2 e.

Proof.
induction v1; intros. subst v2. reflx. rewrite H. reflx.
Qed.

Lemma Vcast_prf_eq : ∀ n (v : vec n) p (h1 : n=p) (h2 : n=p),
  Vcast v h1 = Vcast v h2.

Proof.
induction v; intros until p; case p; intros; simpl; (discriminate || auto).
apply Vtail_eq. apply IHv.
Qed.

Lemma Vcast_lr : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) (h12 : n1=n2)
  (h21 : n2=n1), Vcast v1 h12 = v2 → v1 = Vcast v2 h21.

Proof.
induction v1; induction v2; simpl; intros. reflx. discriminate. discriminate.
Veqtac. subst h. apply Vtail_eq. eapply IHv1. apply H2.
Qed.

Lemma Vcast_rl : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) (h12 : n1=n2)
  (h21 : n2=n1), v1 = Vcast v2 h21 → Vcast v1 h12 = v2.

Proof.
induction v1; induction v2; simpl; intros. reflx. discriminate. discriminate.
Veqtac. subst h. apply Vtail_eq. eapply IHv1. apply H2.
Qed.

Lemma Vcast_introrl : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) (h21 : n2=n1),
  Vcast v1 (sym_eq h21) = v2 → v1 = Vcast v2 h21.

Proof.
intros. eapply Vcast_lr. apply H.
Qed.

Lemma Vcast_elimlr : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) (h12 : n1=n2),
  Vcast v1 h12 = v2 → v1 = Vcast v2 (sym_eq h12).

Proof.
intros. eapply Vcast_lr. apply H.
Qed.

Lemma VO_eq : ∀ v : vec O, v = Vector.nil.

Proof.
cut (∀ n (v : vec n) (h: n=0), Vcast v h = Vector.nil).
intros. ded (H 0 v (refl_equal 0)). rewrite Vcast_refl in H0. assumption.
destruct v. auto. intro. discriminate.
Defined.

Ltac VOtac := repeat
  match goal with
    | v : Vector.t _ O |- _ ⇒ assert (v = Vector.nil); [apply VO_eq | subst v]
  end.

Fixpoint Vadd n (v : vec n) (x : A) : vec (S n) :=
  match v with
  | Vector.nil ⇒ Vector.cons x Vector.nil
  | Vector.cons a _ v' ⇒ Vector.cons a (Vadd v' x)
  end.

Program Fixpoint Vnth n (v : Vector.t A n) : ∀ i, i < n → A :=
  match v with
  | Vector.nil ⇒
      fun i ip ⇒ !
  | Vector.cons x p v' ⇒
      fun i ⇒
        match i with
        | 0 ⇒ fun _ ⇒ x
        | S j ⇒ fun H ⇒ Vnth v' (i:=j) _
        end
  end.
Solve Obligations with program_simplify; auto with ×.

Lemma Vhead_nth : ∀ n (v : vec (S n)), Vector.hd v = Vnth v (lt_O_Sn n).

Proof.
intros. VSntac v. reflx.
Qed.

Require Omega.

Lemma Vnth_eq : ∀ n (v : vec n) i1 (h1 : i1<n) i2 (h2 : i2<n),
  i1 = i2 → Vnth v h1 = Vnth v h2.

Proof.
induction v; intro; case i1.
intro. absurd (0 ≤ 0); omega.
intros n h1. absurd (0 ≤ S n); omega.
intros. subst i2. reflx.
intros. subst i2. simpl. apply IHv. reflx.
Qed.

Lemma Vnth_tail : ∀ n (v : vec (S n)) i (h : i < n),
  Vnth (Vector.tl v) h = Vnth v (lt_n_S h).

Proof.
intros. VSntac v. simpl. apply Vnth_eq. reflx.
Qed.

Lemma Vnth_cons : ∀ k n (v : vec n) a (H1 : S k < S n) (H2 : k < n),
  Vnth (Vector.cons a v) H1 = Vnth v H2.

Proof.
intros. simpl. assert (H : lt_S_n H1 = H2). apply lt_unique.
rewrite H. reflx.
Qed.

Lemma Veq_nth : ∀ n (v v' : vec n),
  (∀ i (ip : i < n), Vnth v ip = Vnth v' ip) → v = v'.

Proof.
induction n; intros.
VOtac. reflx.
VSntac v. VSntac v'. apply Vcons_eq.
do 2 rewrite Vhead_nth. apply H.
apply IHn. intros. do 2 rewrite Vnth_tail. apply H.
Qed.

Lemma Vnth_head : ∀ x n (v : vec n) k (h : k < S n),
  k = 0 → Vnth (Vector.cons x v) h = x.

Proof.
intros. subst k. reflx.
Qed.

Lemma Vnth_addl : ∀ k n (v : vec n) a (H1 : k < S n) (H2 : k < n),
  Vnth (Vadd v a) H1 = Vnth v H2.

Proof.
intros. assert (H3 : H1 = (@le_S (S k) n H2)). apply lt_unique.
subst H1. generalize dependent k. generalize dependent n. intro n. elim n.
 intros v k H. elimtype False. apply (lt_n_O _ H).
 intros n' Hrec v k H. rewrite (VSn_eq v). destruct k.
  simpl. reflx.
  simpl Vadd.
  assert (H' : k < S n'). auto with arith.
  rewrite (Vnth_cons (Vadd (Vector.tl v) a) (Vector.hd v) (le_S H) H').
  assert (H'' : k < n'). auto with arith.
  rewrite (Vnth_cons (Vector.tl v) (Vector.hd v) H H'').
  generalize (Hrec (Vector.tl v) k H''). intro H0.
  assert (H1 : H' = le_S H''). apply lt_unique. rewrite H1. clear H1.
  assumption.
Qed.

Lemma Vnth_addr : ∀ k n (v : vec n) a (H1 : k < S n) (H2 : k = n),
  Vnth (Vadd v a) H1 = a.

Proof.
intros. subst k. assert (H2 : H1 = lt_n_Sn n). apply lt_unique. subst H1.
generalize dependent v. intro v. elim v.
simpl. reflx.
intros a' p' v' Hrec. simpl Vadd.
rewrite (Vnth_cons (Vadd v' a) a' (lt_n_Sn (S p')) (lt_n_Sn p')).
assumption.
Qed.

Lemma Vnth_const : ∀ n (a : A) i (ip : i < n), Vnth (Vector.const a n) ip = a.

Proof.
induction n; intros. absurd_arith.
destruct i. trivial.
simpl. rewrite IHn. reflx.
Qed.

Program Fixpoint Vreplace n (v : vec n) i (ip : i < n) (a : A) : vec n :=
  match v with
  | Vector.nil ⇒ !
  | Vector.cons h _ v' ⇒
      match i with
      | 0 ⇒ Vector.cons a v'
      | S i' ⇒ Vector.cons h (Vreplace v' (i:=i') _ a)
      end
  end.
Solve Obligations with program_simplify ; auto with ×.

Lemma Vreplace_tail : ∀ n i (ip : S i < S n) (v : vec (S n)) (a : A),
  Vreplace v ip a = Vector.cons (Vector.hd v) (Vreplace (Vector.tl v) (lt_S_n ip) a).

Proof.
destruct n; intros. absurd_arith.
VSntac v. reflx.
Qed.

Lemma Vnth_Vreplace_replaced : ∀ n i (ip : i < n) (v : vec n) (a : A),
  Vnth (Vreplace v ip a) ip = a.

Proof.
induction n; intros.
elimtype False. omega.
VSntac v. destruct i. trivial.
simpl. apply IHn.
Qed.

Lemma Vnth_Vreplace_notReplaced : ∀ n i (ip : i < n) j (jp : j < n)
  (v : vec n) (a : A), i ≠ j →
  Vnth (Vreplace v ip a) jp = Vnth v jp.

Proof.
induction n; intros.
elimtype False. omega.
VSntac v. destruct i; destruct j; trivial.
elimtype False. omega.
simpl. rewrite IHn. trivial. omega.
Qed.

Fixpoint Vapp n1 n2 (v1 : vec n1) (v2 : vec n2) {struct v1} : vec (n1+n2) :=
  match v1 with
  | Vector.nil ⇒ v2
  | Vector.cons a _ v' ⇒ Vector.cons a (Vapp v' v2)
  end.

Lemma Vapp_cons : ∀ a n1 n2 (v1 : vec n1) (v2 : vec n2),
  Vapp (Vector.cons a v1) v2 = Vector.cons a (Vapp v1 v2).

Proof.
intros. simpl. reflx.
Qed.

Lemma Vapp_nil_eq : ∀ n (v : vec n) (w : vec 0) (h : n=n+0),
  Vapp v w = Vcast v h.

Proof.
induction v; intros. VOtac. reflx.
simpl. apply Vtail_eq. apply IHv.
Qed.

Lemma Vapp_nil : ∀ n (v : vec n) (w : vec 0),
  Vapp v w = Vcast v (plus_n_O n).

Proof.
intros. apply Vapp_nil_eq.
Qed.

Lemma Vapp_rcast_eq : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) p2 (h1 : n2=p2)
  (h2 : n1+n2=n1+p2), Vapp v1 (Vcast v2 h1) = Vcast (Vapp v1 v2) h2.

Proof.
induction v1; simpl; intros.
assert (h1=h2). apply (UIP eq_nat_dec). rewrite H. reflx.
apply Vtail_eq. apply IHv1.
Qed.

Lemma Vapp_rcast : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) p2 (h1 : n2=p2),
  Vapp v1 (Vcast v2 h1) = Vcast (Vapp v1 v2) (plus_reg_l_inv n1 h1).

Proof.
intros. apply Vapp_rcast_eq.
Qed.

Lemma Vapp_lcast_eq : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) p1 (h1 : n1=p1)
  (h2 : n1+n2=p1+n2), Vapp (Vcast v1 h1) v2 = Vcast (Vapp v1 v2) h2.

Proof.
induction v1; intros until p1; case p1; simpl; intros.
rewrite Vcast_refl_eq. reflx. discriminate. discriminate.
apply Vtail_eq. apply IHv1.
Qed.

Lemma Vapp_lcast : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) p1 (h1 : n1=p1),
  Vapp (Vcast v1 h1) v2 = Vcast (Vapp v1 v2) (plus_reg_r_inv n2 h1).

Proof.
intros. apply Vapp_lcast_eq.
Qed.

Lemma Vapp_assoc_eq : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) n3 (v3 : vec n3)
  (h : n1+(n2+n3) = (n1+n2)+n3),
  Vapp (Vapp v1 v2) v3 = Vcast (Vapp v1 (Vapp v2 v3)) h.

Proof.
induction v1; intros; simpl.
rewrite Vcast_refl_eq. reflx.
apply Vtail_eq. apply IHv1.
Qed.

Lemma Vapp_assoc : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2) n3 (v3 : vec n3),
  Vapp (Vapp v1 v2) v3 = Vcast (Vapp v1 (Vapp v2 v3)) (plus_assoc n1 n2 n3).

Proof.
intros. apply Vapp_assoc_eq.
Qed.

Lemma Vapp_eq : ∀ n1 (v1 v1' : vec n1) n2 (v2 v2' : vec n2),
  v1 = v1' → v2 = v2' → Vapp v1 v2 = Vapp v1' v2'.

Proof.
intros. rewrite H. rewrite H0. reflx.
Qed.

Definition Vsplit n (v : vec (S n)) := (Vector.hd v, Vector.tl v).

Fixpoint Vbreak n1 n2 {struct n1} : vec (n1+n2) → vec n1 × vec n2 :=
  match n1 with
  | O ⇒ fun v ⇒ (Vector.nil, v)
  | S p1 ⇒ fun v ⇒
      let w := Vbreak p1 n2 (Vector.tl v) in
        (Vector.cons (Vector.hd v) (fst w), snd w)
  end.

Implicit Arguments Vbreak [n1 n2].

Lemma Vbreak_app : ∀ n1 (v1 : vec n1) n2 (v2 : vec n2),
  Vbreak (Vapp v1 v2) = (v1, v2).

Proof.
induction n1; simpl; intros. VOtac. reflx. VSntac v1. simpl.
generalize (IHn1 (Vector.tl v1) n2 v2). intro. rewrite H0. reflx.
Qed.

Lemma Vbreak_eq_app : ∀ n1 n2 (v : vec (n1+n2)),
  v = Vapp (fst (Vbreak v)) (snd (Vbreak v)).

Proof.
intros n1 n2. elim n1.
 auto.
 clear n1. intros n1 Hrec. simpl.
 intro v.
 transitivity (Vector.cons (Vector.hd v) (Vector.tl v)).
apply VSn_eq. f_equal. exact (Hrec (Vector.tl v)).
Qed.

Lemma Vbreak_eq_app_cast : ∀ n n1 n2 (H : n1+n2=n) (v : vec n),
  v = Vcast (Vapp (fst (Vbreak (Vcast v (sym_equal H))))
    (snd (Vbreak (Vcast v (sym_equal H))))) H.

Proof.
intros until H. case H. simpl. intro v.
rewrite <- Vbreak_eq_app. do 2 rewrite Vcast_refl_eq. reflx.
Qed.

Fixpoint Vin (x : A) n (v : vec n) {struct v} : Prop :=
  match v with
  | Vector.nil ⇒ False
  | Vector.cons y _ w ⇒ x = y ∨ Vin x w
  end.

Lemma Vin_head : ∀ n (v : vec (S n)), Vin (Vector.hd v) v.

Proof.
intros. VSntac v. simpl. auto.
Qed.

Lemma Vin_tail : ∀ n x (v : vec (S n)), Vin x (Vector.tl v) → Vin x v.

Proof.
  intros. VSntac v. simpl. auto.
Qed.

Lemma Vnth_in : ∀ n (v : vec n) k (h : k<n), Vin (Vnth v h) v.

Proof.
induction v. intros. absurd (k<0); omega.
intro. destruct k; simpl. auto. intro. right. apply IHv.
Qed.

Lemma Vin_nth : ∀ n (v : vec n) a, Vin a v →
  ∃ i, ∃ ip : i < n, Vnth v ip = a.

Proof.
  induction n; intros.
  VOtac. destruct H.
  VSntac v. rewrite H0 in H. destruct H.
  ∃ 0. ∃ (lt_O_Sn n). simpl. congruence.
  destruct (IHn (Vector.tl v) a H) as [j [jp v_j]].
  ∃ (S j). ∃ (lt_n_S jp). simpl.
  rewrite lt_Sn_nS. assumption.
Qed.

Lemma Vin_cast_intro : ∀ m n (H : m=n) (v : vec m) x,
  Vin x v → Vin x (Vcast v H).

Proof.
intros m n H. case H. intros. rewrite Vcast_refl. assumption.
Qed.

Lemma Vin_cast_elim : ∀ m n (H : m=n) (v : vec m) x,
  Vin x (Vcast v H) → Vin x v.

Proof.
intros m n H. case H. intros v x. rewrite Vcast_refl. auto.
Qed.

Implicit Arguments Vin_cast_elim [m n H v x].

Lemma Vin_appl : ∀ x n1 (v1 : vec n1) n2 (v2 : vec n2),
  Vin x v1 → Vin x (Vapp v1 v2).

Proof.
induction v1; simpl; intros. contradiction. destruct H. auto.
right. apply IHv1. assumption.
Qed.

Lemma Vin_appr : ∀ x n1 (v1 : vec n1) n2 (v2 : vec n2),
  Vin x v2 → Vin x (Vapp v1 v2).

Proof.
induction v1; simpl; intros. assumption. right. apply IHv1. assumption.
Qed.

Lemma Vin_app_cons : ∀ x n1 (v1 : vec n1) n2 (v2 : vec n2),
  Vin x (Vapp v1 (Vector.cons x v2)).

Proof.
induction v1; intros; simpl; auto.
Qed.

Lemma Vin_app : ∀ x n1 (v1 : vec n1) n2 (v2 : vec n2),
  Vin x (Vapp v1 v2) → Vin x v1 ∨ Vin x v2.

Proof.
induction v1; intros; simpl in × . auto. destruct H. auto.
assert (Vin x v1 ∨ Vin x v2). apply IHv1. exact H. destruct H0; auto.
Qed.

Lemma Vin_elim : ∀ x n (v : vec n),
  Vin x v → ∃ n1, ∃ v1 : vec n1, ∃ n2, ∃ v2 : vec n2,
    ∃ H : n1 + S n2 = n, v = Vcast (Vapp v1 (Vector.cons x v2)) H.

Proof.
induction v; simpl. contradiction.
intro H. destruct H. clear IHv. subst x.
∃ 0. ∃ (@Vector.nil A). ∃ n. ∃ v. ∃ (refl_equal (S n)).
rewrite Vcast_refl. reflx.
assert (∃ n1, ∃ v1 : vec n1, ∃ n2, ∃ v2 : vec n2,
  ∃ H : n1 + S n2 = n, v = Vcast (Vapp v1 (Vector.cons x v2)) H). exact (IHv H).
destruct H0 as [n1]. destruct H0 as [v1]. destruct H0 as [n2].
destruct H0 as [v2].
destruct H0 as [H1].
∃ (S n1). ∃ (Vector.cons h v1). ∃ n2. ∃ v2. ∃ (S_add_S H1).
rewrite H0. clear H0. simpl.
apply Vtail_eq. apply Vcast_prf_eq.
Qed.

Fixpoint Vforall (P : A→Prop) n (v : vec n) { struct v } : Prop :=
  match v with
  | Vector.nil ⇒ True
  | Vector.cons a _ w ⇒ P a ∧ Vforall P w
  end.

Lemma Vforall_intro : ∀ (P : A→Prop) n (v : vec n),
  (∀ x, Vin x v → P x) → Vforall P v.

Proof.
induction v; simpl; intros. exact I. split.
apply H. left. reflx. apply IHv. intros. apply H. right. assumption.
Qed.

Lemma Vforall_nth_intro : ∀ (P : A → Prop) n (v : vec n),
  (∀ i (ip : i < n), P (Vnth v ip)) → Vforall P v.

Proof.
  intros. apply Vforall_intro. intros.
  destruct (Vin_nth v x H0) as [i [ip v_i]].
  rewrite <- v_i. apply H.
Qed.

Lemma Vforall_in : ∀ P x n (v : vec n), Vforall P v → Vin x v → P x.

Proof.
induction v; simpl.
contradiction.
intros Ha Hv. destruct Ha. destruct Hv.
rewrite H1. exact H.
auto.
Qed.

Lemma Vforall_nth : ∀ P n (v : vec n) i (ip : i < n),
  Vforall P v → P (Vnth v ip).

Proof.
  intros. apply Vforall_in with n v. assumption. apply Vnth_in.
Qed.

Lemma Vforall_incl : ∀ (P : A→Prop) n1 (v1 : vec n1) n2 (v2 : vec n2),
  (∀ x, Vin x v1 → Vin x v2) → Vforall P v2 → Vforall P v1.

Proof.
intros. apply Vforall_intro. intros. apply Vforall_in with (v := v2).
assumption. apply H. assumption.
Qed.

Lemma Vforall_cast : ∀ P n v p (h : n=p),
  Vforall P v → Vforall P (Vcast v h).

Proof.
intros. apply Vforall_intro. intros.
eapply Vforall_in with (n := n). apply H. ded (Vin_cast_elim H0). assumption.
Qed.

Lemma Vforall_imp : ∀ (P Q : A→Prop) n (v : vec n),
  Vforall P v → (∀ x, Vin x v → P x → Q x) → Vforall Q v.

Proof.
intros. apply Vforall_intro. intros. apply H0. assumption.
eapply Vforall_in with (n := n). apply H. apply H1.
Qed.

Lemma Vforall_dec : ∀ (P : A → Prop) (P_dec : ∀ x, {P x}+{¬P x}) n,
  ∀ v : vec n, {Vforall P v}+{¬Vforall P v}.

Proof.
  induction n; intros.
  VOtac. left. constructor.
  VSntac v. destruct (P_dec (Vector.hd v)).
  destruct (IHn (Vector.tl v)).
  left. simpl. split; assumption.
  right. intro V. destruct V. contradiction.
  right. intro V. destruct V. contradiction.
Defined.

Fixpoint Vsig_of_v (P : A→Prop) n (v : vec n) {struct v}
  : Vforall P v → Vector.t (sig P) n :=
  match v in Vector.t _ n return Vforall P v → Vector.t (sig P) n with
    | Vector.nil ⇒ fun _ ⇒ Vector.nil
    | Vector.cons a _ w ⇒ fun H ⇒
      Vector.cons (exist P a (proj1 H)) (Vsig_of_v P w (proj2 H))
  end.

Section Vforall2_sec.

Variable R : A → A → Prop.

Fixpoint Vforall2 n1 (v1 : vec n1) n2 (v2 : vec n2) {struct v1} : Prop :=
  match eq_nat_dec n1 n2 with
  | left _ ⇒
      match v1 with
      | Vector.nil ⇒ True
      | Vector.cons a _ v ⇒
          match v2 with
          | Vector.nil ⇒ False
          | Vector.cons b _ w ⇒ R a b ∧ Vforall2 v w
          end
      end
  | _ ⇒ False
  end.

Definition Vforall2n n (v1 v2 : vec n) := Vforall2 v1 v2.

Lemma Vforall2_tail : ∀ n (v1 v2 : vec (S n)), Vforall2 v1 v2 →
  Vforall2 (Vector.tl v1) (Vector.tl v2).

Proof.
  intros. VSntac v1. rewrite H0 in H. VSntac v2. rewrite H1 in H.
  simpl in H. rewrite eq_nat_dec_refl in H. destruct H. exact H2.
Qed.

Lemma Vforall2n_tail : ∀ n (v1 v2 : vec (S n)), Vforall2n v1 v2 →
  Vforall2n (Vector.tl v1) (Vector.tl v2).

Proof.
  intros. unfold Vforall2n. apply Vforall2_tail. assumption.
Qed.

Lemma Vforall2_nth : ∀ n (v1 : Vector.t A n) (v2 : Vector.t A n) i
  (ip : i < n), Vforall2n v1 v2 → R (Vnth v1 ip) (Vnth v2 ip).

Proof.
  induction n; intros. absurd_arith.
  VSntac v1. VSntac v2.
  destruct i. simpl.
  rewrite H0 in H. rewrite H1 in H.
  unfold Vforall2n in H. simpl in H.
  rewrite eq_nat_dec_refl in H. destruct H. trivial.
  simpl. apply IHn.
  unfold Vforall2n. apply Vforall2_tail. assumption.
Qed.

Lemma Vforall2_intro : ∀ n (v1 : vec n) (v2 : vec n),
  (∀ i (ip : i < n), R (Vnth v1 ip) (Vnth v2 ip)) → Vforall2n v1 v2.

Proof.
  induction n; intros.
  VOtac. constructor.
  VSntac v1. VSntac v2.
  unfold Vforall2n. simpl.
  rewrite eq_nat_dec_refl. split.
  do 2 rewrite Vhead_nth. apply H.
  apply IHn. intros.
  do 2 rewrite Vnth_tail. apply H.
Qed.

Require Import RelDec.

Variable R_dec : rel_dec R.

Lemma Vforall2_dec : ∀ n1 (v1 : Vector.t A n1) n2 (v2 : Vector.t A n2),
  {Vforall2 v1 v2} + {¬Vforall2 v1 v2}.

Proof.
  induction v1; intros; destruct v2; simpl; auto.
  destruct (eq_nat_dec n n0); simpl; auto.
  destruct (IHv1 n0 v2); intuition.
  destruct (R_dec h h0); intuition.
Defined.

Lemma Vforall2n_dec : ∀ n, rel_dec (@Vforall2n n).

Proof.
  intros n v1 v2. unfold Vforall2n. apply Vforall2_dec.
Defined.

End Vforall2_sec.

Section Vexists.

Fixpoint Vexists (P : A → Prop) n (v : vec n) {struct v} : Prop :=
  match v with
  | Vector.nil ⇒ False
  | Vector.cons a _ w ⇒ P a ∨ Vexists P w
  end.

End Vexists.

Program Fixpoint Vbuild_spec (n : nat) (gen : ∀ i, i < n → A) :
  { v : vec n | ∀ i (ip : i < n), Vnth v ip = gen i ip } :=
  match n with
  | 0 ⇒ Vector.nil
  | S p ⇒
      let gen' := fun i ip ⇒ gen (S i) _ in
        Vector.cons (gen 0 _) (@Vbuild_spec p gen')
  end.

Next Obligation.
  exfalso. omega.
Qed.
Next Obligation.
  omega.
Qed.
Next Obligation.
  omega.
Qed.
Next Obligation.
  simpl.
  destruct i.
  f_equal. apply lt_unique.
  rewrite e. f_equal. apply lt_unique.
Defined.

Definition Vbuild n gen : vec n := proj1_sig (Vbuild_spec gen).

Lemma Vbuild_nth : ∀ n gen i (ip : i < n),
  Vnth (Vbuild gen) ip = gen i ip.

Proof.
  intros. unfold Vbuild. destruct (Vbuild_spec gen). simpl. apply e.
Qed.

Lemma Vbuild_head : ∀ n (gen : ∀ i, i < S n → A),
  Vector.hd (Vbuild gen) = gen 0 (lt_O_Sn n).

Proof.
  intros. unfold Vbuild. destruct (Vbuild_spec gen). simpl.
  rewrite Vhead_nth. apply e.
Qed.

Lemma Vbuild_tail : ∀ n (gen : ∀ i, i < S n → A),
  Vector.tl (Vbuild gen) = Vbuild (fun i ip ⇒ gen (S i) (lt_n_S ip)).

Proof.
  intros. apply Veq_nth. intros.
  rewrite Vnth_tail. do 2 rewrite Vbuild_nth. reflx.
Qed.

Fixpoint Vfold_left (B : Type) (f : B→A→B) (b:B) n (v : vec n)
  {struct v} : B :=
  match v with
    | Vector.nil ⇒ b
    | Vector.cons a _ w ⇒ f (Vfold_left f b w) a
  end.


Fixpoint Vfold_right (B : Type) (f : A→B→B) n (v : vec n) (b:B)
  {struct v} : B :=
  match v with
    | Vector.nil ⇒ b
    | Vector.cons a _ w ⇒ f a (Vfold_right f w b)
  end.

Require Import List.

Fixpoint vec_of_list (l : list A) : vec (length l) :=
  match l with
  | nil ⇒ Vector.nil
  | cons x m ⇒ Vector.cons x (vec_of_list m)
  end.

Fixpoint list_of_vec n (v : vec n) {struct v} : list A :=
  match v with
  | Vector.nil ⇒ nil
  | Vector.cons x _ v ⇒ x :: list_of_vec v
  end.

Lemma in_list_of_vec : ∀ n (v : vec n) x, In x (list_of_vec v) → Vin x v.

Proof.
induction v; simpl; intros. assumption. destruct H. auto. right. auto.
Qed.

Lemma vec_of_list_exact i l (Hi :i < length(l)) :
  element_at l i = Some (Vnth (vec_of_list l) Hi).

Proof.
induction i in l, Hi |- ×.
destruct l; simpl in ×. contradict Hi; omega. auto.
destruct l;simpl in ×. contradict Hi; omega. apply IHi.
Qed.

Lemma list_of_vec_exact i n (v:Vector.t A n) (Hi:i < n) :
  element_at (list_of_vec v) i = Some (Vnth v Hi).

Proof.
induction i in n, v, Hi |- ×.
destruct v; simpl in ×. contradict Hi; omega. auto.
destruct v; simpl in ×. contradict Hi; omega. apply IHi.
Qed.

Section eq_dec.

Variable eq_dec : ∀ x y : A, {x=y}+{¬x=y}.

Lemma eq_vec_dec : ∀ n (v1 v2 : vec n), {v1=v2}+{¬v1=v2}.

Proof.
induction v1; intro. VOtac. auto. VSntac v2.
case (eq_dec h (Vector.hd v2)); intro.
rewrite e. case (IHv1 (Vector.tl v2)); intro. rewrite e0. auto.
right. unfold not. intro. Veqtac. auto.
right. unfold not. intro. Veqtac. auto.
Defined.

End eq_dec.

Section beq.

Variable beq : A → A → bool.
Variable beq_ok : ∀ x y, beq x y = true ↔ x = y.

Fixpoint beq_vec n (v : vec n) p (w : vec p) {struct v} :=
  match v, w with
  | Vector.nil, Vector.nil ⇒ true
  | Vector.cons x _ v', Vector.cons y _ w' ⇒ beq x y && beq_vec v' w'
  | _, _ ⇒ false
  end.

Lemma beq_vec_refl : ∀ n (v : vec n), beq_vec v v = true.

Proof.
induction v; simpl. reflx. apply andb_intro. apply (beq_refl beq_ok). exact IHv.
Qed.

Lemma beq_vec_ok_length : ∀ n (v : vec n) p (w : vec p),
  beq_vec v w = true → n = p.

Proof.
induction v; destruct w; simpl; intros; try (reflx || discriminate).
destruct (andb_elim H). ded (IHv _ _ H1). subst n0. reflx.
Qed.

Implicit Arguments beq_vec_ok_length [n v p w].

Lemma beq_vec_ok1 : ∀ n (v : vec n) p (w : vec p) (leq : n = p),
  beq_vec v w = true → Vcast v leq = w.

Proof.
induction v; destruct w; simpl; intros; try (reflx || discriminate).
destruct (andb_elim H). rewrite beq_ok in H0. subst h. apply Vtail_eq.
apply IHv. assumption.
Qed.

Lemma beq_vec_beq_impl_eq : ∀ n (v w : vec n),
  beq_vec v w = true → v = w.

Proof.
  intros. rewrite <- (Vcast_refl v). apply beq_vec_ok1. assumption.
Qed.

Lemma beq_vec_ok2 : ∀ n (v w : vec n), v = w → beq_vec v w = true.

Proof.
induction v; intros. VOtac. reflx. VSntac w. rewrite H0 in H. Veqtac. subst h.
subst v. simpl. rewrite (beq_refl beq_ok). simpl. apply beq_vec_refl.
Qed.

End beq.

Implicit Arguments beq_vec_ok_length [n v p w].

Section beq_in.

Variable beq : A → A → bool.

Lemma beq_vec_ok_in1 : ∀ n (v : vec n)
  (hyp : ∀ x, Vin x v → ∀ y, beq x y = true ↔ x = y)
  p (w : vec p) (h : beq_vec beq v w = true),
  Vcast v (beq_vec_ok_length beq h) = w.

Proof.
induction v; destruct w; simpl; intro; try (reflx || discriminate).
destruct (andb_elim h1).
assert (ha : Vin h (Vector.cons h v)). simpl. auto.
ded (hyp _ ha h0). rewrite H1 in H. subst h0. apply Vtail_eq.
assert (hyp' : ∀ x, Vin x v → ∀ y, beq x y = true ↔ x=y).
intros x hx. apply hyp. simpl. auto.
destruct (andb_elim h1). ded (IHv hyp' _ w H2). rewrite <- H3.
apply Vcast_prf_eq.
Qed.

Lemma beq_vec_ok_in2 : ∀ n (v : vec n)
  (hyp : ∀ x, Vin x v → ∀ y, beq x y = true ↔ x = y) w,
  v = w → beq_vec beq v w = true.

Proof.
induction v; intros. VOtac. reflx. VSntac w. rewrite H0 in H. Veqtac. subst h.
simpl. apply andb_intro. set (a := Vector.hd w).
assert (Vin a (Vector.cons a v)). simpl. auto.
ded (hyp _ H a). rewrite H1. reflx.
apply IHv. intros. apply hyp. simpl. auto. exact H3.
Qed.

End beq_in.

End S.

Implicit Arguments VSn_eq [A n].
Implicit Arguments Vsig_of_v [A P n v].
Implicit Arguments Vbreak [A n1 n2].
Implicit Arguments Vbreak_eq_app [A n1 n2].
Implicit Arguments Vbreak_eq_app_cast [A n n1 n2].
Implicit Arguments Vforall_in [A P x n v].
Implicit Arguments Vin_cast_elim [A m n H v x].
Implicit Arguments Vin_elim [A x n v].
Implicit Arguments Vin_app [A x n1 v1 n2 v2].
Implicit Arguments beq_vec_ok_in1 [A beq n v p w].
Implicit Arguments beq_vec_ok_in2 [A beq n v w].
Implicit Arguments in_list_of_vec [A n v x].

Ltac VOtac := repeat
  match goal with
    | v : Vector.t _ O |- _ ⇒ assert (v = Vector.nil); [apply VO_eq | subst v]
  end.

Ltac VSntac y :=
  match type of y with
    | Vector.t _ (S _) ⇒ let H := fresh in
      (assert (H : y = Vector.cons (Vector.hd y) (Vector.tl y)); [apply VSn_eq | rewrite H])
  end.

Ltac castrefl h := rewrite (UIP_refl eq_nat_dec h); rewrite Vcast_refl; reflx.

Section map.

Variables (A B : Type) (f : A→B).

Fixpoint Vmap n (v : Vector.t A n) {struct v} : Vector.t B n :=
  match v with
  | Vector.nil ⇒ Vector.nil
  | Vector.cons a _ v' ⇒ Vector.cons (f a) (Vmap v')
  end.

Lemma Vnth_map : ∀ n (v : Vector.t A n) i (H : i < n),
  Vnth (Vmap v) H = f (Vnth v H).

Proof.
intros n. elim n.
 intros v i H. elimtype False. apply (lt_n_O _ H).
 clear n. intros n Hrec v i. case i.
  intro. rewrite (VSn_eq v). simpl. reflx.
  clear i. intros i Hi. rewrite (VSn_eq v). simpl.
  apply (Hrec (Vector.tl v) i (lt_S_n Hi)).
Qed.

Lemma Vin_map : ∀ x n (v : Vector.t A n), Vin x (Vmap v)
  → ∃ y, Vin y v ∧ x = f y.

Proof.
induction v; simpl; intros. contradiction. destruct H. subst x. ∃ h. auto.
assert (∃ y, Vin y v ∧ x = f y). apply IHv. assumption.
destruct H0 as [y]. ∃ y. intuition.
Qed.

Lemma Vin_map_intro : ∀ x n (v : Vector.t A n),
  Vin x v → Vin (f x) (Vmap v).

Proof.
induction v; simpl; intros. contradiction. destruct H. subst x. auto. intuition.
Qed.

Lemma Vforall_map_elim : ∀ (P : B→Prop) n (v : Vector.t A n),
  Vforall P (Vmap v) → Vforall (fun a : A ⇒ P (f a)) v.

Proof.
induction v; simpl; intuition.
Qed.

Lemma Vforall_map_intro : ∀ (P : B→Prop) n (v : Vector.t A n),
  Vforall (fun a : A ⇒ P (f a)) v → Vforall P (Vmap v).

Proof.
induction v; simpl; intuition.
Qed.

Lemma Vmap_app : ∀ n1 n2 (v1 : Vector.t A n1) (v2 : Vector.t A n2),
  Vmap (Vapp v1 v2) = Vapp (Vmap v1) (Vmap v2).

Proof.
intros; induction v1.
simpl; auto.
simpl. rewrite IHv1. reflx.
Qed.

Lemma Vmap_cast : ∀ m n (H : m=n) (v : Vector.t A m),
  Vmap (Vcast v H) = Vcast (Vmap v) H.

Proof.
intros until H. case H. intro v. repeat rewrite Vcast_refl. reflx.
Qed.

Lemma Vmap_tail : ∀ n (v : Vector.t A (S n)),
  Vmap (Vector.tl v) = Vector.tl (Vmap v).

Proof.
intros. VSntac v. reflx.
Qed.

Lemma Vmap_eq_nth : ∀ n (v1 : Vector.t A n) (v2 : Vector.t B n),
  (∀ i (h : i<n), f (Vnth v1 h) = Vnth v2 h) → Vmap v1 = v2.

Proof.
induction n; simpl; intros. VOtac. reflx.
VSntac v1. VSntac v2. simpl. apply Vcons_eq.
do 2 rewrite Vhead_nth. apply H.
apply IHn. intros. do 2 rewrite Vnth_tail. apply H.
Qed.

End map.

Implicit Arguments Vin_map [A B f x n v].
Implicit Arguments Vforall_map_elim [A B f P n v].
Implicit Arguments Vin_map_intro [A B x n v].