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 using 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 using 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.
 generalize (Hrec (Vector.tl v)).
intro H. transitivity (Vector.cons (Vector.hd v) (Vector.tl v)).
apply VSn_eq. rewrite H. auto.
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].