The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Nov 18, 2014, at 12:41 , Daniel Schepler <dschepler AT gmail.com> wrote:

I often define the equivalence on container types using an inductive with constructors which are directly of a Proper type:

Daniel,

That is very helpful. However when I try to reconcile your definition with standard library vector

type I run into the same problem with Proper definition for Vcons. 

Your vector definition:

Inductive vector (A:Type) : nat -> Type :=

| vector_nil : vector A 0

| vector_cons : forall {n:nat}, A -> vector A n -> vector A (S n).

Standard library one:

Inductive t A : nat -> Type :=

|nil : t A 0

|cons : forall (h:A) (n:nat), t A n -> t A (S n).

I could not make it work with this:

…

| vector_cons_proper : forall n:nat,

  Proper ((=) ==> vector_equiv A n ==> vector_equiv A (S n))

  (@Vcons A n).

As cons types differ. I am working with standard vectors and would like to proove that Cons

is proper in first argument wrt ‘(=)’ for them.

P.S. I am also not sure I fully understand the mechanism of inductive Proper definition. Would it be

correct to say that Inductive type here is just a syntactic trick and the the same could be achieved

with non-inductive definition?

Sincerely,
Vadim