failed to unify

Stream: maths

[Joachim Breitner]

invalid apply tactic, failed to unify
  y * x = x * y
with
  y * x = x * y
state:
G : Type u_1,
_inst_1 : group G,
_inst_3 : comm_group G,
x y : G
⊢ y * x = x * y

irregardless of the current cause, maybe lean (and any other programming language around there) could be so kind and notice that when it produces a “failed to unify” error message with identical pretty-printed code, and maybe add a polite sentence like “and I’m sorry for the unhelpful error message”.

[Eric Rodriguez]

usually it unfolds the definitions it if things pretty print the same, I'm not sure why it didn't here. the issue is that you have two group instances, btw

[Joachim Breitner]

Hmm, maybe I am using comm_group G wrong then. How do I express that a group G for which I have group G is commutative? I didn't find a predicate G.abelian or something like that.

[Joachim Breitner]

⊤.is_commutative is a bit roundabout

[Joachim Breitner]

Ah, maybe is_commutative G (*)

[Eric Rodriguez]

cyclic sort of has to deal with this a little, ctrl+f "commutative" here to see some of what they do

[Kevin Buzzard]

If you're assuming [comm_group G] then don't assume [group G]

[Joachim Breitner]

So is this reasonable?

def _root_.group.comm_group_of_center_eq_top (h : center G = ⊤) : comm_group G :=
begin
  have h' : ∀ x, x ∈ center G, by {rw h, simp,},
  exact { mul_comm := λ x y, h' y x, .. (_ : group G) }
end

[Eric Rodriguez]

yeah, you can maybe golf it to this but otherwise fine:

def _root_.group.comm_group_of_center_eq_top (h : center G = ⊤) : comm_group G :=
let h' : ∀ x, x ∈ center G := by simp [h] in { mul_comm := λ x y, h' y x, .. (_ : group G) }

[Yaël Dillies]

You would usually put the comm_group.mk outermost

[Joachim Breitner]

Further refinements welcome at https://github.com/leanprover-community/mathlib/pull/11718 :-)

[Joachim Breitner]

Ah, this should probably be a def, not a lemma, if it returns comm_group, right?

[Stuart Presnell]

Joachim Breitner said:

maybe add a polite sentence like “and I’m sorry for the unhelpful error message”.

You're right that it would be good to have a more helpful error message here. This kind of error — things that pretty-print to the same thing but aren't considered identical — often seems to be due to typeclass problems. So maybe something could be added to the error message to direct the user to check their typeclasses?

[Stuart Presnell]

(I'm assuming here that it's possible to automatically detect that the pp output is identical in these cases.)

[Anne Baanen]

The error message is generated by apply_tactic.cpp:220, and there's similar code in tactic_state.cpp:513