From Coq Require Export Bool Arith Vector Lia.
Import Vector VectorNotations.

Arguments cons {A} _ {n} _ .
Arguments nil {A}.

Definition Vid {A : Type} {n:nat} : t A n → t A n :=
  match n with
    0 ⇒ fun v ⇒ []
  | S p ⇒ fun v ⇒ hd v :: tl v
  end.


Lemma Vid_eq : ∀ (n:nat) (A:Type)(v:t A n), v = Vid v.

Theorem t_0_nil : ∀ (A:Type) (v:t A 0), v = nil.

Theorem decomp :
  ∀ (A : Type) (n : nat) (v : t A (S n)),
    v = cons (hd v) (tl v).

Lemma decomp1 {A : Type} (v : t A 1):
  v = cons (hd v) (nil).

Definition vector_double_rect :
  ∀ (A:Type) (X: ∀ (n:nat),(t A n)->(t A n) → Type),
    X 0 nil nil →
    (∀ n (v1 v2 : t A n) a b, X n v1 v2 →
                                   X (S n) (cons a v1) (cons b v2)) →
    ∀ n (v1 v2 : t A n), X n v1 v2.
Defined.

Definition vector_triple_rect :
  ∀ (A:Type)
         (X: ∀ (n:nat),
             t A n → t A n → t A n →Type),
    X 0 nil nil nil →
    (∀ n (v1 v2 v3: t A n) a b c, X n v1 v2 v3→
                                       X (S n) (cons a v1) (cons b v2)(cons c v3)) →
    ∀ n (v1 v2 v3: t A n), X n v1 v2 v3.
Defined.

Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:t A p){struct v}
  : option A :=
  match n,v with
    _ , nil ⇒ None
  | 0 , cons b _ ⇒ Some b
  | S n', @cons _ _ p' v' ⇒ vector_nth A n' p' v'
  end.

Arguments vector_nth {A } n {p}.

Lemma Forall_inv {A :Type}(P: A → Prop)(n:nat)
  a v : Vector.Forall P (n:= S n) (Vector.cons a v) →
          P a ∧ Vector.Forall P v .

Lemma Forall2_inv {A B:Type}(P: A → B → Prop)(n:nat)
  a b v w : Vector.Forall2 P (n:=S n)
              (Vector.cons a v)
              (Vector.cons b w) →
            P a b ∧ Vector.Forall2 P v w.

Fixpoint vect_from_fun {A} (f : nat → A) n from : t A n :=
  match n return t A n with
    0%nat ⇒ nil
  | S p ⇒ cons (f from) (vect_from_fun f p (S from))
  end.

Notation vfst := Vector.hd.
Notation vsnd v := (Vector.hd (Vector.tl v)).
Notation vthird v := (Vector.hd (Vector.tl (Vector.tl v))).
Notation vfourth v := (Vector.hd (Vector.tl (Vector.tl (Vector.tl v)))).

Lemma decomp2 {A} : ∀ v : Vector.t A 2,
    v = [Vector.hd v; Vector.hd (Vector.tl v)].

Lemma decompos2 {A} : ∀ v: Vector.t A 2, {a : A & {b : A | v = [a;b]}}.

Definition match2 {A B:Type} (f : A → A → B) (v: Vector.t A 2): B :=
  match (decompos2 v )
  with existT _ x Hx ⇒
         match Hx with exist _ y _ ⇒ f x y end end.

Definition Vec2_proj {A} (P2 : A → A → Prop) : Vector.t A 2 → Prop.
Defined.


Ltac vdec2 v a b :=
  let x := fresh a in
  let y :=fresh b in
  let tmp := fresh "tmp" in
  let e :=fresh "e" in
  destruct (decompos2 v) as [x tmp]; destruct tmp as [y e]; subst v.

Lemma In_cases {A:Type}{n:nat} (v: t A (S n)) :
  ∀ x, In x v →
            x = hd v ∨ In x (tl v).

Lemma Forall_and {A:Type}(P: A → Prop) {n:nat} (v: t A (S n)) :
  Forall P v → P (hd v) ∧ Forall P (tl v).

Lemma Forall_forall {A:Type}(P: A → Prop) :
  ∀ {n:nat} (v: t A n) ,
    Forall P v ↔ (∀ a, In a v → P a).

Fixpoint max_v {n:nat} (v: Vector.t nat n) : nat :=
  match v with
  | nil ⇒ 0
  | cons x t ⇒ max x (max_v t)
  end.



Lemma max_v_2 : ∀ x y, max_v (x::y::nil) = max x y.

Lemma max_v_lub : ∀ n (v: t nat n) y,
    (Forall (fun x ⇒ x ≤ y) v) →
    max_v v ≤ y.

Lemma max_v_ge : ∀ n (v: t nat n) y,
    In y v → y ≤ max_v v.
Lemma max_v_tl {n:nat}(v: Vector.t nat (S n)) :
  max_v (Vector.tl v) ≤ max_v v.