to_additive and tags

Stream: general

[Kevin Buzzard]

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]

Unrelated: the output of #print is quite something if the lemma is tagged with the extensionality tag.

[Mario Carneiro]

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]

But bar4 is not getting the extensionality tag.

[Mario Carneiro]

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]

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]

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]

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

[Kevin Buzzard]

@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]

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]

why is mul_mem a def?

[Kevin Buzzard]

Because I'm a twit.

[Mario Carneiro]

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

[Kevin Buzzard]

I can dig out another example if you like.

[Mario Carneiro]

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

[Mario Carneiro]

It's possible to create a docstring for the copy

[Kevin Buzzard]

@[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]

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]

yeah, that happens

[Kevin Buzzard]

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

[Mario Carneiro]

You have to transfer more things

[Kevin Buzzard]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

I have tagged things which will never ever be used.

[Mario Carneiro]

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

[Mario Carneiro]

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]

But then will the additive version be auto-generated?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

But it's still a pain.

[Mario Carneiro]

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]

basically we're painted into a corner by lean 3

[Chris Hughes]

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

[Kevin Buzzard]

Ha ha!

[Mario Carneiro]

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

[Kevin Buzzard]

[gets back to tagging]

[Kevin Buzzard]

/-- `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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

def foo := ℕ

run_cmd tactic.add_doc_string `foo "*This* is a docstring for `foo`."

#print foo

[Kevin Buzzard]

Thanks. I think that's everything.

[Kevin Buzzard]

Thanks a lot, in fact.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

@[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]

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]

See group_power for examples of this

[Mario Carneiro]

We just don't use to_additive to define the copy in this case

[Mario Carneiro]

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]

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

See group_power for examples of this

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

[Kevin Buzzard]

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.