regression in rw

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Data.Nat.Basic

example {a b : ℕ} : (a + 1) * b = a * b + b :=
  by rw [add_one_mul]

This rewrite fails, with errors

RwError.lean:4:9
failed to synthesize instance
  RightDistribClass ?m.180
RwError.lean:4:9
tactic 'rewrite' failed, equality or iff proof expected
  ?m.258
ab: ℕ
⊢ (a + 1) * b = a * b + b

I'm aware this is fixable with (α := ℕ) or specifying a, but this still seems undesired to me. Further, this works in Lean 3, and I'm not aware of anything in the documentation which explains why this rewrite should fail. For the sake of reference, docs4#add_one_mul

[Eric Wieser]

(and docs3#add_one_mul)

[Eric Wieser]

This looks fairly easy to minimize into a mathlib-free mwe (#mfmwe?) and open an issue about

[Bhavik Mehta]

I'm having a bit of trouble doing this - can anyone help out?

[Scott Morrison]

Having a look now.

[Scott Morrison]

set_option autoImplicit true

section Mathlib.Init.ZeroOne

class One (α : Type) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

end Mathlib.Init.ZeroOne

section Mathlib.Algebra.Group.Defs

class MulOneClass (M : Type) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a

export MulOneClass (one_mul)

end Mathlib.Algebra.Group.Defs

section Mathlib.Algebra.Ring.Defs

class Distrib (R : Type) extends Mul R, Add R where
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

class RightDistribClass (R : Type) [Mul R] [Add R] : Prop where
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

instance Distrib.rightDistribClass (R : Type) [Distrib R] : RightDistribClass R :=
  ⟨Distrib.right_distrib⟩

theorem add_mul [Mul R] [Add R] [RightDistribClass R] (a b c : R) :
    (a + b) * c = a * c + b * c :=
  RightDistribClass.right_distrib a b c

theorem add_one_mul [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
    (a + 1) * b = a * b + b := by
  rw [add_mul, one_mul]

class Semiring (R : Type) extends Distrib R, MulOneClass R

end Mathlib.Algebra.Ring.Defs

section Mathlib.Data.Nat.Basic

instance : Semiring Nat where
  add := Nat.add
  mul := Nat.mul
  one := Nat.succ Nat.zero
  one_mul := sorry
  right_distrib := sorry

end Mathlib.Data.Nat.Basic

#synth MulOneClass Nat       -- works
#synth RightDistribClass Nat -- works

example {a b : Nat} : (a + 1) * b = a * b + b :=
  have := add_one_mul a b -- works
  by rw [add_one_mul]     -- failed to synthesize instance: RightDistribClass ?m

[Bhavik Mehta]

Did an issue ever get made for this? I just ran into it again :/

[Bhavik Mehta]

I've managed to hit this again in a third situation! Here's an issue for it: https://github.com/leanprover/lean4/issues/2736

[Thomas Murrills]

I think you might have linked a different recent rw issue by mistake—I think you want lean4#2736 :)

[Bhavik Mehta]

Thomas Murrills said:

I think you might have linked a different recent rw issue by mistake—I think you want lean4#2736 :)

Oops, you're right, thanks!