debugging to_additive

Stream: general

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Kevin Buzzard]

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.

[Sebastien Gouezel]

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

[Kevin Buzzard]

Indeed! Nice catch, thanks.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

Right. Can't this be done automatically?

[Mario Carneiro]

in principle

[Mario Carneiro]

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

[Mario Carneiro]

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