membership with interval

Stream: Is there code for X?

[Ka Wing Li]

Discussion at #mathlib4 > Proposal: Add decidable membership for Interval

How to use interval? Tried

import Mathlib
-- def tmp := Finset.Icc 0 10
def tmp : Interval ℕ := some { fst := 0, snd := 10, fst_le_snd := by grind}
#eval 5 ∈ tmp
/- failed to synthesize
  Decidable (5 ∈ tmp) -/

[Ka Wing Li]

Try to define membership

instance {α} [LE α] : Membership α (Interval α) where
  mem
  | none, _ => False
  | some ι, a => a ∈ ι
/- failed to synthesize instance of type class
  Membership α (NonemptyInterval α) -/

[Ka Wing Li]

But don't we have NonemptyInterval.instMembership?

[Aaron Liu]

what do you want to do

[Aaron Liu]

can you make a #mwe

[Ka Wing Li]

Ka Wing Li said:

import Mathlib
-- def tmp := Finset.Icc 0 10
def tmp : Interval ℕ := some { fst := 0, snd := 10, fst_le_snd := by grind}
#eval 5 ∈ tmp
/- failed to synthesize
  Decidable (5 ∈ tmp) -/

Is this mwe?

[Robin Arnez]

It seems like we're simply missing some Decidable instances:

import Mathlib

instance [Preorder α] [DecidableLE α] (x : α) (i : NonemptyInterval α) : Decidable (x ∈ i) :=
  inferInstanceAs (Decidable (i.fst ≤ x ∧ x ≤ i.snd))

instance [PartialOrder α] [DecidableLE α] (x : α) (i : Interval α) : Decidable (x ∈ i) :=
  match i with
  | ⊥ => isFalse (by rw [← SetLike.mem_coe]; simp)
  | (a : NonemptyInterval α) => inferInstanceAs (Decidable (x ∈ a))

def tmp : Interval ℕ := some { fst := 0, snd := 10, fst_le_snd := by grind}

#eval 5 ∈ tmp

[Ka Wing Li]

Thanks!

[Ka Wing Li]

I am wondering whether we need Interval.instMembership as well?

[Ka Wing Li]

I am puzzled about the differences in the following two evals

import Mathlib

instance [Preorder α] [DecidableLE α] (x : α) (i : NonemptyInterval α) : Decidable (x ∈ i) :=
  inferInstanceAs (Decidable (i.fst ≤ x ∧ x ≤ i.snd))

instance [PartialOrder α] [DecidableLE α] (x : α) (i : Interval α) : Decidable (x ∈ i) :=
  match i with
  | ⊥ => isFalse (by rw [← SetLike.mem_coe]; simp)
  | (a : NonemptyInterval α) => inferInstanceAs (Decidable (x ∈ a))

def tmp : Interval ℕ := some { fst := 0, snd := 10, fst_le_snd := by grind}

#eval 5 ∈ tmp
-- true
#eval 5 ∈ (some { fst := 0, snd := 10, fst_le_snd := by grind} : Interval ℕ)
-- false

[Robin Arnez]

Oh, using some is defeq abuse, it interpreted this as

#eval (5 : NonemptyInterval ℕ) ∈ some { fst := 0, snd := 10, fst_le_snd := by grind : NonemptyInterval ℕ }

The right way to write this is:

#check 5 ∈ ({ fst := 0, snd := 10, fst_le_snd := by grind : NonemptyInterval ℕ } : Interval ℕ)

[Ka Wing Li]

I see! Thanks for clarifying.

[Ka Wing Li]

Okay, a simplified version

@[instance 100]
instance Interval.instMembership {α} [Preorder α] : Membership α (Interval α) where
  mem
  | ⊥, _ => False
  | (i : NonemptyInterval α), x => x ∈ i

instance [Preorder α] [DecidableLE α] (x : α) (i : NonemptyInterval α) : Decidable (x ∈ i) :=
  inferInstanceAs (Decidable (i.fst ≤ x ∧ x ≤ i.snd))

instance [Preorder α] [DecidableLE α] (x : α) (i : Interval α) : Decidable (x ∈ i) :=
  match i with
  | ⊥ => isFalse (by simp only [Interval.instMembership, not_false_eq_true])
  | (i : NonemptyInterval α) => inferInstanceAs (Decidable (x ∈ i))

def tmp : Interval ℕ := { fst := 0, snd := 10, fst_le_snd := by grind : NonemptyInterval ℕ}

#eval 5 ∈ tmp

example : 5 ∈ tmp := by
  unfold tmp
  simp only [Interval.instMembership]
  simp

[Ka Wing Li]

Should this be upstreamed?

[Robin Arnez]

Well remove the top instance though, that's an instance diamond with docs#Interval.setLike

[Ka Wing Li]

Sorry, I do not understand? Could you elab more?

[Ka Wing Li]

I am wondering about the [PartialOrder α] requirement if we use SetLike.mem_coe?

[Ka Wing Li]

My implementation keeps the weaker [Preorder α] requirement as in Interval definitions.

[Robin Arnez]

Well if you add Interval.instMembership, there will be two instance paths to e.g. Membership ℕ (Interval ℕ). The first being docs#Interval.setLike followed by docs#SetLike.instMembership and the other one being Interval.instMembership. Having two instances of the same thing is most likely a bad idea! Which is to say, I wouldn't try to generalize Interval to work with Preorders because that would require a larger refactor but rather just keep to PartialOrder.

[Edward van de Meent]

Note that it's only an issue if they are not definitionally equal...

[Aaron Liu]

defeq at reducible+instances transparency

[Aaron Liu]

I'm 80% sure they're defeq at default transparency if you turn off smart unfolding

[Edward van de Meent]

Right, but my point is that having multiple paths to deriving a certain instance is not an issue per sé. (Please do verify if the proposed instance is actually not defeq at the right transparency, as I'm on mobile right now)

[Ka Wing Li]

Forwarding the mathlib proposal at #mathlib4 > Proposal: Add decidable membership for Interval

[Ka Wing Li]

Do you mean proving this?

theorem coe_mem : a ∈ (s : Interval α) ↔ a ∈ (s : Set α) := by
  simp only [instMembership, SetLike.mem_coe]
  apply Iff.intro
  · intro h
    split at h
    · exact h
    · exact h
  · intro h
    split
    · exact h
    · exact h

[Aaron Liu]

not proving it

[Aaron Liu]

proving it specifically with rfl

[Aaron Liu]

well more specifically by with_reducible_and_instances rfl

[Ka Wing Li]

Oh, I see what you mean. Recalled what definitionally equal means.

[Ka Wing Li]

Sadly, I endup with

theorem coe_mem (s : Interval α) : (a ∈ s) ↔ (a ∈ (s : Set α)) := by
  cases s
  · rfl
  · rfl

[Ka Wing Li]

with_reducible_and_instances rfl doesn't work.

[Ka Wing Li]

However, I found that in mathlib4 NonemptyInterval.coe_coeHom is also not definitionally equal.

@[simp]
theorem coe_coeHom : (coeHom : NonemptyInterval α → Set α) = ((↑) : NonemptyInterval α → Set α) :=
  by with_reducible_and_instances rfl
  /-
Tactic `rfl` failed: The left-hand side
  ⇑coeHom
is not definitionally equal to the right-hand side
  SetLike.coe
  -/

[Aaron Liu]

well that one doesn't need to be

[Ka Wing Li]

Excuse me, why not?

[Aaron Liu]

it's not an instance