set of pairs

Stream: general

[Alexandre Rademaker]

#check { n : ℕ | n < 3 }
#check { (n, m)  | n < 2 ∧ m < 5 } -- ERROR

Why I can't construct a set of pairs of numbers? The first command works, why the second fails?

[Scott Morrison]

The set builder notation is very basic. You can't write patterns in the left slot.

[Scott Morrison]

#check { p : ℕ × ℕ | p.1 < 2 ∧ p.2 < 5 }

[Scott Morrison]

I would guess that Lean4 is going to let us do things the way you want, however.

[Alexandre Rademaker]

Hum, thinking in an alternative for defining

def r_interp (I : Interpretation AtomicConcept AtomicRole) : Role AtomicRole → set (I.δ × I.δ)
  | (Role.Atomic R)  := I.atom_R R
  | (Role.Compose R S) := { (a, b) | ∀ a b c : I.δ, (a, b) ∈ I.atom_R R ∧ (b,c) ∈ I.atom_R S }
  | (Role.Inverse R)   := { b : I.δ × I.δ | ∀ a b: I.δ, (a, b) ∈ I.atom_R R }

that is, an interpretation of a Compose R S where both R and S has (by induction) the interpretation as pairs...

[Leonardo de Moura]

Scott Morrison said:

I would guess that Lean4 is going to let us do things the way you want, however.

You guessed right :)

def Set (α : Type u) := α → Prop
def Set.in (s : Set α) (a : α) := s a

notation:50 a " ∈ " s:50 => Set.in s a

notation "{" a "|" p "}" => fun a => p

theorem ex : (1, 3) ∈ { (n, m) | n < 2 ∧ m < 5 } := by
  simp [Set.in]

[Scott Morrison]

That is shockingly straightforward. :-)

[Alexandre Rademaker]

Indeed

[Kevin Buzzard]

I remember asking Sebastian over a year ago whether this exact thing would be possible in Lean 4 and him being optimistic, but it's great to see that it's also easy :-)