to_additive align failures

Stream: mathlib4

[Johan Commelin]

Thanks to Mario:

import Mathlib

open Lean

#eval show MetaM _ from do
  let m := Mathlib.Prelude.Rename.getRenameMap (← getEnv)
  for (fr, to') in ToAdditive.translations.getState (← getEnv) do
    match m.toLean3.contains fr, m.toLean3.contains to' with
    | true, false => println! "❌ {to'} <- ✅ {fr}"
    | false, true => println! "❌ {fr} -> ✅ {to'}"
    | _, _ => pure ()

[Johan Commelin]

Output: https://gist.github.com/jcommelin/1299f6a0b10e823c96bb251902f209ef

[Johan Commelin]

I think that together with mathlib3, we can auto-generate the missing #align statements

[Johan Commelin]

:check: Con.instPowQuotientToMulToMulOneClassNat -> :cross_mark: AddCon.Quotient.nsmul

How did that ever become a to_additive pair?

[Mario Carneiro]

actually the :cross_mark: is on the left in both cases

[Mario Carneiro]

the arrow indicates which one is the multiplicative and which is the additive

[Johan Commelin]

oops, contravariance is hard

[Johan Commelin]

Fixed the code above, and updated the gist

[Johan Commelin]

!4#1816 fixes 1020 of these

[Reid Barton]

merge conflict already :)

[Johan Commelin]

Fixed

[Reid Barton]

Is it ready for review?

[Johan Commelin]

I think so.

[Johan Commelin]

Let's find out whether CI agrees

[Reid Barton]

How automatically-generated is this PR? Maybe it would be better to proceed with !4#1502 first?

[Johan Commelin]

It is pretty automatically generated

[Reid Barton]

oh, 1502 is actually not as big as I feared

[Johan Commelin]

I'm fixing its conflicts

[Reid Barton]

On 1502, or 1816?

[Johan Commelin]

1502

[Reid Barton]

OK, I will look over 1816 then.

[Johan Commelin]

@Reid Barton !4#1502 is mergable without conflicts

[Reid Barton]

I'm lost

[Reid Barton]

Are we merging 1502 first, or 1816?

[Johan Commelin]

I think 1502

[Johan Commelin]

Because afaik it's ready to go

[Reid Barton]

Presumably 1816 will have merge conflicts after that, and you will fix them?

[Johan Commelin]

Yeps

[Reid Barton]

I'm going to merge master into 1502 manually first, I don't really trust what github thinks

[Reid Barton]

Because I think I probably modified some of the Lean 3 names in these #align statements.
So for reviewing at least it would be good to be looking at the correct thing

[Reid Barton]

Right so now the first diff is

-@[to_additive (attr := simp)]
+-- todo: should nat power be called `nsmul` here?
+@[to_additive (attr := simp) smul_right]
 theorem pow_right (h : Commute a b) (n : ℕ) : Commute a (b ^ n) :=
   SemiconjBy.pow_right h n
 #align commute.pow_right Commute.pow_rightₓ
 #align add_commute.nsmul_right AddCommute.smul_rightₓ
 -- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

[Reid Barton]

I assume we actually want the name AddCommute.nsmul_right now

[Reid Barton]

OK, then I will try to update these

[Johan Commelin]

@Reid Barton I'm confused. When I locally try to merge master, I don't get any conflicts.

[Reid Barton]

Indeed there are no conflicts as detected by git

[Johan Commelin]

Ooh, ok

[Reid Barton]

but there are logical conflicts

[Johan Commelin]

gotcha

[Reid Barton]

e.g. why have add_commute.nsmul_right translated to AddCommute.smul_right

[Johan Commelin]

yes, understood. I should have stared at the diff a bit more

[Reid Barton]

OK I think I updated 1502, though there's a chance of a build failure

[Johan Commelin]

I think/hope that !4#1816 now compiles

[Johan Commelin]

I discovered some to_additive clashes that already exist in ml3.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/b69c9a770ecf37eb21f7b8cf4fa00de3b62694ec/src/algebra/order/hom/basic.lean#L118
clashes with the decl above it.
The two decls below it also clash.

[Johan Commelin]

Pushed more fixes

[Reid Barton]

@Floris van Doorn do you have anything to add to !4#1502? I think it is ready to go

[Reid Barton]

I added a note to "nat smul lemmas" that were called smul in mathlib3 to rename them.

I think these were bad guesses by porters, and in most cases the lemmas were really called nsmul in mathlib3 as well.

[Floris van Doorn]

I'm happy for it to be merged, I'm still catching up on the rest of this thread.

[Floris van Doorn]

It seems good to fix all the names that I marked. I was just being conservative.

[Reid Barton]

OK, the rest of this thread is really unrelated, except that it will probably have merge conflicts.

[Reid Barton]

I put 1502 on the queue then.

[Floris van Doorn]

I updated the commit message of !4#1502

[Floris van Doorn]

Johan Commelin said:

I discovered some to_additive clashes that already exist in ml3.

Sometimes you have two operations in a lemma statement that each can be multiplicative or additive independently of each other, which gives 4 possible lemmas. However, additivizing any of them will give you the "fully additive" one, so multiple multiplicative lemmas can have the same additivized version. I think this is probably usefully used in some places of mathlib3.

[Floris van Doorn]

I delegated !4#1816 btw, but you should merge with master first after !4#1502 is merged