# Zulip Chat Archive

## 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 @[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 (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 `def`

s, 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?

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

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