Zulip Chat Archive

Stream: general

Topic: debugging to_additive


view this post on Zulip Kevin Buzzard (Apr 27 2019 at 09:55):

I'm writing code about open subgroups. Patrick wrote the first lemma here and I wrote the second. Note: this is not a MWE, the WE is "clone the perfectoid project and try this in for_mathlib/nonarchimedean/open_subgroup" and I'm not going to minimise right now because I'm looking for techniques, not answers.

@[to_additive open_add_subgroup.is_open_of_open_add_subgroup]
lemma is_open_of_open_subgroup {s : set G} (h₁ : is_subgroup s)
  (h₂ :  U : open_subgroup G, (U : set G)  s) : is_open s :=
begin
  rw is_open_iff_forall_mem_open,
  intros x hx,
  rcases h₂ with ⟨⟨U, h₁U, h₂U, H,
  use (λ y, y * x⁻¹) ⁻¹' U,
  split,
  { intros u hu,
    erw set.mem_preimage_eq at hu,
    replace hu := H hu,
    simpa using is_submonoid.mul_mem hu hx },
  split,
  { apply continuous_mul continuous_id continuous_const,
    { exact h₁U },
    { apply_instance } },
  { erw set.mem_preimage_eq,
    simpa using is_submonoid.one_mem _,
    exact h₂U.to_is_submonoid }
end

@[to_additive open_add_subgroup.is_closed]
lemma is_closed (U : open_subgroup G) : is_closed (U : set G) :=
begin
  show is_open (-(U : set G)),
  rw is_open_iff_forall_mem_open,
  intros x hx,
  use (λ y, y * x⁻¹) ⁻¹' U,
  split,
  { intros u hux,
    erw set.mem_preimage_eq at hux,
    rw set.mem_compl_iff at hx ,
    intro hu, apply hx,
    convert is_submonoid.mul_mem (is_subgroup.inv_mem hux) hu,
    simp },
  split,
  { apply continuous_mul continuous_id continuous_const,
    { exact U.is_open },
    { apply_instance } },
  { erw set.mem_preimage_eq,
    rw mul_inv_self,
    exact is_submonoid.one_mem _ }
end

First lemma works fine. Second lemma gives error

type mismatch at application
  @open_subgroup.is_open G _inst_1
term
  _inst_1
has type
  add_group G
but is expected to have type
  group G

and my interpretation of this error is "the to_additive algorithm failed". Indeed if I comment out @[to_additive open_add_subgroup.is_closed] the error goes away.

How do I begin to debug this issue? I would prefer an answer which didn't involve bisection (i.e. attempting to prove smaller and smaller lemmas using automation) -- that's what I'm trying to avoid.

view this post on Zulip Patrick Massot (Apr 27 2019 at 10:04):

Maybe one intermediate lemma used in the proof misses a to_additive tag

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 10:06):

Right. But Lean knows which one, and yet the only way I know of for finding out for myself is by a tedious process involving lots of sublemmas half the size of the previous sublemma. Whereas Lean knows right now.

view this post on Zulip Sebastien Gouezel (Apr 27 2019 at 10:18):

Offtopic, but your first lemma's assumptions are too strong: you just need s to contain a nonempty open set.

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 10:23):

Indeed! Nice catch, thanks.

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 16:18):

OK so I debugged this by cutting and pasting the old proof and then trying to fix it and luckily I ran into the missing thing.

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 16:19):

There's no better way? I was lucky that mul_X was defined and add_X was not; if it had been defined but not given the attribute I suspect this method would have failed.

view this post on Zulip Mario Carneiro (Apr 27 2019 at 19:49):

The error actually tells you which to_additive tag is missing, if you know where to look. The error says it tried to apply open_subgroup.is_open, but it is expecting a group and it was given an add_group. That's because group got translated correctly but open_subgroup.is_open didn't. So double check that open_subgroup.is_open has a @[to_additive open_add_subgroup.is_open] annotation

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 19:53):

Yes, that was exactly the problem. I should have read the error more carefully instead of just throwing my hands in the air!

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 19:54):

We had defined open_subgroup.is_open , left a gap, and then defined open_add_subgroup.is_open and added the annotation then. Is it safe to just put the annotation before the first definition instead of after the second one? I still don't feel I quite know how these things work. We should do something with equation lemmas too, right?

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:02):

You can either write open_subgroup.is_open with a @[to_additive open_add_subgroup.is_open] annotation, and it will be generated automatically, or you can write open_subgroup.is_open and open_add_subgroup.is_open and put attribute [to_additive open_add_subgroup.is_open] open_subgroup.is_open afterwards. This will add the tag but will not create the theorem, which can be useful if the proof is not automatic for some reason

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 20:03):

But what about all of the equation lemmas etc? We also then have to tag all of these, right? this is the impression I'm getting from looking at mathlib.

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:03):

For defs, you also have to mark the equation lemmas with to_additive

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 20:03):

Right. Can't this be done automatically?

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:03):

in principle

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:04):

right now to_additive doesn't do this because it's not easy to find out when this is necessary

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:05):

Also you can't create equation lemmas manually (they have a special internal tag that isn't accessible to tactics) so it's not a perfect replica


Last updated: May 18 2021 at 16:25 UTC