nice code snippet: equality of pairs

Stream: lean4

[Floris van Doorn]

Based on the discussion in #Is there code for X? > surreals (but in parallel to Knuth book) I wanted to prove as an exercise the defining property of Kuratowski pairs. This was a nice test to test the capabilities of grind. grind can prove all but 1 of these lemmas, the last one is provably with simp.

class HasPairing (α : Type _) where
  mem : Membership α α
  ext {x y : α} : (∀ z, z ∈ x ↔ z ∈ y) → x = y
  pair : α → α → α
  mem_pair {x y z : α} : z ∈ pair x y ↔ z = x ∨ z = y

open HasPairing
attribute [instance] mem
attribute [ext, grind ext] ext
attribute [simp, grind =] mem_pair

notation (priority := high) "{" x ", " y "}" => pair x y
notation (priority := high) "{" x "}" => pair x x

variable {α : Type _} [HasPairing α] {x y x' y' z : α}

@[grind]
def orderedPair (x y : α) : α := {{x}, {x, y}}

notation (priority := high) "(" x ", " y ")" => orderedPair x y

@[simp, grind =]
theorem mem_orderedPair : z ∈ (x, y) ↔ x ∈ z ∧ ∀ w ∈ z, w = x ∨ w = y := by grind

@[grind! .] theorem left_mem_orderedPair : {x} ∈ (x, y) := by grind
@[grind! .] theorem right_mem_orderedPair : {x, y} ∈ (x, y) := by grind

-- Only this lemma is out-of-reach for `grind`, since it cannot use `forall_eq_or_imp`
@[grind =] theorem pair_mem_orderedPair : {x, y} ∈ (x, y') ↔ y = x ∨ y = y' := by simp

theorem orderedPair_eq_iff : (x, y) = (x', y') ↔ x = x' ∧ y = y' := by grind