I am having some issues with, I suspect, transparency of fields in type classes. Consider a type class such as
Class CommutativeOperator ( Carrier : Type ) ( Equality : relation Carrier ) ( Op : operator Carrier ) : Prop := { equality := Equality where "a ≡ b" := (equality a b). ; op := Op where "a ⋆ b" := (op a b). ; commutative_proper : Proper (equality ==> equality ==> equality) op ; commutativity : ∀ a b, a ⋆ b ≡ b ⋆ a }.
And some object derived from the fields equality
and op
. Take for example
Definition square { L } `{ CommutativeOperator L } ( a : L ) := (op a a).
The problem is, now, that when one unfolds square
it uses the name op
rather than the name of the operator in the inferred instance, which is an issue, for example, when one is working with multiple instances of CommutativeOperator
at once (meaning the names from the instances are needed to disambiguate). Continuing by unfolding op
makes it use the names from the instance but, I am guessing due to some transparency reasons, results in the operator no longer being considered commutative, i.e. one can no longer rewrite with commutativity
(doing so results in a "goal contains no subterm of the form a ⋆ b").
Is there some way for me to keep the convenience of fields like equality
and op
without confusing instance resolution when rewriting?
EDIT: Turns out what I needed to do was use the setoid_rewrite tactic (after unfolding op).