Library Coqtail.Vec.Vec_prop

Require Import Vec_def.
Require Import Omega.
Require Import Ass_handling.
Require Import PI.

Lemma Vget_PI : ∀ {A : Type} {n : nat} (v : Vec A n) (m : nat) (mltn1 mltn2 : m < n),
      Vget v m mltn1 = Vget v m mltn2.
Proof.
intros A n v ; induction v.
 intros m H ; apply False_ind ; omega.
 destruct m ; simpl ; auto.
Qed.

Lemma Vmap_sound : ∀ (A B : Type) (n : nat) (f : A → B) (v : Vec A n)
  (p : nat) (pltn : p < n), Vget (Vmap f v) p pltn = f (Vget v p pltn).
Proof.
intros A B n f v ; induction v ; intros p pltn.
 inversion pltn.
 destruct p ; [reflexivity | simpl ; apply IHv].
Qed.

Lemma Vmap_full_sound : ∀ (A B : Type) (n : nat)
  (f : ∀ (m : nat) (mltn : m < n), A → B)
  (v : Vec A n) (p : nat) (pltn : p < n),
  Vget (Vmap_full f v) p pltn = f p pltn (Vget v p pltn).
Proof.
intros A B n f v ; induction v ; intros p pltn.
 inversion pltn.
 destruct p ; simpl ; [| rewrite IHv ] ;
 f_equal ; apply lt_PI.
Qed.

Definition Vec_rect2 : ∀ A (P : ∀ n, Vec A n → Vec A n → Type),
  P 0 Vnil Vnil → (∀ n h1 h2 (v1 v2 : Vec A n), P n v1 v2 → P (S n) (Vcon h1 v1) (Vcon h2 v2)) →
  ∀ n v1 v2, P n v1 v2 :=
fun A P H0 HS ⇒ fix F (n : nat) {struct n} :=
match n return ∀ (v1 v2 : Vec A n), P n v1 v2 with
| 0 ⇒ fun v1 ⇒
  match v1 in Vec _ m return
    match m with
    | 0 ⇒ ∀ v2 : Vec A m, P m v1 v2
    | S _ ⇒ False → False
    end
  with
  | Vnil ⇒ fun v2 ⇒
    match v2 in Vec _ m return
      match m return ∀ v2 : Vec A m, Type with
      | 0 ⇒ fun v2 ⇒ P 0 Vnil v2
      | S _ ⇒ fun v2 ⇒ False → False
      end v2
    with
    | Vnil ⇒ H0
    | Vcon _ _ _ ⇒ False_rect _
    end
  | Vcon _ _ _ ⇒ False_rect _
  end
| S n ⇒
  let F := F n in
  fun v1 ⇒ match v1 in Vec _ m return
    match m with
    | 0 ⇒ False → False
    | S m' ⇒ (∀ v1 v2, P m' v1 v2) → ∀ v2 : Vec A m, P m v1 v2
    end
  with
  | Vnil ⇒ False_rect _
  | Vcon _ h1 v1 ⇒ fun F v2 ⇒
    match v2 in Vec _ m return
      match m return ∀ v2 : Vec A m, Type with
      | 0 ⇒ fun v2 ⇒ False → False
      | S m ⇒ fun v2 ⇒ ∀ v1 : Vec A m, (∀ v2, P _ v1 v2) → P (S m) (Vcon h1 v1) v2
      end v2
    with
    | Vnil ⇒ False_rect _
    | Vcon _ h2 v2 ⇒ fun v1 F ⇒ HS _ h1 h2 v1 v2 (F v2)
    end v1 (F v1)
  end F
end.

Lemma Vec_ext_eq : ∀ (A : Type) (n : nat) (v1 v2 : Vec A n)
  (Hext : ∀ (p : nat) (pr : p < n), Vget v1 p pr = Vget v2 p pr),
  v1 = v2.
Proof.
intros A n v1 v2; pattern n, v1, v2; apply Vec_rect2; clear.
+ reflexivity.
+ intros n h1 h2 v1 v2 IH H; f_equal.
  - assert (pr : 0 < S n) by auto with arith.
    now apply (H 0 pr).
  - apply IH; intros p pr.
    assert (prS : S p < S n) by auto with arith.
    specialize (H _ prS); simpl in H.
    erewrite (Vget_PI v1), (Vget_PI v2); eassumption.
Qed.

Lemma genVec_pr_get : ∀ (n p : nat) (pr : p < n),
  Vget (genVec_pr n) p pr = exist _ p pr.
Proof.
intros n p pr ; unfold genVec_pr ; rewrite Vmap_full_sound ;
 reflexivity.
Qed.

Definition PI_fun {A n} (P : ∀ (m : nat), m < n → A) :=
  ∀ (m : nat) (pr1 pr2 : m < n), P m pr1 = P m pr2.

Lemma genVec_P_get : ∀ (A : Type) (n : nat) (P : ∀ (m : nat), m < n → A)
 (m : nat) (mltn : m < n), PI_fun P → Vget (genVec_P n P) m mltn = P m mltn.
Proof.
intros A n P m mltn HP ; unfold genVec_P ; rewrite Vmap_full_sound ;
reflexivity.
Qed.

Lemma genVec_get : ∀ (n p : nat) (pr : p < n), Vget (genVec n) p pr = p.
Proof.
intro n ; induction n ; intros p pr.
 inversion pr.
 destruct p ; [| simpl ; rewrite Vmap_full_sound] ; reflexivity.
Qed.