nightly-2024-03-13

Stream: nightly-testing

[Kim Morrison]

lean4#3579 should land in nightly-2024-03-13. This adds @[simp] to Nat.succ_eq_add_one.

There is a fair bit of Mathlib fallout, but it is mostly nice. The changes required are on the lean-pr-testing-3579 branch. This can be merged in nightly-testing when nightly-2024-03-13 arrives.

[Kim Morrison]

nightly-2024-03-13 has landed, and I've merged the lean-pr-testing-3579 branches into nightly-testing on both Std and Mathlib.

Whether that builds remains to be seen!

[Kim Morrison]

Also landed in nightly-2024-03-13 is a fancy new canonicalizer from Leo, that he's hooked out to omega. The recent regression with omega no longer identifying atoms up to defeq should now be fixed!

[Kim Morrison]

#11353 is the adaptation PR for nightly-2024-03-13.

[Kim Morrison]

I've created https://github.com/leanprover-community/mathlib4/issues/11357 to track an outstanding issue which seems very likely to be a Lean bug. If anyone would like to try minimizing this to a no imports example we can try to get it fixed.

[Kim Morrison]

I think besides:

• this issue
• merging #11353 after it passes CI
• dealing with any Adaptation notes

we are otherwise caught up on nightly releases.

[Kevin Buzzard]

The simp issue appears to be already present on master:

import Mathlib.Algebra.Group.Hom.Basic
import Mathlib.Algebra.GroupPower.Basic

universe uM uN uP uQ

variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}

instance MonoidHom.commMonoid [MulOneClass M] [CommMonoid N] :
    CommMonoid (M →* N) where
  mul := (· * ·)
  mul_assoc := sorry
  one := 1
  one_mul := sorry
  mul_one := sorry
  mul_comm := sorry
  npow n f :=
    { toFun := fun x => f x ^ n, map_one' := by simp, map_mul' := fun x y => by simp [mul_pow] }
  npow_zero f := sorry
  npow_succ n f := sorry


instance MonoidHom.commGroup {M G} [MulOneClass M] [CommGroup G] : CommGroup (M →* G) where
    mul := (· * ·)
    mul_assoc := sorry
    one := 1
    one_mul := sorry
    mul_one := sorry
    mul_comm := sorry
    npow n f :=
      { toFun := fun x => f x ^ n, map_one' := by simp, map_mul' := fun x y => by simp [mul_pow] }
    npow_zero f := sorry
    npow_succ n f := sorry
    inv := Inv.inv
    div := Div.div
    div_eq_mul_inv := sorry
    mul_left_inv := by intros; ext; apply mul_left_inv
    zpow := fun n f =>
      { toFun := fun x => f x ^ n,
        map_one' := sorry,
        map_mul' := sorry }
    zpow_zero' := sorry
    zpow_succ' := fun n f => by
      ext x
      simp [zpow_add_one, mul_comm] -- "unexpected bound variable #0"
    zpow_neg' := sorry

so it's not clear to me why it's relevant to nightly-testing.

[Kim Morrison]

Great, thanks @Kevin Buzzard. If you want to do anything more towards updating the issue at #11357 to reflect this, and/or minimizing, please do! At whatever point you finish, let me know and I'll see if I can continue.

[Kevin Buzzard]

It's pretty fragile though: e.g. removing the MonoidHom.commMonoid instance or the universes makes the bug vanish

[Kevin Buzzard]

It's bedtime here, I'll tinker around for bit longer and post on the issue when I give up.

[Kevin Buzzard]

OK I'm done -- I got essentially nowhere. I updated the issue.

[Kim Morrison]

Thanks!

[Kevin Buzzard]

I was surprised that I got simp only [mul_comm] to hang Lean -- maybe the same issue?

[Matthew Ballard]

Minimized Mathlib free example in the issue. Please confirm on your machine!

[Kim Morrison]

Confirmed!