1
$\begingroup$

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).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.