Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
    
Unless I am mistaken, no question is asked here. (This reminds me of math.stackexchange.com/questions/36676.) –  Did Aug 17 '11 at 21:35
    
You're quite right, I'll fix it. –  Tilo Wiklund Aug 18 '11 at 0:28
add comment

Know someone who can answer? Share a link to this question via email, Google+, Twitter, or Facebook.

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.