The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Nov 18, 2014 at 11:58 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

> On Nov 18, 2014, at 11:33 , Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:
>
> You probably have forgotten to prove a Proper for Vcons.

Robbert,

Thanks! I also suspected that that might be the problem. How I should formulate
Propper instantiation in this case? My first naive attempt:

Instance Vcons_Proper:
    Proper (equiv ==> equiv) (Vcons).

did not work. Thanks!

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

(* crude reconstruction of what I need for the illustration *)

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

| vector_nil : vector A 0

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

Class Equiv (A:Type) :=

eqv : A -> A -> Prop.

Infix "=" := eqv.

Notation "(=)" := eqv.

(* end crude reconstruction section *)

Require Import Morphisms.

Inductive vector_equiv (A:Type) `{Equiv A} : forall n:nat, Equiv (vector A n) :=

| vector_nil_proper : Proper (vector_equiv A 0) (@vector_nil A)

| vector_cons_proper : forall n:nat,

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

  (@vector_cons A n).

Existing Instance vector_equiv.

Existing Instance vector_nil_proper.

Existing Instance vector_cons_proper.

-- 

Daniel Schepler