The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Dear all,

This is a follow-up to some questions on the list a few months back.
Having focussed on other parts of our projects for a while, we now
return to our vectors, unfortunately to be confronted with new problems.

Original thread is here
  http://logical.saclay.inria.fr/coq-puma/messages/9978d9af68461f02


In the definitions of functions on vectors such as take, drop, and nth,
we would use proofs of 'le' ord 'lt', e.g.:

  Definition vtake (n m : nat) : n <= m -> vector m -> vector n.

But unfortunately, we cannot deconstruct the proof of n <= m since it
lives in Prop. Now, my guess is that there is no real solution to this
problem, but then again, I'm still quite new to Coq.

I see two (not so great) solutions:

1) Instead of the proof, ask for a vector of at least the right size,
e.g.:

  Definition vtake (n m : nat) : vector (n + m) -> vector n.

But my first steps in using this definition in our development are not
really encouraging, we have to find m and cast the vector.

2) Instead of 'le' and 'lt', use new relations, not in Prop. I don't
really like the idea of duplicating a definition from the standard
library.

So I was wondering if anyone has a suggestion.

(A small piece of Coq code is attached.)

kind regards,
Martijn

Set Implicit Arguments.


Inductive Fin : nat -> Type :=
  | First : forall n, Fin (S n)
  | Next  : forall n, Fin n -> Fin (S n).

Lemma Fin_0_inv (A : Type) : Fin 0 -> A.
inversion 1.
Qed.


Section Vector.

Variable A : Type.

Definition vector (n : nat) := Fin n -> A.

Definition vnil : vector 0 := Fin_0_inv A.

Definition vcons (x : A) n (v : vector n) : vector (S n) :=
  let P :=
    fun k =>
    match k return Type with
    | O   => Empty_set
    | S n => vector n -> A
    end
  in
    fun i =>
    match i in Fin Sn return P Sn with
    | First _   => fun _ => x
    | Next _ i' => fun v => v i'
    end v.

Definition vhead (n : nat) (v : vector (S n)) : A :=
  v (First n).

Definition vtail (n : nat) (v : vector (S n)) : vector n :=
  fun i : Fin n => v (Next i).

Lemma le_weaken : forall n m, S n <= m -> n <= m.
Proof.
induction 1; auto.
Qed.

(* vtake n m H v is a vector with first n elements of v *)
(* First try, this is not complete yet, but deconstructing H would not be
   allowed anyway... *)
(*
Program Fixpoint vtake (n m : nat) : n <= m -> vector m -> vector n :=
  match n return n <= m -> vector m -> vector n with
  | O   => fun _ _ => vnil
  | S n => fun H => match H return vector m -> vector n with
                      | le_n       => fun v => vcons (vhead (n := n) v) 
(@vtake n n (le_n n) (vtail v))
                      | le_S m' H' => fun v => vcons (vhead (n := m') v) 
(@vtake n m' (le_weaken H') (vtail v))
                    end
  end.
*)

(* As a simpler example, translate something in Fin n to Fin m. *)
(*
Fixpoint project_i n m (i : Fin n) : (n <= m) -> Fin m :=
  match i in Fin n return (n <= m) -> Fin m with
  | First n'  => fun H => match H with
                 | le_n       => First n'
                 | le_S m' H' => First m'
                 end
  | Next n' i => fun H => match H with
                 | le_n       => Next (project_i i (le_n n'))
                 | le_S m' H' => Next (project_i i (le_weaken H'))
                 end
  end.
*)

(* The following are some alternative definitions, the don't seem to be
   ideal to use in our developments (m has to be constructed) *)

(* vtake n m v is a vector with first n elements of v *)
Fixpoint vtake' (n m : nat) : vector (n + m) -> vector n :=
  match n with
  | O   => fun _ => vnil
  | S n => fun v => vcons (vhead v) (vtake' m (vtail v))
  end.

Fixpoint vdrop' (n m : nat) : vector (n + m) -> vector m :=
  match n with
  | O   => fun v => v
  | S n => fun v => vdrop' n (vtail v)
  end.

Fixpoint vnth' (n m : nat) : vector (n + S m) -> A :=
  match n with
  | O   => fun v => vhead v
  | S n => fun v => vnth' n m (vtail v)
  end.

End Vector.


Implicit Arguments First [n].
Implicit Arguments vtake' [A m].
Implicit Arguments vnth' [A m].