## Stream: general

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

import group_theory.submonoid

theorem foo1 (α : Type*) [monoid α] : (1 : α) = 1 := sorry

#check bar1 -- ∀ (α : Type u_1) [_inst_1 : add_monoid α], 0 = 0

theorem foo2 (α : Type*) [monoid α] : (1 : α) * 1 = 1 := sorry

#print bar2 -- no simp tag

theorem foo3 (α : Type*) [monoid α] : (1 : α) * 1 = 1 := sorry

#print bar3 -- has a simp tag

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. -/
def mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S := submonoid.mul_mem' S


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. -/
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
but is expected to have type
monoid M


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

yeah, that happens

#### 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
(carrier : set α)
(zero_mem' : (0 : α) ∈ carrier)
(add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier)



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


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

But then will the additive version be auto-generated?

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?

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 _ }


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


(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


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


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

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 :=

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