Algebra.Group.Opposite

Stream: mathlib4

[Matej Penciak]

I think I've gotten the PR for this file (mathlib4#912) to a best place I can get it, but I think the remaining issues that prevent it from compiling are a little over my head:

1) At the to_additive declaration for the DivInvMonoid instance, Lean has a pretty spooky error:

(kernel) invalid projection
  inst✝.1

This leads to the next few to_additive instances failing as well, with other unknown constant errors.

2) In the AddHom.mulOp, AddMonoidHom.mulOp, and AddEquiv.mulOp the proofs of left_inv and right_inv complain that there are no relevant ext lemmas here, here, and here... My hypothesis is that this might be because of some issue between the interaction of the to_additive and extattributes.

In Lean 3, trace.ext says that it's using add_hom.ext, which is a to_additive version of mul_hom.ext which exists, and is tagged with ext in Lean 4 here. In fact I can get the proofs to work by applying the relevant ext lemmas by hand, for example

...
  left_inv f := by
    apply AddMonoidHom.ext
    intro
    simp [MulOpposite.op, MulOpposite.unop]
    rfl

(though it's kind of interesting that just apply <ext lemma> ; simp doesn't work by itself, unlike the original proofs)

Beyond things that are preventing the file from compiling, there were a few recurring mathport issues/changes in tactic behavior that I've noticed, and I wanted to touch on them as well:

1) Even though there's a
#align function.injective.add_semigroup Function.Injective.addSemigroup
mathport still translated unop_injective.add_semigroup to unop_injective.AddSemiGroup. Not sure if I should expect anything else, or if some #aligns aren't triggering?

2) Mathport had a lot of issues with instance names, so I had to do a lot of MulOpposite.semigroup -> instSemigroupMulOpposite translations by hand. Is there a way of aligning instance declarations to make this easier in the future? (Or is it bad practice to even refer to an instance by name? It seems wrong)

3) There were a few places in the Lean 3 file which were placed in the root namespace explicitly (_root_.semiconj_by_op for example). But mathport lost the _root_ in translation, and placed the lemmas in the wrong namespace as a result.

4) There were a few situations where the Lean 3 proof could finish with a rw or a simp, but I had to add in an extra rfl at the end. I think I've seen this brought up in other threads, but I wanted to make sure I didn't do anything wrong.

Finally, a small divergence between Lean 3 and Lean 4's way of dealing with namespaces:

MWE

def foo.num := 5

def bar.num := 6

open bar

def foo.add (x) := x + num

In Lean 4 the num in foo.add gets resolved to foo.num, but in Lean 3 (in the equivalent file) the num in foo.addgets resolved to bar.num.

This caused a bunch of places where I had to explicitly add in the fully qualified name of a symbol (MulOpposite.op and MulOpposite.unop) because there was already an op and unop in the namespace (MulHom.op for example).

Sorry for the long message, but a lot of stuff came up in this file and I wanted to get feedback about it!

[Jon Eugster]

2) It seems that MulOpposite.semigroup is the desired instance name, so that seems ok, or not? See Zulip discussion

[Floris van Doorn]

1) I haven't fully tracked down the to_additive issue, but it is caused by using the default field for div in this function.
Adding div := fun x y => x * y⁻¹ will make the error go away.
I expect that the elaborator for these default fields is creating a term that is non-standard in some way (that maybe we have to special-case in to_additive).

[Floris van Doorn]

I opened #939 to track the issue

[Chris Hughes]

There are to_additive problems in the Port of Algebra.Order.LatticeGroup. Are these related?

[Floris van Doorn]

link to PR/branch/file?

[Floris van Doorn]

mathlib4#934

[Floris van Doorn]

Looking at the error on Github, that looks unrelated. It looks like a missing @[to_additive] attribute, or a bug in the implementation of how to_additive deals with internally generated lemmas.

[Floris van Doorn]

There indeed seems to be a auxiliary generated lemma Mathlib.Algebra.Order.Group.Defs._auxLemma.5 that is not additivized.
Interestingly, this declaration does not exist at the bottom of the file Algebra.Order.Group.Defs, despite what the name suggests...
You can check this yourself using

open Lean Meta Elab Command
run_cmd liftCoreM <| do
  let env ← getEnv
  let nm : Name := .mkNum `Mathlib.Algebra.Order.Group.Defs._auxLemma 5
  let d := env.find? nm
  logInfo m!"{d.isSome}"

(this maybe needs import Mathlib.Tactic.RunCmd)
I'm wondering if this is because when we apply to_additive to a declaration where the additive version already exists.
I don't have any time anymore today to investigate further. I'll try again next week (or maybe this weekend).

[Mario Carneiro]

This might have to do with the fact that equation lemmas are no longer generated eagerly, which means that they can end up getting created in downstream files when simp wants to use the definition

[Mario Carneiro]

I recall discussing this a while ago and I think we need to implement and enable an option to autogenerate definitional equations eagerly in all of mathlib

[Mario Carneiro]

but this is an interesting issue caused by it, it was supposed to be only a performance concern

[Matej Penciak]

I can add the div := fun x y => x * y⁻¹ to fix the to_additive issue and add a porting note for now.

Any thoughts on the other observations?

• Issues with the interaction between ext and to_additive
• aligning instance names
• Divergence in behavior between Lean 3 and Lean 4 namespaces

And then mathport issues

• Aligning instance names
• Dropping _root_

Sorry the original message was so long, I just didn't want to make a new stream for each issue I encountered in the file.

[Kevin Buzzard]

The divergence in behaviour between Lean 3 and Lean 4 namespaces is well-known and intentional. I opened mathlib4#950 to track the ext v to_additive issue.

[Floris van Doorn]

Issue 1 is fixed in mathlib4#952

[Floris van Doorn]

I investigated the issue in LatticeGroup.
Whenever you tag an iff with @[simp], an auxiliary declaration is added to the environment that is the same lemma but with = instead of iff. This auxiliary declaration is used by simp to rewrite.
So if you tag something with @[simp, to_additive] we do get both of these auxiliary declarations, but they are not related to each other by the to_additive dictionary (so we don't translate the multiplicative one to the additive one).
The interface for simp (in the form of addSimpTheorem) is not giving too much information about the simp lemmas it added, but I'll try to find a hacky fix.

[Floris van Doorn]

Mario Carneiro said:

This might have to do with the fact that equation lemmas are no longer generated eagerly, which means that they can end up getting created in downstream files when simp wants to use the definition

The implementation of @[to_additive] does generate the equation lemmas for everything involved with @[to_additive] eagerly, by running

  let srcEqns? ← MetaM.run' (getEqnsFor? src true)
  let tgtEqns? ← MetaM.run' (getEqnsFor? tgt true)

and then translating from the former to the latter.

[Floris van Doorn]

The best solution I can find is to replace @[simp, to_additive] by @[to_additive (attr := simp)] from now on. If we do that, we can go a little bit into the internals of the simp attribute to see what auxiliary simp lemmas are generated for the multiplicative and additive versions of the lemmas, and insert a translation between them.

This has an additional advantage if we do the same for all other attributes so that we also write e.g. @[to_additive (attr := ext)]. Then we don't have to copy attributes from the multiplicative version to the additive version anymore (the hard part of that is figuring out which attributes were given to the multiplicative version).

Maybe it's even possible to use the attribute parser to parse the arguments of other attributes, but that might be tricky.