Typeclasses on functions

Using Coq
1

I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue:

(* Note that I don't actually have this class in my real code, this is just the
simplest way I could find to demonstrate the issue. *)
Class Trivial {U V} (f : U -> V) := {
    trivial : forall a b, f a = f b
}.

Definition zero (a : nat) := 0.

Instance zero_trivial : Trivial zero.
Proof.
    split.
    reflexivity.
Qed.

Theorem fails : zero 0 = 0.
Proof.
     rewrite (trivial (f := zero) 0 1). (* succeeds *)
     rewrite (trivial 1 0). (* succeeds *)
     rewrite (trivial 0 1). (* fails *)
Abort.

When trying to run that last rewrite, Coq says

Unable to satisfy the following constraints:

?Trivial : "Trivial (eq (zero 0))"

It seems that Coq is interpreting equality as the function I’m trying to say is trivial. I can get around this by specifying the function explicitly as I did in the first rewrite, but that’s cumbersome. So I guess I have two questions. First, I thought that typeclass resolution would keep skipping things until it found something that worked. So why is it getting stuck on trying to use equality as my function? It’s also strange that the second rewrite works but the third one doesn’t. Second, is there any easy way around this issue? I know that I can specify the function explicitly as above. I could also do some crazy thing where I make functions that typeclasses can apply to be their own type, but I feel like there has to be a simple way to do this.

1 Like
2

Just an observation: it seems like setoid_rewrite (trivial 0 1). works, i.e. picks out the right Trivial instance, so rewrite and setoid_rewrite differ in some way here. However, this doesn’t seem to work always, as this person experienced setoid_rewrite failed with MathClasses Coq - Stack Overflow

Alternatively, pose also picks out the right Trivial instance, so introducing the lemma in the environment with pose proof (trivial 1 0) as H. gives you H: zero 1 = zero 0 which you can rewrite with.