3
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ My guess is that if you say rewrite (trivial a b), coq has to find a higher order term T such that T a is a subterm and rewrite it to T b. So your second example works because there is only one occurrence of 1, so T = (fun x -> (zero x)). The third fails because it will try T = (fun x -> zero 0 = x). I assume typeclasses were designed with the assumption that the typeclass would be parametrized over a type, rather than a term. $\endgroup$
    – Couchy ♦
    Sep 28, 2022 at 2:12
  • 1
    $\begingroup$ This may be a case of the XY problem. What are you actually trying to accomplish? $\endgroup$
    – Andrej Bauer
    Oct 2, 2022 at 7:33
  • $\begingroup$ I said at the top that I'm trying to generalize the different notions of homomorphisms. $\endgroup$
    – sudgy
    Oct 3, 2022 at 15:36
  • 1
    $\begingroup$ @sudgy Could you explain what you mean by that? It's not at all clear from your question. $\endgroup$
    – Couchy ♦
    Oct 4, 2022 at 2:50
  • $\begingroup$ As an example, I have many different examples of group homomorphisms, and several repeated proofs of things like f(0) = 0 and f(-a) = -f(a). I want to be able to have a single "f(0) = 0" theorem and a single "f(-a) = -f(a)" theorem that all the different examples can use. I also have several different types of homomorphisms (group homomorphisms, ring homomorphisms, etc.) and want to be able to use things about (say) group homomorphisms on ring homomorphisms (such as using the same "f(0) = 0" and "f(-a) = -f(a)" theorems on ring homomorphisms). $\endgroup$
    – sudgy
    Oct 5, 2022 at 21:38

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.