Fix bad diamond via forgetting data in MIL Chapter7

Stream: new members

[Shanghe Chen]

Hi I am quite confused in how adding nsmul to AddMonoid₄:

  /-- Multiplication by a natural number. -/
  nsmul : ℕ → M → M := nsmul₁
  /-- Multiplication by `(0 : ℕ)` gives `0`. -/
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
  nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl

instance mySMul {M : Type} [AddMonoid₄ M] : SMul ℕ M := ⟨AddMonoid₄.nsmul⟩

solves the bad diamond problem

[Shanghe Chen]

In https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html with AddMonoid3 there are two instances of the ring Z:

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
  smul := fun r s ↦ r*s
  zero_smul := zero_mul
  one_smul := one_mul
  mul_smul := mul_assoc₃
  add_smul := Ring₃.right_distrib
  smul_add := Ring₃.left_distrib

instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
  smul := zsmul₁
  zero_smul := sorry
  one_smul := sorry
  mul_smul := sorry
  add_smul := sorry
  smul_add := sorry

[Shanghe Chen]

But the corresonding content for AddMonoid₄ only defines and shows that:

instance : AddMonoid₄ ℤ where
  add := (· + ·)
  add_assoc₃ := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  nsmul := fun n m ↦ (n : ℤ) * m
  nsmul_zero := Int.zero_mul
  nsmul_succ := fun n m ↦ show (n + 1 : ℤ) * m = m + n * m
    by rw [Int.add_mul, Int.add_comm, Int.one_mul]

example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl

How is the example relavant to bad diamond?

[Patrick Massot]

Maybe I should be more explicit and include the code that doesn’t work:

instance myBadSMul {M : Type} [AddMonoid₃ M] : SMul ℕ M := ⟨nsmul₁⟩

example (n : ℕ) (m : ℤ) : SMul.smul (self := myBadSMul) n m = n * m := rfl

[Patrick Massot]

This is endowing every additive monoid with a scalar multiplication by natural numbers instead of including this data in the definition of additive monoid, and it ruins the rfl.

[Shanghe Chen]

Yeah this code for AddMonoid₃ corresponding the example of AddMonoid₄. Hence it solved it by "override" the default implementation (i.e., nsmul₁) for AddMonoid₄?

[Shanghe Chen]

I was thinking defining Module₂ and two instances selfModule2 and abGrpModule2, and checking they are the same before. But it's more complicated than the example supplied here :blush:

[Patrick Massot]

Yes the AddMonoid₄ ℤ instance overrides the default implementation.

[Patrick Massot]

Could you please open an issue on the MIL source repo so that I don’t forget to add the explicit bad code? I really don’t have time now but I will do it later.

[Shanghe Chen]

Sure, I will open an issue in https://github.com/avigad/mathematics_in_lean_source

[Shanghe Chen]

It's kind of solving the bad diamond problem via avoiding it. Since they are definitionally equal, hence I understand that they can be proved the same by rfl now. What is the advantage of this way over proving that they are equal not using rfl?

[Matthew Ballard]

Lots of automation in the system relies on definitional equality (eg rfl works). Propositional equality is much less useful in this way

[Shanghe Chen]

I think I am kind of getting it now. Thank you very much Patrick and Matthew :tada:

[Shanghe Chen]

Could you please open an issue on the MIL source repo so that I don’t forget to add the explicit bad code? I really don’t have time now but I will do it later.

A issue created here linking this thread

[Eric Rodriguez]

Matthew Ballard said:

Lots of automation in the system relies on definitional equality (eg rfl works). Propositional equality is much less useful in this way

Could we possibly add a "meta" instance search that instead looks up proofs that these equalities are true? Could also speed up the system by making sure that any rfls are cached effectively

[Matthew Ballard]

You mean in type class synthesis or more generally?

[Eric Rodriguez]

Within typeclass synthesis is where I imagined this

[Matthew Ballard]

I just learned yesterday that typeclass synthesis starts off filtering the list of instances by matching on a key in a discrimination tree. So we aren’t even getting to unification before some things are tossed for performance reasons.