vector.v

From Equations Require Import Equations.

(** finite types and vector definitons *)

Section BASICS.
  Inductive fin : nat -> Type :=
  | FZero : forall n, fin (S n)
  | FSucc : forall n, fin n -> fin (S n).

  Derive Signature for fin.

  Arguments FZero {n}.
  Arguments FSucc {n}.

  Inductive vec (A : Type) : nat -> Type :=
  | VNil  : vec A 0
  | VCons : forall n, A -> vec A n -> vec A (S n).

  Derive Signature for vec.

  Arguments VNil {_}.
  Arguments VCons {_}{n}.

  Equations vlookup {A}{n}(i : fin n) (v : vec A n) : A :=
    vlookup  FZero (VCons x _) := x ;
    vlookup  (FSucc ix) (VCons _ xs) := vlookup ix xs.
   
  Inductive vforall {A : Type}(P : A -> Type) : forall n, vec A n -> Type :=
  | VFNil  : vforall P _ VNil
  | VFCons : forall n x xs,
      P x -> vforall P n xs -> vforall P (S n) (VCons x xs).

  Derive Signature for vforall.

  Arguments vforall {_}(P){n}.

  Equations vforall_lookup
            {n}
            {A : Type}
            {P : A -> Type}
            {xs : vec A n}
            (idx : fin n) :
            vforall P xs -> P (vlookup idx xs) :=
    vforall_lookup FZero (VFCons _ _ pf _) := pf ;
    vforall_lookup (FSucc ix) (VFCons _ _ _ ps) := vforall_lookup ix ps.
End BASICS.