(* VECTORS                     *)
(* Venanzio Capretta, Jun 2005 *)
(* Coq version 8.0             *)

(* There are three definition of vectors/finite sequences:
    vector: inductive definition;
    Vector: functional definition (functions on finite types);
    tuples: recursive products.
*)

Require Import Arith.
Require Import Max.

Inductive vector (A:Set): nat -> Set :=
  vec_nil: vector A 0
| vec_cons: forall n:nat, vector A n -> A -> vector A (S n).

Implicit Arguments vec_cons.

Definition vector_head: forall (A:Set)(n:nat),(vector A (S n)) -> A.
intros A n v; inversion_clear v.
exact H0.
Defined.

Implicit Arguments vector_head [A n].

Definition vector_tail: forall (A:Set)(n:nat),(vector A (S n)) -> (vector A n).
intros A n v; inversion_clear v.
exact H.
Qed.

Implicit Arguments vector_tail [A n].

(* Finite types *)

Inductive Finite: nat -> Set :=
  fin_zero: forall n:nat, Finite (S n)
| fin_succ: forall n:nat, Finite n -> Finite (S n).

Implicit Arguments fin_succ [n].

Lemma fin_0_empty: (Finite 0) -> False.
Proof.
intro i; inversion i.
Qed.

Fixpoint nat_finite (n:nat){struct n}: forall k:nat, k<n -> Finite n :=
match n return (forall k:nat, k<n -> Finite n) with
  O => fun (k:nat)(h:k<O) =>
         False_rec (Finite O) (lt_n_O k h)
| (S n') => fun k:nat =>
              match k return (k<(S n') -> Finite (S n')) with
                O => fun _ => (fin_zero n')
              | (S k') => fun h:S k' < S n' =>
                            fin_succ (nat_finite n' k' 
                                          (lt_S_n k' n' h))
              end
end.

Implicit Arguments nat_finite [n].

Fixpoint finite_nat (n:nat)(i:Finite n){struct i}: nat :=
match i with
  fin_zero n => 0
| fin_succ n i' => S (finite_nat n i')
end.

Implicit Arguments finite_nat [n].

Lemma nat_finite_id:
  forall (n k:nat)(h:k<n), (finite_nat (nat_finite k h)) = k.
Proof.
induction n.
intros k h; elim (lt_n_O k h).
induction k.
auto.
intro h; simpl.
rewrite IHn.
trivial.
Qed.

Lemma finite_lt_n:
  forall (n:nat)(i:Finite n), (finite_nat i)<n.
Proof.
induction i.
simpl; apply lt_O_Sn.
simpl; apply lt_n_S; assumption.
Qed.

Lemma finite_nat_id_general:
  forall (n:nat)(i:Finite n)(h:(finite_nat i)<n),
    (nat_finite (finite_nat i) h) = i.
Proof.
induction i.
auto.
intro h; simpl; rewrite IHi; auto.
Qed.

Lemma finite_nat_id:
  forall (n:nat)(i:Finite n),
    (nat_finite (finite_nat i) (finite_lt_n n i)) = i.
Proof.
intros; apply finite_nat_id_general; auto.
Qed.

Lemma finite_case:
  forall (n:nat)(i:Finite (S n)),
    i=fin_zero n \/ exists j:Finite n, i=fin_succ j.
Proof.
set (Q:= (fun n:nat =>
           match n return (Finite n) -> Prop with
             O => fun i:(Finite 0) => True
           | (S n) => fun i:(Finite (S n)) =>
                        i=fin_zero n \/ exists j:Finite n, i=fin_succ j
           end)
      : forall n:nat, (Finite n) -> Prop).
cut (forall (n:nat)(i:Finite n),(Q n i)).
intros HQ n i; apply (HQ (S n) i).
induction i.
simpl; left; trivial.
simpl; right.
exists i; trivial.
Qed.

(* To construct a vector in one go: vector_make n a1 ... an *)

Fixpoint pow_fun (n:nat)(A B:Set){struct n}: Set :=
match n with
  0 => B
| (S n) => A -> pow_fun n A B
end.

Fixpoint pow_fun_map (n:nat)(A B C:Set){struct n}:
  (B->C) -> pow_fun n A B -> pow_fun n A C :=
match n return (B->C) -> pow_fun n A B -> pow_fun n A C with
  O => fun f => f
| (S n) => fun f => fun pf => fun a:A => pow_fun_map n A B C f (pf a)
end.

Fixpoint vector_make (A:Set)(n:nat){struct n}: pow_fun n A (vector A n) :=
match n return pow_fun n A (vector A n) with
  0 => vec_nil A
| (S n) => fun a:A => pow_fun_map n A (vector A n) (vector A (S n))
                                  (fun v => vec_cons v a)
                                  (vector_make A n)
end.

Implicit Arguments vector_make [A].

Section Vectors.

Variable A:Set.

Definition Vector: nat -> Set :=
fun n:nat => (Finite n) -> A.

Definition vec_proj: forall n:nat, Vector n -> Finite n -> A :=
fun n v i => v i.

Definition vector_0: Vector 0 :=
  fun i:(Finite 0) => False_rec A (fin_0_empty i).

End Vectors.

Implicit Arguments vec_proj [A n].

Fixpoint vector_max (m:nat): Vector nat m -> nat :=
match m return (Vector nat m)->nat with
  O => fun _ => 0
| S m => fun v => max (v (fin_zero m))
                      (vector_max m (fun j => (v (fin_succ j))))
end.
Implicit Arguments vector_max [m].

Lemma vector_max_le:
  forall (m:nat)(v:Vector nat m)(i:Finite m), v i <= (vector_max v).
Proof.
induction i; simpl.
apply le_max_l.
apply le_trans with  (vector_max (fun j : Finite n => v (fin_succ j))).
apply (IHi (fun j : Finite n => v (fin_succ j))).

apply le_max_r; auto.
Qed.

(* Tuples: Another way to describe vectors *)

Section Tuples.

Variable A:Set.

Fixpoint Tuple (n:nat){struct n}: Set :=
match n with
  O => unit
| (S n') => (A*(Tuple n'))%type
end.

Fixpoint tuple_proj (n:nat){struct n}: forall k:nat, k<n -> Tuple n -> A :=
match n return (forall k:nat, k<n -> Tuple n -> A) with
  O => fun (k:nat)(h:k<O)(v:Tuple 0) =>
         False_rec A (lt_n_O k h)
| (S n') => fun k:nat =>
              match k return (k<(S n') -> Tuple (S n') -> A) with
                O => fun (h:0<(S n'))(v:Tuple (S n')) => (fst v)
              | (S k') => fun (h:S k' < S n')(v:Tuple (S n')) =>
                            (tuple_proj n' k' (lt_S_n k' n' h) (snd v))
              end
end.

End Tuples.

Implicit Arguments tuple_proj [A n].

Section Function_Tuples.

Variables A B:Set.

Fixpoint mult_app (n:nat){struct n}:
  Tuple (A->B) n -> A -> Tuple B n :=
match n return Tuple (A->B) n -> A -> Tuple B n with
  0 => fun (f:unit)(a:A) => tt
| (S n') => fun (f:(A->B)*(Tuple (A->B) n'))
                (a:A)
            => let (f0,f'):=f in (f0 a, mult_app n' f' a)
end.

End Function_Tuples.

Implicit Arguments mult_app [A B n].