What's an idiomatic way to avoid defeq abuse here?

Stream: new members

[Dan Abramov]

I'm working on some proofs related to equivalence of Mathlib functions and Sets of Kuratowski pairs.

My current setup (and a few theorems) looks like this.

import Mathlib.Tactic

def kpair (a b : Nat) : Set (Set Nat) := {{a}, {a, b}}

lemma kpair_injective : ∀ {a₁ b₁ a₂ b₂}, kpair a₁ b₁ = kpair a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ := by
  intro a1 b1 a2 b2 h
  unfold kpair at h
  constructor
  · contrapose! h
    intro hs
    rw [Set.ext_iff] at hs
    specialize hs {a1}
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or] at hs
    rw [← Set.pair_eq_singleton a1, Set.pair_eq_pair_iff] at hs
    simp_all
  contrapose! h
  intro hs
  simp only [Set.pair_eq_pair_iff] at hs
  rcases hs with (_ | ⟨h1, h2⟩)
  · aesop
  rw [← Set.pair_eq_singleton a1, Set.pair_eq_pair_iff] at h1
  rw [← Set.pair_eq_singleton a2, Set.pair_eq_pair_iff] at h2
  simp_all

def IsRelation (g: (Set (Set (Set Nat)))) : Prop := ∀ p ∈ g, ∃ x y, p = kpair x y
def IsDefined (g: (Set (Set (Set Nat)))) : Prop := ∀ x, ∃ y, kpair x y ∈ g
def IsFunctional (g: (Set (Set (Set Nat)))) : Prop := ∀ {x y₁ y₂}, (kpair x y₁) ∈ g → (kpair x y₂) ∈ g → y₁ = y₂
def IsGraph (g: (Set (Set (Set Nat)))) : Prop := IsRelation g ∧ IsDefined g ∧ IsFunctional g

lemma graph_defined (hg : IsGraph g) (x: Nat) : ∃ y, kpair x y ∈ g := by
  unfold IsGraph IsDefined at hg
  exact hg.2.1 x

lemma graph_functional (hg : IsGraph g) (x: Nat) :
  (kpair x y1) ∈ g → (kpair x y2) ∈ g → y1 = y2 := by
  unfold IsGraph IsFunctional at hg
  exact hg.2.2

def funToPairs (f : Nat → Nat) : Set (Set (Set Nat)) :=
  {kpair a (f a) | a : Nat}

def funToPairs_spec (f : Nat → Nat) : p ∈ funToPairs f ↔ ∃ x, kpair x (f x) = p := by
  unfold funToPairs
  simp

def funToPairs_spec' (f : Nat → Nat) : kpair x (f x) ∈ funToPairs f := by
  unfold funToPairs
  simp

noncomputable def pairsToFun (hg : IsGraph g) (x : Nat) :=
  (graph_defined hg x).choose

lemma pairsToFun_spec (hg : IsGraph g) (x : Nat) : kpair x (pairsToFun hg x) ∈ g :=
  (graph_defined hg x).choose_spec

theorem funToPairs_IsGraph (f : Nat → Nat) : IsGraph (funToPairs f) := by
  unfold IsGraph
  constructor
  · unfold IsRelation
    intro p hp
    obtain ⟨x, hx⟩ := (funToPairs_spec f).mp hp
    use x, (f x), hx.symm
  constructor
  · unfold IsDefined
    intro x
    use f x
    apply funToPairs_spec'
  unfold IsFunctional
  intro x y1 y2 h1 h2
  obtain ⟨x1, hx1⟩ := (funToPairs_spec f).mp h1
  obtain ⟨x2, hx2⟩ := (funToPairs_spec f).mp h2
  obtain ⟨rfl, rfl⟩ := kpair_injective hx1
  obtain ⟨rfl, rfl⟩ := kpair_injective hx2
  rfl

theorem pairsToFun_funToPairs (f : Nat → Nat) : pairsToFun (funToPairs_IsGraph f) = f := by
  set hg := funToPairs_IsGraph f
  ext x
  apply graph_functional hg
  · apply pairsToFun_spec
  apply funToPairs_spec'

What I'm hoping to get feedback on is how far I am from idiomatic code. I've previously been doing a lot more unfolding in my proofs but as a result they were very messy and difficult to follow. I've now extracted important props into definitions (IsRelation, IsGraph, etc). My questions are:

• Is this still defeq abuse? Should I keep going further and replace unfold IsRelation and such with lemmas? Should they mirror existing Props 1:1 or is there something smarter I could do?
• Are these funToPairs_specand funToPairs_spec' weird? I've defined them next to funToPairs but not sure if they're too trivial and if the names make sense.
• Am I using explicit/implicit parameters well, or could signatures be improved?
• Overall, if you were reworking this, is there anything you'd change at a high level? Maybe replacing Props with structures? Or something else?

Thanks!

[Aaron Liu]

Dan Abramov said:

• Are these funToPairs_specand funToPairs_spec' weird? I've defined them next to funToPairs but not sure if they're too trivial and if the names make sense.

Quite the opposite, this is how most definitions in mathlib work. What you are supposed to do is define your definition, and then (in the same file preferably) you should prove a bunch of lemmas about your definition so you never have to unfold it again. In practice this is not what happens, and being able to unfold some definitions is useful, for example docs#Set.mem_inter_iff, docs#Set.mem_compl_iff, and docs#Set.subset_def are theorems I rarely use because they're defeqs and I can just (implicity) unfold some definitions.

[Dan Abramov]

If I were to tuck away the props like this:

structure IsGraph (g : Set (Set (Set Nat))) where
  relation : ∀ p ∈ g, ∃ x y, p = kpair x y
  defined : ∀ x, ∃ y, kpair x y ∈ g
  functional : ∀ {x y₁ y₂}, kpair x y₁ ∈ g → kpair x y₂ ∈ g → y₁ = y₂

is there still a benefit to having lemmas like

lemma graph_relation (hg : IsGraph g) : ∀ p ∈ g, ∃ x y, kpair x y = p := by
  intro p hp
  obtain ⟨x, ⟨y, rfl⟩⟩ := hg.relation p hp
  use x, y

lemma graph_defined (hg : IsGraph g) (x: Nat) : ∃ y, kpair x y ∈ g := by
  exact hg.defined x

lemma graph_functional (hg : IsGraph g) (x: Nat) :
  (kpair x y1) ∈ g → (kpair x y2) ∈ g → y1 = y2 := by
  exact hg.functional

?

Or are structure fields generally considered public API?

[Kyle Miller]

Structure fields are usually public API. You can mark fields as private:

structure S where
  x : Nat
  private y : Nat

That doesn't affect the current module, but anyone who imports it won't be able to use S.y.

Sometimes it's worth having extra lemmas like that if they restate the field differently.

[Dan Abramov]

Ah, cool. Using a Graph structure feels a bit cleaner. With this change, I've gotten rid of the _spec stuff, not sure if that's okay here.

import Mathlib.Tactic

def kpair (a b : Nat) : Set (Set Nat) := {{a}, {a, b}}

lemma kpair_injective : ∀ {a₁ b₁ a₂ b₂}, kpair a₁ b₁ = kpair a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ := by
  intro a1 b1 a2 b2 h
  unfold kpair at h
  constructor
  · contrapose! h
    intro hs
    rw [Set.ext_iff] at hs
    specialize hs {a1}
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or] at hs
    rw [← Set.pair_eq_singleton a1, Set.pair_eq_pair_iff] at hs
    simp_all
  contrapose! h
  intro hs
  simp only [Set.pair_eq_pair_iff] at hs
  rcases hs with (_ | ⟨h1, h2⟩)
  · aesop
  rw [← Set.pair_eq_singleton a1, Set.pair_eq_pair_iff] at h1
  rw [← Set.pair_eq_singleton a2, Set.pair_eq_pair_iff] at h2
  simp_all

@[ext]
structure Graph where
  pairs : Set (Set (Set Nat))
  relation : ∀ p ∈ pairs, ∃ x y, p = kpair x y
  defined : ∀ x, ∃ y, kpair x y ∈ pairs
  functional : ∀ {x y₁ y₂}, kpair x y₁ ∈ pairs → kpair x y₂ ∈ pairs → y₁ = y₂

def funToGraph (f : Nat → Nat) : Graph where
  pairs := {kpair a (f a) | a : Nat}
  relation := by
    intro p hp
    obtain ⟨x, hx⟩ :=  hp
    use x, (f x), hx.symm
  defined := by
    intro x
    use f x
    simp
  functional := by
    intro x y1 y2 h1 h2
    obtain ⟨x1, hx1⟩ := h1
    obtain ⟨x2, hx2⟩ := h2
    obtain ⟨rfl, rfl⟩ := kpair_injective hx1
    obtain ⟨rfl, rfl⟩ := kpair_injective hx2
    rfl

noncomputable def Graph.toFun (g: Graph) (x : Nat) :=
  (g.defined x).choose

lemma Graph.toFun_spec (g: Graph) (x : Nat) : kpair x (g.toFun x) ∈ g.pairs :=
  (g.defined x).choose_spec

theorem pairsToFun_funToPairs (f : Nat → Nat) : (funToGraph f).toFun = f := by
  set g := funToGraph f
  ext x
  apply g.functional
  · apply g.toFun_spec
  simp [g, funToGraph]

theorem funToPairs_surjective (g: Graph) : ∃ f : Nat → Nat, funToGraph f = g := by
  set f := g.toFun
  use f
  ext p
  constructor
  · rintro ⟨x, rfl⟩
    apply g.toFun_spec
  intro hp
  obtain ⟨x, ⟨_, rfl⟩⟩ := g.relation p hp
  use x
  have hp' := g.toFun_spec x
  rw [g.functional hp hp']