# Zulip Chat Archive

## Stream: general

### Topic: to_additive and tags

#### Kevin Buzzard (Aug 09 2019 at 12:16):

import group_theory.submonoid @[to_additive bar1] theorem foo1 (α : Type*) [monoid α] : (1 : α) = 1 := sorry #check bar1 -- ∀ (α : Type u_1) [_inst_1 : add_monoid α], 0 = 0 @[to_additive bar2, simp] theorem foo2 (α : Type*) [monoid α] : (1 : α) * 1 = 1 := sorry #print bar2 -- no simp tag @[simp, to_additive bar3] theorem foo3 (α : Type*) [monoid α] : (1 : α) * 1 = 1 := sorry #print bar3 -- has a simp tag @[extensionality, to_additive bar4] theorem foo4 {α : Type*} [monoid α] {β : Type*} [monoid β] (h : α = β) : α = β := sorry #print foo4 -- has extensionality tag #print bar4 -- no extensionality tag

`to_additive`

can move `simp`

tags if they're put in the right place. Can it move extensionality tags? I just had to tag a couple of things manually, so there's an easy workaround, but it made me wonder.

#### Kevin Buzzard (Aug 09 2019 at 12:18):

Unrelated: the output of `#print`

is quite something if the lemma is tagged with the extensionality tag.

#### Mario Carneiro (Aug 09 2019 at 12:20):

The attribute list is processed in left to right order, and when the `to_additive`

attribute is called it will copy any attributes on the theorem to the additive version. So `to_additive`

should always go at the end

#### Kevin Buzzard (Aug 09 2019 at 12:22):

But `bar4`

is not getting the extensionality tag.

#### Mario Carneiro (Aug 09 2019 at 12:23):

ugh, lean core failed me again

meta def transport_with_dict (dict : name_map name) (src : name) (tgt : name) : command := copy_decl_using dict src tgt >> copy_attribute `reducible src tt tgt >> copy_attribute `simp src tt tgt >> copy_attribute `instance src tt tgt

#### Mario Carneiro (Aug 09 2019 at 12:25):

then again, there is probably a reason why it isn't copying *all* attributes on the original. For instance it would be a bad idea to copy `to_additive`

#### Kevin Buzzard (Aug 09 2019 at 12:32):

`to_additive`

is better than nothing, but it is still rather inadequate. I have got 30 definitions and theorems about submonoids with a PR which is ready to go other than the fact that I have to to-additive everything. I have namespaces and variables and it would be wonderful just to get everything working with `@[to_additive ...]`

because that way one doesn't have to write the proofs twice. But there are many obstructions to doing this. Here's an example of a definition with problems:

/-- A submonoid is closed under multiplication. -/ @[to_additive add_submonoid.add_mem] def mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S := submonoid.mul_mem' S attribute [to_additive add_submonoid.add_mem.equations._eqn_1] submonoid.mul_mem.equations._eqn_1

`to_additive`

defines `add_mem`

, but I have to manually tag `eqn_1`

. The other problem with this approach is that add_mem does not get a docstring.

Here's a worse issue; a complicated definition.

/-- A directed union of submonoids is a submonoid. -/ @[to_additive add_submonoid.Union_of_directed] def Union_of_directed {ι : Type*} [hι : nonempty ι] (s : ι → submonoid M) (directed : ∀ i j, ∃ k, s i ≤ s k ∧ s j ≤ s k) : submonoid M := { carrier := (⋃i, s i), one_mem' := let ⟨i⟩ := hι in set.mem_Union.2 ⟨i, submonoid.one_mem _⟩, mul_mem' := λ a b ha hb, let ⟨i, hi⟩ := set.mem_Union.1 ha in let ⟨j, hj⟩ := set.mem_Union.1 hb in let ⟨k, hk⟩ := directed i j in set.mem_Union.2 ⟨k, (s k).mul_mem (hk.1 hi) (hk.2 hj)⟩ }

Here `to_additive`

fails to port the theorem, and my understanding of the error is that `submonoid.Union_of_directed._match_1`

has not been tagged with `to_additive`

-- but I don't see anywhere where I have a chance to tag this. If I close the namespace now and add the additive version manually (copying and pasting the code, which in my mind already indicates something is wrong) then I have to set up all my variables again. If instead I decide to close the namespace after I've formalised all 20 lemmas/definitions then it gets to the point where even the lemmas stop working because not enough earlier stuff has been tagged. Together with the docstring issue it seems to me that currently the best way to deal with this is simply to prove a bunch of stuff in a submonoid namespace and then simply prove everything again in an add_submonoid namespace and port the proofs manually. That way I can get docstrings as well. But then I have to go through all this rigmarole of tagging all the _match and _eqn1 stuff , and, more importantly, *I never use to_additive myself at all*.

#### Kevin Buzzard (Aug 09 2019 at 12:34):

In short: it seems to me that Lean best practice is to avoid to_additive when the going gets tough.

#### Kevin Buzzard (Aug 09 2019 at 12:34):

@Cyril Cohen do you have these problems in Coq? Do you have additive groups and multiplicative groups, and a system for porting definitions / theorems in one domain to the other?

#### Kevin Buzzard (Aug 09 2019 at 12:36):

I am bundling submonoids and add_submonoids and coming to the conclusion that our infrastructure for helping is giving me literally nothing more than the fact that the work I have to do is *more* than doubled, instead of just doubled.

#### Mario Carneiro (Aug 09 2019 at 12:37):

why is `mul_mem`

a def?

#### Kevin Buzzard (Aug 09 2019 at 12:38):

Because I'm a twit.

#### Mario Carneiro (Aug 09 2019 at 12:38):

if it's a theorem there is no eqn_1 to worry about

#### Kevin Buzzard (Aug 09 2019 at 12:38):

I can dig out another example if you like.

#### Mario Carneiro (Aug 09 2019 at 12:38):

The docstring thing would be nice, but what should it say?

#### Mario Carneiro (Aug 09 2019 at 12:39):

It's possible to create a docstring for the copy

#### Kevin Buzzard (Aug 09 2019 at 12:40):

@[to_additive add_submonoid.univ] def univ : submonoid M := { carrier := set.univ, one_mem' := set.mem_univ 1, mul_mem' := λ _ _ _ _, set.mem_univ _ }

#### Kevin Buzzard (Aug 09 2019 at 12:40):

This one fails --

type mismatch at application univ._proof_1 M _inst_3 term _inst_3 has type add_monoid M but is expected to have type monoid M

#### Mario Carneiro (Aug 09 2019 at 12:40):

yeah, that happens

#### Kevin Buzzard (Aug 09 2019 at 12:40):

There's nothing I can do about this, right?

#### Mario Carneiro (Aug 09 2019 at 12:41):

You have to transfer more things

#### Kevin Buzzard (Aug 09 2019 at 12:41):

What do you mean? I have transferred everything up unto this point I think.

#### Kevin Buzzard (Aug 09 2019 at 12:41):

/-- A submonoid of a monoid α is a subset containing 1 and closed under multiplication. -/ structure submonoid (α : Type*) [monoid α] := (carrier : set α) (one_mem' : (1 : α) ∈ carrier) (mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier) /-- An additive submonoid of an additive monoid α is a subset containing 0 and closed under addition. -/ structure add_submonoid (α : Type*) [add_monoid α] := (carrier : set α) (zero_mem' : (0 : α) ∈ carrier) (add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier) attribute [to_additive add_submonoid] submonoid attribute [to_additive add_submonoid.carrier] submonoid.carrier attribute [to_additive add_submonoid.cases_on] submonoid.cases_on attribute [to_additive add_submonoid.has_sizeof_inst] submonoid.has_sizeof_inst attribute [to_additive add_submonoid.mk] submonoid.mk attribute [to_additive add_submonoid.mk.inj] submonoid.mk.inj attribute [to_additive add_submonoid.mk.inj_arrow] submonoid.mk.inj_arrow attribute [to_additive add_submonoid.mk.inj_eq] submonoid.mk.inj_eq attribute [to_additive add_submonoid.mk.sizeof_spec] submonoid.mk.sizeof_spec attribute [to_additive add_submonoid.add_mem'] submonoid.mul_mem' attribute [to_additive add_submonoid.no_confusion] submonoid.no_confusion attribute [to_additive add_submonoid.no_confusion_type] submonoid.no_confusion_type attribute [to_additive add_submonoid.zero_mem'] submonoid.one_mem' attribute [to_additive add_submonoid.rec] submonoid.rec attribute [to_additive add_submonoid.rec_on] submonoid.rec_on attribute [to_additive add_submonoid.sizeof] submonoid.sizeof

#### Kevin Buzzard (Aug 09 2019 at 12:42):

I have been doing this extremely anally, trying to get the system to work.

#### Kevin Buzzard (Aug 09 2019 at 12:42):

I have tagged things which will never ever be used.

#### Mario Carneiro (Aug 09 2019 at 12:42):

Oh, I see, you have to do an after the fact annotation

#### Mario Carneiro (Aug 09 2019 at 12:43):

like this one

def left_rel [group α] (s : set α) [is_subgroup s] : setoid α := ⟨λ x y, x⁻¹ * y ∈ s, assume x, by simp [is_submonoid.one_mem], assume x y hxy, have (x⁻¹ * y)⁻¹ ∈ s, from is_subgroup.inv_mem hxy, by simpa using this, assume x y z hxy hyz, have x⁻¹ * y * (y⁻¹ * z) ∈ s, from is_submonoid.mul_mem hxy hyz, by simpa [mul_assoc] using this⟩ attribute [to_additive quotient_add_group.left_rel._proof_1] left_rel._proof_1 attribute [to_additive quotient_add_group.left_rel] left_rel attribute [to_additive quotient_add_group.left_rel.equations._eqn_1] left_rel.equations._eqn_1

#### Kevin Buzzard (Aug 09 2019 at 12:43):

But then will the additive version be auto-generated?

#### Mario Carneiro (Aug 09 2019 at 12:43):

yes

#### Mario Carneiro (Aug 09 2019 at 12:43):

you just have to make sure to tag `foo._proof_1`

before you tag `foo`

#### Kevin Buzzard (Aug 09 2019 at 12:44):

Why am I being left to discover these things myself? [because nobody wrote the docs I guess]

#### Mario Carneiro (Aug 09 2019 at 12:44):

I agree that tagging new structures is horrible, because lean generates a ton of definitions and doesn't let user code know what it did

#### Kevin Buzzard (Aug 09 2019 at 12:45):

I just run `#print prefix`

after everything. I have been writing the code in emacs because I can automate much of the procedure which does all the post hoc tagging.

#### Kevin Buzzard (Aug 09 2019 at 12:45):

But it's still a pain.

#### Mario Carneiro (Aug 09 2019 at 12:46):

I tried setting up `to_additive`

so that it would copy everything in the namespace, but this turns out to be really slow because there is no index for that so you have to basically go through every definition in the environment to find which ones were added just a few lines ago

#### Mario Carneiro (Aug 09 2019 at 12:46):

basically we're painted into a corner by lean 3

#### Chris Hughes (Aug 09 2019 at 12:46):

Is it slower than a human copying everything in the namespace?

#### Kevin Buzzard (Aug 09 2019 at 12:47):

Ha ha!

#### Mario Carneiro (Aug 09 2019 at 12:47):

we might be able to do it with a hole command?

#### Kevin Buzzard (Aug 09 2019 at 12:47):

[gets back to tagging]

#### Kevin Buzzard (Aug 09 2019 at 12:51):

/-- `univ` is the submonoid M of the monoid M -/ def univ : submonoid M := { carrier := set.univ, one_mem' := set.mem_univ 1, mul_mem' := λ _ _ _ _, set.mem_univ _ } attribute [to_additive add_submonoid.univ._proof_1] submonoid.univ._proof_1 attribute [to_additive add_submonoid.univ._proof_2] submonoid.univ._proof_2 attribute [to_additive add_submonoid.univ] submonoid.univ attribute [to_additive add_submonoid.univ.equations._eqn_1] submonoid.univ.equations._eqn_1

So this does work and the additive version is indeed auto-generated; I hadn't understood that I could do that after the fact. Now how do I do the docstring?

#### Kevin Buzzard (Aug 09 2019 at 12:53):

#check submonoid.univ -- hover to see docstring #check add_submonoid.univ -- works but no docstring

#### Kevin Buzzard (Aug 09 2019 at 12:55):

[The point here is that the attributes have to be set in the right order]

#### Kevin Buzzard (Aug 09 2019 at 13:02):

Before:

attribute [to_additive add_submonoid.Union_of_directed] submonoid.Union_of_directed attribute [to_additive add_submonoid.Union_of_directed._match_1] submonoid.Union_of_directed._match_1 attribute [to_additive add_submonoid.Union_of_directed._match_1.equations._eqn_1] submonoid.Union_of_directed._match_1.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._match_2] submonoid.Union_of_directed._match_2 attribute [to_additive add_submonoid.Union_of_directed._match_2.equations._eqn_1] submonoid.Union_of_directed._match_2.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._match_3] submonoid.Union_of_directed._match_3 attribute [to_additive add_submonoid.Union_of_directed._match_3.equations._eqn_1] submonoid.Union_of_directed._match_3.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._match_4] submonoid.Union_of_directed._match_4 attribute [to_additive add_submonoid.Union_of_directed._match_4.equations._eqn_1] submonoid.Union_of_directed._match_4.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._proof_1] submonoid.Union_of_directed._proof_1 attribute [to_additive add_submonoid.Union_of_directed.equations._eqn_1] submonoid.Union_of_directed.equations._eqn_1

(auto-generated by emacs, with added errors)

#### Mario Carneiro (Aug 09 2019 at 13:02):

That requires modifying the `to_additive`

code. If you want to write a docstring rather than have an autogenerated one, there is some `run_cmd`

thing you can do

#### Kevin Buzzard (Aug 09 2019 at 13:03):

Yeah I'm happy to do the run_cmd. It's been mentioned before. In some sense I am trying to write a "best practice" to_additive thing here. I've noticed looking through other people's code in mathlib that there are others who don't know all the tricks either.

#### Mario Carneiro (Aug 09 2019 at 13:04):

def foo := ℕ run_cmd tactic.add_doc_string `foo "*This* is a docstring for `foo`." #print foo

#### Kevin Buzzard (Aug 09 2019 at 13:04):

Thanks. I think that's everything.

#### Kevin Buzzard (Aug 09 2019 at 13:05):

Thanks a lot, in fact.

#### Kevin Buzzard (Aug 09 2019 at 13:07):

After:

attribute [to_additive add_submonoid.Union_of_directed._match_1] submonoid.Union_of_directed._match_1 attribute [to_additive add_submonoid.Union_of_directed._match_2] submonoid.Union_of_directed._match_2 attribute [to_additive add_submonoid.Union_of_directed._match_3] submonoid.Union_of_directed._match_3 attribute [to_additive add_submonoid.Union_of_directed._match_4] submonoid.Union_of_directed._match_4 attribute [to_additive add_submonoid.Union_of_directed._proof_1] submonoid.Union_of_directed._proof_1 attribute [to_additive add_submonoid.Union_of_directed] submonoid.Union_of_directed attribute [to_additive add_submonoid.Union_of_directed._match_1.equations._eqn_1] submonoid.Union_of_directed._match_1.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._match_2.equations._eqn_1] submonoid.Union_of_directed._match_2.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._match_3.equations._eqn_1] submonoid.Union_of_directed._match_3.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed._match_4.equations._eqn_1] submonoid.Union_of_directed._match_4.equations._eqn_1 attribute [to_additive add_submonoid.Union_of_directed.equations._eqn_1] submonoid.Union_of_directed.equations._eqn_1

You just keep looking at the first error, see what Lean is complaining about, find the corresponding line and then move it above where the error was. I cannot guarantee that this terminates in general but it's just terminated for this complicated lemma so that's a positive sign.

#### Kevin Buzzard (Aug 09 2019 at 13:08):

I will remark that whilst the answer clearly has some structure, the moves taken to get there were match 1, match 4, proof 1, match 3, match 2 (or something -- I'm doing this from memory; it works now and I'm not going back)

#### Kevin Buzzard (Aug 09 2019 at 13:10):

Oh cool, you can really confuse VS Code by editing an open file in emacs ;-)

#### Kevin Buzzard (Aug 09 2019 at 13:14):

dammit now I'm back to doing emacs command line shortcuts in VS Code :-/ It took me months to shake this off the first time around...

#### Kevin Buzzard (Aug 09 2019 at 13:29):

attribute [to_additive add_monoid.mul._main] monoid.pow._main attribute [to_additive add_monoid.mul] monoid.pow attribute [to_additive add_monoid.has_mul] monoid.has_pow attribute [to_additive multiples._proof_1] powers._proof_1 attribute [to_additive multiples._proof_2] powers._proof_2

Thanks a bunch, other people.

#### Kevin Buzzard (Aug 09 2019 at 13:30):

I'm quite getting into this :-) Someone could write a script to figure out which attributes are missing. There's just some dictionary monoid->add_monoid, powers->multiples, mul->add etc and then you scan every namespace and try and spot what's missing.

#### Kevin Buzzard (Aug 09 2019 at 13:34):

@[to_additive add_submonoid.multiples.self_mem] lemma powers.self_mem {x : M} : x ∈ powers x := ⟨1, pow_one _⟩ /- type mismatch at application 0 term nat.has_one has type has_one ℕ but is expected to have type has_zero ℕ -/

*d'oh* Lean -- don't change _that_ 1!

#### Kevin Buzzard (Aug 09 2019 at 13:38):

This one has me stumped. The algorithm fails, and it is not unreasonable that it fail because how is Lean supposed to know which 1's to change to 0's and which ones not to change? We're proving x^1=x here and I want that translated into 1*x=x for the additive thing but the translation fails. So now I have to write `add_monoid.multiples.self_mem`

myself, but if I don't do it now then maybe the next thing will fail, and if I do do it now then I have to close the namespace, open a new one, set up some variables, prove the lemma, close it and then open the old one. Thank goodness for `#where`

;-)

#### Mario Carneiro (Aug 09 2019 at 13:44):

See `group_power`

for examples of this

#### Mario Carneiro (Aug 09 2019 at 13:44):

We just don't use `to_additive`

to define the copy in this case

#### Mario Carneiro (Aug 09 2019 at 13:45):

Notice also that `x^1`

and `1*x`

are not even written in the same order, `to_additive`

can't handle that kind of thing

#### Kevin Buzzard (Aug 09 2019 at 13:47):

/-- x is in the submonoid generated by x. -/ lemma powers.self_mem {x : M} : x ∈ powers x := ⟨1, pow_one _⟩ end submonoid /-- x is in the add_submonoid generated by x. -/ lemma add_submonoid.multiples.self_mem {M : Type*} [add_monoid M] {x : M} : x ∈ add_submonoid.multiples x := ⟨1, add_monoid.one_smul x⟩ attribute [to_additive add_submonoid.multiples.self_mem] submonoid.powers.self_mem namespace submonoid variables {M : Type*} [monoid M] (S : submonoid M)

[grumble]

#### Kevin Buzzard (Aug 09 2019 at 13:53):

See

`group_power`

for examples of this

Aah -- so it was you who didn't to_additive `monoid.has_pow`

!

#### Kevin Buzzard (Aug 09 2019 at 13:54):

theorem pow_add (a : α) (m n : ℕ) : a^(m + n) = a^m * a^n := by induction n with n ih; [rw [add_zero, pow_zero, mul_one], rw [pow_succ, ← pow_mul_comm', ← mul_assoc, ← ih, ← pow_succ']]; refl theorem add_monoid.add_smul : ∀ (a : β) (m n : ℕ), (m + n)•a = m•a + n•a := @pow_add (multiplicative β) _ attribute [to_additive add_monoid.add_smul] pow_add

Aah I see. So the point is that you just try and port the proofs using `multiplicative`

in this case.

Last updated: May 11 2021 at 13:22 UTC