The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Nov 18, 2014 at 3:25 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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.

Hmm, that would be a bit tricky - as far as I know, Proper isn't really defined for functions taking dependent types.  I was able to get around it with my definition by using the fact that my @vector_cons A n was a simply typed function for each A, n.  Maybe you could define your own version of Vcons with arguments reordered, then provide trivial rewriting lemmas to convert Vcons to myVcons, and then you could use some Proper result on myVcons to do setoid rewriting.

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?

Using Proper constructor types is a syntactic trick for generating the relation of two vectors having their elements pointwise equivalent, as an inductive relation:

Inductive vector_equiv (A:Type) `{Equiv A} :

  forall n:nat, vector A n -> vector A n -> Prop :=

| vector_nil_equiv : vector_equiv A 0 (@vector_nil A) (@vector_nil A)

| vector_cons_equiv : forall (n:nat) (h1 h2:A), eqv h1 h2 ->

  forall (t1 t2:vector A n), vector_equiv A n t1 t2 ->

  vector_equiv A (S n) (vector_cons A h1 t1) (vector_cons A h2 t2).

But the point is that the Proper version is very easy to generalize to other inductive types (e.g. abstract syntax trees for some algebra signature).

-- 

Daniel Schepler