invalid projection on irreducible structures

Stream: lean4

[Jun Yoshida]

The following produces an error message (I am sorry its a bit long; I couldn't minimize it more):

class LeftDistribHMul (α β γ : Type _) [Add β] [Add γ] [HMul α β γ] where
  left_distrib : ∀ (a : α) (b₁ b₂ : β), a * (b₁ + b₂) = a * b₁ + a * b₂

instance : LeftDistribHMul Nat Nat Nat where
  left_distrib l m n := Nat.mul_add l m n

def Whole (α : Type _) : Type _ := {a : α // a = a}

namespace Whole

variable {α β γ: Type _}

instance [HMul α β γ] : HMul (Whole α) (Whole β) (Whole γ) where
  hMul a b := Subtype.mk (a.1 * b.1) rfl

instance [Add α] : Add (Whole α) where
  add a₁ a₂ := Subtype.mk (a₁.1 + a₂.1) rfl

theorem left_distrib
  [Add β] [Add γ] [HMul α β γ] [LeftDistribHMul α β γ]
  (a : Whole α) (b₁ b₂ : Whole β) : a * (b₁ + b₂) = a * b₁ + a * b₂ :=
  Subtype.eq <| LeftDistribHMul.left_distrib a.1 b₁.1 b₂.1

end Whole

attribute [irreducible] Whole

class LeftDistribMul (α : Type _) [Add α] [Mul α] where
  left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c

variable {α : Type _}

instance [Mul α] : Mul (Whole α) := ⟨HMul.hMul⟩

instance : LeftDistribMul (Whole Nat) where
  left_distrib x y z :=
    Whole.left_distrib x y z -- invalid projection (x * y).1

The error goes away if either

• remove attribute [irreducible] Whole line, or
• replace the proof by by rw [Whole.left_distrib]

[Jun Yoshida]

Why does isDefEq not go beyond the irreducibility?

[Eric Wieser]

Jun Yoshida said:

Why does isDefEq not go beyond the irreducibility?

This is the whole point of irreducibility!

[Jun Yoshida]

Hmm, right. Does it mean the error in this example is expected?

[Sebastian Ullrich]

I didn't look at the example in detail but changing reducibility between instance declaration and use is highly problematic; don't do it. Same goes for [simp] etc.

[Jun Yoshida]

You mean attribute [irreducible] X should not be anywhere other than just after the declaration of X?

[Kevin Buzzard]

That is indeed what they mean. In mathlib3 we used to do this all the time: define a thing, make the API, and then make the thing irreducible afterwards. Then the CS purists caught us doing it and told us it was terrible and evil, because there are now proofs that used to be rfl but rfl doesn't work any more. My reaction to this was always "so what? It all still works fine" but in Lean 4 they have really attempted to ban this kind of thing (for example I don't think you even can make a declaration irreducible if it's defined in another file). I have no idea why they get so upset about this, it didn't seem to cause any problems in practice in mathlib3 and actually helped to solve problems.

[Sebastian Ullrich]

What I described above is purely related to data structures making these subsystems much faster in Lean 4. Sometimes you can't have fast and flexible at the same time.

[Jun Yoshida]

I didn't know that this "making decls irreducible afterward" pattern got deprecated. The news makes me sad since I was used to it since Lean 2 & 3, too. Anyway, I understand the current Lean 4 behavior about reducibility; the kernel assumes it would be unchanged after declaration. Thank you for letting me know. So, what is the recommended design pattern hiding implementation details? For example, how about this?

@[unbox]
structure Whole (α : Type _) where
  private mk :: private val : {a : α // a = a}

[Sebastian Ullrich]

Yes, newtype-style structures are much preferred over [irreducible]. Note though that private is not as restricting as one might expect, e.g. you can still construct the type using anonymous constructors.

[Jun Yoshida]

Fortunately, I successfully got errors:

/- Another file -/

example : Whole Nat := ⟨10,rfl⟩
example : Whole Nat → Nat := fun ⟨n,h⟩ => n
/-
Both lines produce the following error:
invalid ⟨...⟩ notation, constructor for `Whole` is marked as private
-/

[Sebastian Ullrich]

Hah, thanks for checking! It is not bullet-proof, but neither is it in other languages with reflection