Zulip Chat Archive

Stream: new members

Topic: Puzzling error message


view this post on Zulip Walter Moreira (Jun 13 2020 at 02:05):

This simple example does not compile and it shows a puzzling error message. The error message says that it cannot unify g * h = h * g with g * h = h * g. What am I doing wrong?

import tactic

example (G : Type*) [group G] [comm_group G] :
   g h : G, g * h = h * g :=
begin
intros,
apply mul_comm g h,
end

Screen-Shot-2020-06-12-at-9.03.50-PM.png

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:06):

whenever you see an error like that turn up the printing options

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:06):

set_option pp.all true

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:08):

In the error message you will see that it is trying to unify something about the inst_1 group to something about the inst_2 group

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:08):

You have endowed G with two incompatible group structures with your assumptions

view this post on Zulip Walter Moreira (Jun 13 2020 at 02:09):

Ah yes! Makes total sense. A bit difficult to read the error message with the full options, but I can see that now.

view this post on Zulip Walter Moreira (Jun 13 2020 at 02:38):

Following up on this, I'm confused about something that gives me an "extra" structure (which was what I was trying to #mwe before):

import tactic
import group_theory.order_of_element

example (G : Type*) [group G] [is_cyclic G]:
   g h : G, g * h = h * g :=
begin
intros,
have z := @is_cyclic.comm_group G _inst_1 _inst_2,
sorry
end

How do I use the mul_comm property of z to prove the goal? Every attempt seems to produce those two different structures in G that don't unify.

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:53):

Use letI

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:53):

example (G : Type*) [group G] [is_cyclic G]:
   g h : G, g * h = h * g :=
begin
  intros,
  letI := @is_cyclic.comm_group G _inst_1 _inst_2,
  apply mul_comm
end

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:54):

letI does two things: it inserts a let into the context, and it adds that new variable to the typeclass search so that mul_comm picks it up

view this post on Zulip Mario Carneiro (Jun 13 2020 at 02:54):

it is essential that it be a let and not a have so that lean can verify that the group structure on G here is defeq to the original group structure on G

view this post on Zulip Walter Moreira (Jun 13 2020 at 02:58):

Oh, I see. I guess these are the docs https://leanprover-community.github.io/mathlib_docs/tactics.html#Instance%20cache%20tactics, right? I missed that.

Thanks so much!


Last updated: May 10 2021 at 18:22 UTC