Zulip Chat Archive

Stream: general

Topic: to_additive and tags


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:22):

But bar4 is not getting the extensionality tag.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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*} [ : 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 :=  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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:37):

why is mul_mem a def?

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:38):

Because I'm a twit.

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:38):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:38):

I can dig out another example if you like.

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:38):

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

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:39):

It's possible to create a docstring for the copy

view this post on Zulip 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 _ }

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:40):

yeah, that happens

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:40):

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

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:41):

You have to transfer more things

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:41):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:42):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:42):

I have tagged things which will never ever be used.

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:42):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:43):

But then will the additive version be auto-generated?

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:43):

yes

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:43):

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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:45):

But it's still a pain.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:46):

basically we're painted into a corner by lean 3

view this post on Zulip Chris Hughes (Aug 09 2019 at 12:46):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:47):

Ha ha!

view this post on Zulip Mario Carneiro (Aug 09 2019 at 12:47):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:47):

[gets back to tagging]

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:53):

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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 12:55):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 13:04):

Thanks. I think that's everything.

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 13:05):

Thanks a lot, in fact.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Aug 09 2019 at 13:10):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 ;-)

view this post on Zulip Mario Carneiro (Aug 09 2019 at 13:44):

See group_power for examples of this

view this post on Zulip Mario Carneiro (Aug 09 2019 at 13:44):

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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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!

view this post on Zulip 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 = ma + na :=
@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