The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

As you noted, extensional equality on function types is only a partial equivalence relation in cases where the domain type has a non-syntactic equality -- reflexivity only holds for functions that are setoid morphisms.

Perhaps the Reflexive class was not designed to cover such partiality.

You can make a set type of functions that are setoid morphisms, but additional work (eta expansion of dependent pairs) would be needed before invoking reflexivity.

Instead, you can redefine `reflexivity` using Ltac, as Jason showed in a coq-club post on 12/23/15.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Jan 6, 2016 at 1:08 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

On Jan 5, 2016, at 21:46 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Sorry, I forgot that I had to make another fix to your code.

Thanks! That was it. Now about your other suggestion:

1) Take a look at  MathClasses.theory.setoids.ext_equiv_refl 

Moreover, you might want to reuse MathClasses.interfaces.abstract_algebra.Setoid_Morphism instead of defining your own `O`.

That was also super helpful! I still want to have my own class but I just defined it as:

  Class O (op: A -> A) :=

    o_setoidmor :> Setoid_Morphism op.

and if I use `apply ext_equiv_refl` instead of `reflexivity` everything works just great. Here is full example: http://ideone.com/rbD6rv reworked per your suggestions.

However I am still wondering if there is a way to declare such refined/specialized instance of ‘Reflexive’ for Setoid_Morphisms so 

reflexivity tactics would work as well?

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva