Where did I lose my way in this proof?

Stream: new members

[Dan Abramov]

I'm trying to prove (based on Tao's book but with an extra challenge) that it's possible to derive a set of all functions from Y to X solely from existence of a powerset and from some ZFC axioms (replacement, specification, but NOT union of a set of sets).

My plan was:

• Start with P(P(X ∪ Y)) where P is the powerset operation
• Filter it down to Kuratowski pairs like {y, {y, x}} that represent (y, x)
• Take a powerset of pairs to get candidates for functions
• Filter it down to valid "functions" (only pairs that map each y to only one x)
• Show a 1:1 correspondence between my set-theoretic "functions" and Mathlib functions

This is where I got so far:

open Classical in
theorem SetTheory.Set.powerset_axiom' {X Y:Set} : ∃ Z:Set,
  ∀ F:Object, F ∈ Z ↔ ∃ f: Y → X, f = F := by
  let pair (a: Object) (b: Object) : Set := {(({a}: Set): Object), (({a,b}: Set): Object)}
  let ⟨PU, hPU⟩ := exists_powerset (X ∪ Y)
  let ⟨PPU, hPPU⟩ := exists_powerset PU
  let YX := PPU.specify (P := fun ppu ↦ ∃ y ∈ Y, ∃ x ∈ X, ppu.val = pair y x)
  let ⟨PYX, hPYX⟩ := exists_powerset YX
  let YXf := PYX.specify (P := fun pyx ↦
    ∃ (pyxs:Set), pyx.val = pyxs ∧
      ∀ y, y ∈ Y ↔
        ∃! yx ∈ pyxs, ∃ x ∈ X,
          yx = pair y x
  )

  let toFun (yxf : YXf) : (Y → X) := fun y ↦
    let hyxf := (specification_axiom'' _ _).mp yxf.2
    let yx_exists := (hyxf.choose_spec.choose_spec.2 y).mp y.property
    let x_exists := yx_exists.choose_spec.1.2
    ⟨x_exists.choose, x_exists.choose_spec.1⟩

  let hsurj : Function.Surjective toFun := by
    intro f
    sorry

  let Z := YXf.replace (P := fun yxf F ↦ F = (toFun yxf)) (by rintro _ _ _ ⟨rfl, rfl⟩; rfl)
  use Z
  intro F
  constructor
  · intro hF
    unfold Z at hF
    rw [replacement_axiom] at hF
    obtain ⟨pairs, rfl⟩ := hF
    use toFun pairs
  rintro ⟨f, rfl⟩
  unfold Z
  rw [replacement_axiom]
  use Function.surjInv hsurj f
  congr; symm
  apply Function.surjInv_eq hsurj

Note this uses Set, replacement_axiom, and specification_axiom'' from Tao's definitions. Complete file here with the incomplete theorem at the end, ready to be pasted into the Lean REPL.

Now, you can see there's a sorry there where I'm trying to show that it's actually possible to find/construct a set of pairs (my "set-function") for a given Mathlib function:

  let hsurj : Function.Surjective toFun := by
    intro f
    sorry

The proof state at that point is:

X Y : Set
pair : Object → Object → Set := fun a b => {set_to_object {a}, set_to_object {a, b}}
PU : Set
hPU : ∀ (x : Object), x ∈ PU ↔ ∃ Y_1, x = set_to_object Y_1 ∧ Y_1 ⊆ X ∪ Y
PPU : Set
hPPU : ∀ (x : Object), x ∈ PPU ↔ ∃ Y, x = set_to_object Y ∧ Y ⊆ PU
YX : Set := PPU.specify fun ppu => ∃ y ∈ Y, ∃ x ∈ X, ↑ppu = set_to_object (pair y x)
PYX : Set
hPYX : ∀ (x : Object), x ∈ PYX ↔ ∃ Y, x = set_to_object Y ∧ Y ⊆ YX
YXf : Set := PYX.specify fun pyx =>
  ∃ pyxs, ↑pyx = set_to_object pyxs ∧ ∀ (y : Object), y ∈ Y ↔ ∃! yx, yx ∈ pyxs ∧ ∃ x ∈ X, yx = set_to_object (pair y x)
toFun : YXf.toSubtype → Y.toSubtype → X.toSubtype := fun yxf y =>
  let hyxf := ⋯;
  let yx_exists := ⋯;
  let x_exists := ⋯;
  ⟨x_exists.choose, ⋯⟩
f : Y.toSubtype → X.toSubtype
⊢ ∃ a, toFun a = f

Now, this is where I got completely lost. I thought it would be easy because I "just" need to trace back through these layers:

  let ⟨PU, hPU⟩ := exists_powerset (X ∪ Y)
  let ⟨PPU, hPPU⟩ := exists_powerset PU
  let YX := PPU.specify (P := fun ppu ↦ ∃ y ∈ Y, ∃ x ∈ X, ppu.val = pair y x)
  let ⟨PYX, hPYX⟩ := exists_powerset YX
  let YXf := PYX.specify (P := fun pyx ↦
    ∃ (pyxs:Set), pyx.val = pyxs ∧
      ∀ y, y ∈ Y ↔
        ∃! yx ∈ pyxs, ∃ x ∈ X,
          yx = pair y x
  )

  let toFun (yxf : YXf) : (Y → X) := fun y ↦
    let hyxf := (specification_axiom'' _ _).mp yxf.2
    let yx_exists := (hyxf.choose_spec.choose_spec.2 y).mp y.property
    let x_exists := yx_exists.choose_spec.1.2
    ⟨x_exists.choose, x_exists.choose_spec.1⟩

and prove the correspondence.

I tried constructing it like this:

  let hsurj : Function.Surjective toFun := by
    intro f
    let pyxs : Set := YX.specify (P := fun yx ↦
      ∃ (y : Object) (hy : y ∈ Y), yx.val = pair y (f ⟨y, hy⟩).1)
    sorry

But actually I realized that I have no idea how to even start going about it. I've tried expanding toFun but I don't know what to do with the goal. When I gave it to Claude, it started proving intermediate statements like ∀ y, y ∈ Y ↔ ∃! yx ∈ pyxs, ∃ x ∈ X, yx = pair y x and (pyxs: Object) ∈ YXf and even had moderate success with it, but it completely gave up on the final goal of toFun ⟨pyxs, h_in_YXf⟩ = f and refused to fill the sorry.

Is it even possible to "unwrap" and retrace a series of choices like I have here:

  let toFun (yxf : YXf) : (Y → X) := fun y ↦
    let hyxf := (specification_axiom'' _ _).mp yxf.2
    let yx_exists := (hyxf.choose_spec.choose_spec.2 y).mp y.property
    let x_exists := yx_exists.choose_spec.1.2
    ⟨x_exists.choose, x_exists.choose_spec.1⟩

and reason about them?

Stepping back to a higher level, I'd like to better understand where I went wrong. I have a few guesses:

• It might've been a bad idea to start with such low level and no supporting structures. E.g. if I want to use Kuratowski pairs, maybe I should first prove some lemmas about them.
• It might be a bad idea to "build up" a bunch of sets via axioms and then try to "work backwards" from the end to figure out what properties hold through the chain. Maybe I should have "built up" assertions about their relations along the way.
• Maybe I should have "extracted" some higher-level concepts (like a function "graph") and proven things about those concepts first.
• Maybe I shouldn't have relied on choice for my main function?
• Maybe I should have made a rigorous paper argument first? I kinda thought that it's "obvious" there's going to be a bijection and I got frustrated that I can't even get a surjection proven.

Overall, given my programmer background, I think I assumed that if I can construct something, it will work — but it felt very hard to prove anything about my construction (despite it being just ~10 lines).

For comparison, @Rado Kirov solved this exercise in a later chapter like this, but using a bunch of more explicit constructions (like Cartesian product and graph). I was trying to keep my proof very low-level as a challenge but it seems like I couldn't handle the challenge.

I'd like to understand whether I'm missing any obvious fixes (e.g. maybe there _is_ a way to unfold these layers that I don't see), and what strategic and tactical blunders I've made when approaching it. My question isn't even so much about this proof in particular but more about how to approach this type of proofs in Lean.

Thanks!

[Aaron Liu]

one at a time

[Aaron Liu]

prove that you have all the pairs before you start building stuff with them

[Rado Kirov]

For comparison, @Rado Kirov solved this exercise in a later chapter like this, but using a bunch of more explicit constructions (like Cartesian product and graph)

I think those are the only two places I use the union_axiom, so I think one approach is to keep that proof and just try take these two defintions:

abbrev SetTheory.Set.slice (x:Object) (Y:Set) : Set :=
  Y.replace (P := fun y z ↦ z = (⟨x, y⟩:OrderedPair)) (by
    intro y z z' ⟨ hz, hz'⟩
    simp_all
  )

/-- Definition 3.5.2 (Cartesian product) -/
abbrev SetTheory.Set.cartesian (X Y:Set) : Set :=
  union (X.replace (P := fun x z ↦ z = slice x Y) (by
    intro x z z' ⟨ hz, hz' ⟩
    simp_all
  ))

are redefining them using powerset and specify instead of replace. Basically, create the big P(P(X \union Y)) and filter, instead of mapping and unioning.

Sorry I didn't fully read the rest of the post to comment on how did you end up stuck specifically.

[Dan Abramov]

For the record, here's how I ended up rewriting it: #Analysis I > ✔ Is Exercise 3.4.6 (ii) missing? @ 💬 .

Not sure if there are more compact ways but the key to not getting lost was to introduce a few abstractions, and to derive intermediate lemmas about those abstractions so that I can keep track of "what I know" about what I've constructed.

[Dan Abramov]

Is it even possible to "unwrap" and retrace a series of choices like I have here:

Answering my own question, the way to unfold them is to use generalize_proofs h to "pull out" the thing we're calling choice on from the goal, and then taking h.choose_spec. This is the main technique I was missing. Another technique I was unaware of is extract_lets which can also be helpful.