Lean style - how to best pack API for a new definition

Stream: new members

[Rado Kirov]

Say I am in the middle of a long proof and want to introduce a new local definition let x' = ...<something in terms of x,y,z...>. If I also decide to build a mini API of lemmas - have (h: <some prop about x' and x,y,z>): <some other prop about x',x,y,z>. I prove it using unfold, but then for the rest of the proof I try not to use unfold and just these lemmas. This works reasonably well, and I have done it in the past for long proofs.

What I am unclear, is if the proof gets even longer, and I want to extract something about x' and it's APIs to a stand-alone lemma, how to pass the original definition and APIs. Should I try to pack them in a structure? Or maybe capture the definition in a single _def lemma that fully captures the definition and pass that around?

Here is somewhat contrived example.

import Mathlib

lemma double_pos {X doubleX: Set ℚ} (h: ∀ x, x ∈ doubleX ↔ ∃ y, y ^ 2 = x) (y: ℚ): y ∈ doubleX → y ≥ 0 := by sorry

example (X: Set ℚ): True := by
  -- some proof
  let doubleX := {x ^ 2 | x ∈ X}
  have doubleX_def (x: ℚ): x ∈ doubleX ↔ ∃ y, y ^ 2 = x := by
    unfold doubleX
    simp
  have (x: ℚ): x ∈ doubleX → x ≥ 0 := by
    unfold doubleX
    simp
    intro y hy hs
    subst x
    exact sq_nonneg y
  -- rest of proof
  tauto

[Eric Wieser]

If the proof starts to get really long, often you'd promote the let to a def

[Eric Wieser]

And then replace the have with lemmas about that def

[Rado Kirov]

I see so something like this

import Mathlib

def SquaredSet(X: Set ℚ) := {x ^ 2 | x ∈ X}

-- unfolds allowed here, this is the API
lemma SquaredSet_pos {X: Set ℚ}: ∀ x, x ∈ SquaredSet X -> x ≥ 0 := by
  intro x h
  unfold SquaredSet at h
  simp at h
  obtain ⟨y, hy, hs⟩ := h
  subst x
  exact sq_nonneg y
-- end of SquaredSet API

example (X: Set ℚ): True := by
  -- some proof
  let S := SquaredSet X
  -- no unfolds here use API
  have := SquaredSet_pos (X:=X)
  -- rest of proof
  tauto

[Aaron Liu]

similar yes

[Eric Wieser]

Note that SquaredSet is in mathlib as X ^ 2 with open scoped Pointwise

[Eric Wieser]

(also note that #naming tells you to capitalize it as squaredSet)

[Damiano Testa]

Is X ^ 2 under Pointwise the set of squares or the set of products on two elements from X?

[Rado Kirov]

Oh, the example doesn't matter at all, I just wrote some contrived let := ...

[Rado Kirov]

My point is in regular programming when I have a messy bunch of code, I know how to refactor it - find repeated expressions - extract to variables and function (with local or global scope). Modern IDEs even provide these basic refactoring for some languages.

However, in theorem proving land it is not so simple, once you pull out some expressions you have to manually keep unfolding it all proofs, which almost defeats the purpose. So one has to also declare some API lemmas with the factored out definition, but I don't have good sense how to package these API + definition, for a clean refactoring.

[Kevin Buzzard]

If you come across a definition which looks useful then factor it out and make some API and yes you're allowed to unfold. Alternatively if the API is always "unfold and then use API for what you got" then maybe an abbrev is in order.

[Eric Wieser]

Damiano Testa said:

Is X ^ 2 under Pointwise the set of squares or the set of products on two elements from X?

We have instances for both!

[Eric Wieser]

(and so also, I don't know)

[Aaron Liu]

It depends on what you open

[Eric Wieser]

Does it?

[Aaron Liu]

I hope it does