Zulip Chat Archive

Stream: maths

Topic: failed to unify


Joachim Breitner (Jan 29 2022 at 13:36):

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 (Jan 29 2022 at 13:37):

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 (Jan 29 2022 at 13:40):

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 (Jan 29 2022 at 13:41):

⊤.is_commutative is a bit roundabout

Joachim Breitner (Jan 29 2022 at 13:43):

Ah, maybe is_commutative G (*)

Eric Rodriguez (Jan 29 2022 at 13:45):

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

Kevin Buzzard (Jan 29 2022 at 13:47):

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

Joachim Breitner (Jan 29 2022 at 13:48):

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 (Jan 29 2022 at 13:52):

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 (Jan 29 2022 at 13:56):

You would usually put the comm_group.mk outermost

Joachim Breitner (Jan 29 2022 at 13:59):

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

Joachim Breitner (Jan 29 2022 at 13:59):

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

Stuart Presnell (Jan 29 2022 at 18:17):

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 (Jan 29 2022 at 18:17):

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

Anne Baanen (Jan 31 2022 at 10:58):

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


Last updated: Dec 20 2023 at 11:08 UTC