Proposal: Add decidable membership for Interval

Stream: mathlib4

[Ka Wing Li]

I am proposing to add the following

instance [Preorder α] : Membership α (Interval α) where
  mem := sorry
instance [Preorder α] [DecidableLE α] (x : α) (i : NonemptyInterval α) : Decidable (x ∈ i) :=
  sorry
instance [Preorder α] [DecidableLE α] (x : α) (i : Interval α) : Decidable (x ∈ i) :=
  sorry

[Ka Wing Li]

It will allow us to do something like

def interval : Interval ℕ := { fst := 0, snd := 10, fst_le_snd := by grind : NonemptyInterval ℕ}
#eval 5 ∈ interval -- true
example : 5 ∈ interval := by
  simp [interval]

[Aaron Liu]

Do we already get the membership instance or is that new

[Ka Wing Li]

As far as I know, I haven't found any implementation about it.

[Ka Wing Li]

Originated from #Is there code for X? > membership with interval

[Ka Wing Li]

After I add the implementations, it seems broke Interval.mem_pure

[Ka Wing Li]

The proof does not need to go to SetLike; does it even need to be a PartialOrder?

@[simp]
theorem mem_pure : b ∈ pure a ↔ b = a := by
  simp [pure]
  -- original proof
  -- rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]

[Aaron Liu]

So it looks like there was already another membership instance

[Aaron Liu]

You should get rid of your new membership and just use the old one

[Ka Wing Li]

Yet, the older one has a stronger requirement of PartialOrder instead of a weaker requirement of Preorder in the new definition.

[Aaron Liu]

oh I guess representation as a set isn't faithful if you don't have antisymmetry

[Aaron Liu]

in that case I don't think Interval correctly captures my intuition on what an interval is

[Aaron Liu]

so I wouldn't be too concerned about preorders

[Ka Wing Li]

I think we can have intervals well defined in a preorder set.

[Ka Wing Li]

So far from isabelle I found membership of interval still uses preorder.

[Ka Wing Li]

NonemptyInterval.instCoeSet still uses preorder. I am wondering where do we end up with partial order in mathlib.

[Robin Arnez]

The reason we need PartialOrder is that SetLike requires the map into a Set to be injective, i.e. two different intervals should also yield two different Sets.

[Ka Wing Li]

Btw, I have made a PR at mathlib4#33299

[Ka Wing Li]

Interesting, I am curious why Setlike requires Partialorder / injective?

[Ka Wing Li]

It is sad that we will never be able to define the following without breaking definitional equality

instance {α β} [Membership α β] : Membership α (WithBot β) where
  mem
  | ⊥ => fun _ => False
  | (b : β) => fun a => a ∈ b

[Ka Wing Li]

I am curious about the following

An alternative to SetLike could have been an extensional Membership typeclass:

class ExtMembership (α : out_param <| Type u) (β : Type v) extends Membership α β where
  (ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)

While this is equivalent, SetLike conveniently uses a carrier set projection directly.

[Ka Wing Li]

ExtMembership looks good, which does not require injectivity.

[Aaron Liu]

no it definitely does require injectivity

[Ka Wing Li]

Hmm, I don't see how?

[Ka Wing Li]

Copied an image from wiki
image.png

[Ka Wing Li]

For this preorder set with x R y defined by $x / 4 \le y / 4$ over naturral number. I can define intervals [4, 11] and [6, 9], which are equal. And the corresponding set is just {4,5,6,7,8,9,10,11}.

[Ka Wing Li]

And it satisfies ext_iff.

[Aaron Liu]

but [4, 11] ≠ [6, 9] because their left endpoints aren't equal

[Aaron Liu]

but they have the same members

[Aaron Liu]

so it's not extensional

[Johan Commelin]

Doesn't that depend on your definition of interval? The lemma [a,b] = [c,d] \iff a = c \and b = d will be false. So then we prove that lemma under the stronger partial order assumption...

[Aaron Liu]

I was just going off how the type docs#Interval works

[Ka Wing Li]

Hmm, I am thinking about extensionality: $[a, b] = [c, d] \iff \forall x, (x \in [a, b]) = (x \in [c, d])$

[Aaron Liu]

well if you quotient by extensionality you get extensionality for free

[Johan Commelin]

Aaron Liu said:

I was just going off how the type docs#Interval works

Fair enough. :smiley:

I hadn't looked at it :man_facepalming:

[Ka Wing Li]

Hmm, ain't partial order kind of like a quotient of preorder? Let me lookup more info.

[Aaron Liu]

an Interval is either the empty interval, or a docs#NonemptyInterval which bundles its two endpoints and a proof the the left endpoint is smaller than the right endpoint

[Aaron Liu]

Ka Wing Li said:

Hmm, ain't partial order kind of like a quotient of preorder? Let me lookup more info.

see docs#Antisymmetrization

[Ka Wing Li]

Is there anything like $a \cong b \iff f a \cong f b$. Galois connection / natural transformation / ..., can't remember the terminology.

[Ka Wing Li]

a weaker form of extensionality

[Aaron Liu]

not sure what you mean

[Aaron Liu]

what is $\cong$

[Ka Wing Li]

Like the intervals $[4, 11] \cong [6, 9]$

[Aaron Liu]

do you mean docs#AntisymmRel

[Ka Wing Li]

Just realised interesting stuff: for Preorder a, we have Preorder (NonemptyInterval a)

[Ka Wing Li]

Yes, $\cong$ is the docs#AntisymmRel. I am asking about the $\iff$ part.

[Aaron Liu]

I don't think we have anything exactly like that then

[Aaron Liu]

I guess you could build it with docs#RelIso

[Aaron Liu]

or maybe docs#RelEmbedding

[Ka Wing Li]

Hmm, then we are going back to docs#OrderEmbedding to docs#SetLike :joy:

[Ka Wing Li]

Nvm

[Ka Wing Li]

Quick question, why docs#RelEmbedding has to be injective?

[Ka Wing Li]

Originated from why docs#OrderEmbedding has to be injective?

[Ka Wing Li]

Mathematically we just need $x\leq y \iff f(x)\preceq f(y)$

[Ka Wing Li]

imaging working on preorder set

[Aaron Liu]

I feel like it's not as common to have something like that

[Aaron Liu]

where it's both ways

[Aaron Liu]

unless it's an embedding of one thing as a sub-thing of another thing

[Ka Wing Li]

Hmm, it's not that uncommon if we work on the category of preorder sets.

[Ka Wing Li]

Anyway thanks!