Definition of subset

Stream: mathlib4

[Dan Velleman]

Mathlib.Init.Set.lean contains these lines:

protected def Subset (s₁ s₂ : Set α) :=
∀ {a}, a ∈ s₁ → a ∈ s₂

instance : HasSubset (Set α) :=
⟨Set.Subset⟩

Mathlib.Data.Set.Basic.lean contains these lines:

instance : LE (Set α) :=
  ⟨fun s t => ∀ ⦃x⦄, x ∈ s → x ∈ t⟩

instance : HasSubset (Set α) :=
  ⟨(· ≤ ·)⟩

It appears to me that, as a result, sometimes "subset" gets interpreted with ∀ {a} and sometimes with ∀ ⦃x⦄. For example, try this:

import Mathlib

elab "whnf" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let t ← Lean.Elab.Tactic.getMainTarget
    let w ← Lean.Meta.whnf t
    dbg_trace w

example {A B : Set Nat} : A ⊆ B := by
  whnf

example (A B : Set Nat) : A ∈ 𝒫 B := by
  whnf

In the first example, the output starts with forall {{x : Nat}}, and in the second it starts with forall {a : Nat}. This seems confusing. I suppose the differences in behavior will be rare, but occasionally "subset" will behave in inconsistent ways. Shouldn't it be consistent?

[Yaël Dillies]

I think Mathlib.Init.Set was written before mathport was taought about semi-implicit brackets. So please change it, yes!

[Dan Velleman]

I don't know how to do PRs. Can someone else do it?

[Dan Velleman]

Is there a reason for defining "subset" twice?

[Yaël Dillies]

No, this is weird too.

[Dan Velleman]

There are two more duplications: instances of Union and Inter are defined in both files. I suppose those are less of a problem, because the two definitions end up reducing to the same thing, so you won't have the kind of inconsistency that is happening with HasSubset. But should these things only be defined once?

I don't know Mathlib well enough to know what should be done about this, if anything.

[Yaël Dillies]

This is a remnant of the same duplication in Lean 3, I'm afraid.

[Dan Velleman]

Here's what would make sense to me:

1. Fix the definition of Subset in Mathlib.Init.Set.lean to use ⦃ ⦄ rather than { }
2. Remove the instances of HasSubset, Union, and Inter from Mathlib.Data.Set.Basic.lean, since they are duplicates of instances that already exist.

But I don't know enough about Mathlib to know if that would cause problems.

[Jireh Loreaux]

You can just change it and try building.

[Dan Velleman]

I don't know how to do PRs. If someone else thinks this change makes sense, perhaps they could do it?

[Dan Velleman]

@Yaël Dillies No, I don't think the same duplication existed in Lean 3. In Lean 3, the file core/init.data.set didn't define subset, union, or intersection. Those definitions were only in mathlib/data.set.basic. I think the duplication is the result of the fact that in Mathlib4, Mathlib/Init/Set.lean contains extra stuff that wasn't in Lean 3's core/init.data.set. I'm not sure why that was done.

[Eric Wieser]

I would guess this is junk left from the adhoc port

[Dan Velleman]

Should something be done to clean this up? For a project I'm working on, it's really annoying that there are two definitions of subset that don't quite agree.

[Eric Wieser]

Yes, just delete the ones that aren't there in mathlib3 and see what breaks

[Yaël Dillies]

(and the best way to get something done is to do it yourself :wink:)

[Anne Baanen]

I've made an initial pass in mathlib4#1550 but won't be able to babysit it in the coming days, please push fixes if you have time! :)

[Yaël Dillies]

Ah thank you I was about to do the same :)

[Dan Velleman]

Thanks everyone!

[Anne Baanen]

You were right that this could cause subtle problems: apparently Lean prefers to have the ≤ notation as primitive and then ⊆ defined in terms of it, otherwise it won't accept ⊆ hypotheses to ≤ theorems.

[Anne Baanen]

Let's see if this fix doesn't cause further issues down the line...