How to unfold a typeclass definition?

Stream: new members

[Timothy Mou]

I have defined the following Add instance and written a lemma:

instance BV.instadd : Add (Vector Bool n) where
  add := Vector.map₂ xor

lemma f1 (v1 v2 : Vector Bool (n + 1)) :
  (Vector.map₂ xor v1 v2).tail = Vector.map₂ xor v1.tail v2.tail := by
    match v1, v2 with
    | ⟨ x :: xs , _ ⟩, ⟨ y :: ys, _ ⟩ =>
        simp [Vector.map₂, Vector.tail, List.zipWith]

lemma f2 (v1 v2 : Vector Bool (n + 1)) :
  (v1 + v2).tail = v1.tail + v2.tail := by
  apply f1

f1 and f2 are the same, except in f1 I have just unfolded the definition of +. The statements are definitionally equal. But I can't use the proof of f1 in f2. I don't know how to unfold or simplify the instance definition. I have tried unfold BV.instadd, simp [BV.instadd], unfold +, etc. How can I prove f2 without having to manually unfold the definitions?

Also I'm kinda confused how typeclass instance resolution works. Is there coherence guarantees? Since it seems like I can define an overlapping instance like

instance BV.instadd' : Add (Vector Bool n) where
  add := Vector.map₂ or

and then how would it know which instance to select?

[Kevin Buzzard]

Typeclass instance coherence: If you make two Add instances on a type then your mental model should be that it will select a random one. There's no coherence guarantee,

[Timothy Mou]

I suppose that makes sense to not have coherence, since you have the option of manually applying typeclass instances.
Can anyone help me with my first question?

[Kyle Miller]

A syntax for unfolding + is simp [(· + ·)].

Mathlib has an unfold_projs tactic that might help unfold all the instances

[Timothy Mou]

Thanks, unfold_projs is what I was looking for.