The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Hello again.

Having now completed the finite number type with the assistance
of this list, I've moved on to attempting to define a length-indexed
vector type:

Finite.v:

Inductive finite : nat -> Type :=
  | FO : forall (b : nat), finite (S b)
  | FS : forall (b : nat), finite b -> finite (S b).

Vector.v:

Require Finite.
Module F := Finite.

Inductive vector (A : Type) : nat -> Type :=
  | VZ : vector A 0
  | VC : forall {n : nat}, A -> vector A n -> vector A (S n).

The first two functions were trivial to define:

Fixpoint append {A : Type} {n m : nat} (v0 : vector A n) (v1 : vector A m) : 
vector A (n + m) :=
  match v0 with
    | VZ        => v1
    | VC _ x xs => VC A x (append xs v1)
  end.

Definition head {A : Type} (n : nat) (v : vector A (S n)) : A :=
  match v with
    | VZ       => tt (* Unreachable *)
    | VC _ x _ => x
  end.

However, I'm struggling somewhat to define the 'index' function. I've
written a quick informal proof but am having trouble telling coq about a
couple of the cases:

(*
  Assume b = 0. By the definition of 'finite', b > 0, therefore the
    assumption is invalid!

  Assume b = 1. If b = 1, then the following must hold:
    1. v must only contain one value (from the definition
       of the vector type's VC constructor).
    2. The only possible value of f is FO (from the definition
       of the finite type's constructors).

  In this case, the function returns the first and only element
  of the vector.

  Assume b = (S n) where n /= 0. If b = (S n), then the following must hold:
    1. v must contain at least two elements (from the definition
       of the vector type's VC constructor).
    2. The value of f may be FO or FS m, where m < b.

  In this case, the function matches the VC constructor and either
  of the FO or FS constructors.

  In the case of the FO constructor, the vector v is guaranteed to
  contain two or more elements and the function returns the first.

  In the case of the FS constructor, due to v containing at least two
  elements, the tail of v must contain at least one element and may
  be safely passed as an argument to the recursive call to index.
*)

Fixpoint index {A : Type} {b : nat} (f : F.finite b) (v : vector A b) : A :=
  match v return (b > 0 -> A) with
    | VZ        => fun p => _ (* Unreachable *)
    | VC _ x xs => fun _ =>
      match f with
        | F.FO _    => x
        | F.FS _ f' => index f' xs (* xs : vector A (S n), See informal proof 
above *)
      end
  end.

I'm aware that coq is unlikely to be able to infer that b > 0 directly
and have therefore annotated the first match so that it takes a proof
of b > 0, although I'm not sure what to do with this proof term. The
same really applies to the match on f, too.

Any assistance would, again, be appreciated!