## Stream: general

### Topic: debugging to_additive

#### 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

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
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 (Apr 27 2019 at 10:04):

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

#### 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.

#### 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.

#### Kevin Buzzard (Apr 27 2019 at 10:23):

Indeed! Nice catch, thanks.

#### 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.

#### 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.

#### 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

#### 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!

#### 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?

#### 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

#### 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.

#### Mario Carneiro (Apr 27 2019 at 20:03):

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

#### Kevin Buzzard (Apr 27 2019 at 20:03):

Right. Can't this be done automatically?

in principle

#### 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

#### 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