Data.Set.Semiring

Stream: mathlib4

[Riccardo Brasca]

The #port-status page says data.set.semiring is ready to be ported, but we are missing Mathlib.Data.Set.Pointwise.Smul (the only import in mathlib3). Is this a bug?

[Riccardo Brasca]

Sorry, it's there.

[Notification Bot]

Riccardo Brasca has marked this topic as resolved.

[Ruben Van de Velde]

I guess you noticed it's called SMul now

[Notification Bot]

Riccardo Brasca has marked this topic as unresolved.

[Riccardo Brasca]

This file essentially only contains results like

@[simp]
protected theorem down_up (s : Set α) : s.up.down = s :=
  rfl
#align set_semiring.down_up SetSemiring.down_up

This now doesn't work because of dot notation. This works

@[simp]
protected theorem down_up (s : Set α) : SetSemiring.down (Set.up s) = s :=
  rfl
#align set_semiring.down_up SetSemiring.down_up

Is there a way of making dot notation working again? Note that SetSemiring.down is protected, so it is really annoying to use.

[Yaël Dillies]

Oh, while you're on this file, let me know that some statements do not elaborate the way we want them to.

[Yaël Dillies]

I tried fixing them, to no avail

[Riccardo Brasca]

There is one error in instance [CommMonoid α] : CanonicallyOrderedCommSemiring (SetSemiring α) coming from the fact that in NoZeroDivisors we have

eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0

while in CanonicallyOrderedCommSemiring it's

  protected eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0

It's easy to fix, but I am curious why this wasn't a problem in mathlib3.

[Yakov Pechersky]

lean4 eagerly intros implicit args

[Yakov Pechersky]

or it could be a protected attr issue where in one case it has it, in the other it doesn't. What's the error?

[Riccardo Brasca]

type mismatch
  eq_zero_or_eq_zero_of_mul_eq_zero
has type
  ?m.16230 * ?m.16231 = 0 → ?m.16230 = 0 ∨ ?m.16231 = 0 : Prop
but is expected to have type
  ∀ (a b : SetSemiring α), a * b = 0 → a = 0 ∨ b = 0 : Prop

so it seems because of the implict variables.

[Mario Carneiro]

that's a implicit lambda issue

[Riccardo Brasca]

It's solved by adding explictely (instead of getting it from NoZeroDivisors)

eq_zero_or_eq_zero_of_mul_eq_zero := fun _ _ ab => eq_zero_or_eq_zero_of_smul_eq_zero ab

[Riccardo Brasca]

But I am wondering if we should use the same implicitness in both def

[Mario Carneiro]

Actually it's not about lambdas, that's a bug in lean 3, which normally introduces implicit variables in that situation

[Mario Carneiro]

It should be implicit in both places, I think

[Riccardo Brasca]

Let me see what happens if I change it in mathlib3

[Mario Carneiro]

lean 3 will not introduce implicit variables when you reference a structure projection directly. If you make a wrapper, even if it has exactly the same binder info as the projection, it will not have the same behavior

[Riccardo Brasca]

#18167

I indeed had to modify

instance to_no_zero_divisors : no_zero_divisors α :=

[Riccardo Brasca]

mathlib3 seems happy, I've opened #1545.