Tips on improving proofs

Stream: new members

[shortc1rcuit]

I'm writing up some notes on Dedekind cuts in Lean. The part I'm currently doing is showing that the definition of multiplication (for non-negative numbers) is valid (i.e. it outputs a Dedekind cut). However, the Lean code I wrote works but feels rather janky (probably due to the fact I was writing it at 11pm last night). I'm not sure how to improve it though.

Here is the MWE for the code

import Mathlib.Tactic

structure DedekindCut where
  set : Set ℚ
  set_nonempty : set.Nonempty
  set_ne_univ : set ≠ Set.univ
  mem_of_gt_mem (x y : ℚ) : x < y → y ∈ set → x ∈ set
  exists_gt : ∀ x ∈ set, ∃ y ∈ set, x < y

def DedekindCut.le (A A' : DedekindCut) : Prop := A.set ⊆ A'.set
instance : LE DedekindCut where le := DedekindCut.le
theorem le_def {A A' : DedekindCut} : A ≤ A' ↔ A.set ⊆ A'.set := by rfl

def DedekindCut.zero : DedekindCut where
  set := {x | x < 0}
  set_nonempty := by use -1; simp
  set_ne_univ := by rw[Set.ne_univ_iff_exists_not_mem]; use 1; simp
  mem_of_gt_mem := fun x y ↦ lt_trans
  exists_gt := fun x hx ↦ ⟨x / 2, by simp at *; constructor <;> linarith⟩
instance : Zero DedekindCut where zero := DedekindCut.zero
theorem zero_def : 0 = DedekindCut.zero := by rfl

variable {α : Type*} [LE α] (E : Set α)
def IsUpperBound (l : α) := ∀ x ∈ E, x ≤ l
def BddAbove' := ∃ l, IsUpperBound E l

theorem DedekindCut.bddAbove' (A : DedekindCut) : BddAbove' A.set := by
  rcases (Set.ne_univ_iff_exists_not_mem _).1 A.set_ne_univ
    with ⟨x, hx⟩
  use x
  contrapose! hx
  simp [IsUpperBound] at hx
  rcases hx with ⟨y, hy₁, hy₂⟩
  exact A.mem_of_gt_mem x y hy₂ hy₁

lemma DedekindCut.nonneg_upperBound_nonneg {A : DedekindCut} {a : ℚ} (hA : 0 ≤ A) (ha : IsUpperBound A.set a) : 0 ≤ a := by
  contrapose! ha
  simp [IsUpperBound]
  use a / 2
  constructor
  · apply hA
    simp [zero_def, DedekindCut.zero]
    linarith
  · linarith

def DedekindCut.mulNonneg (A B : DedekindCut) (hA : 0 ≤ A) (hB : 0 ≤ B) : DedekindCut where
  set := {x | x < 0} ∪ {a * b | (a ∈ A.set) (_ : 0 ≤ a) (b ∈ B.set) (_ : 0 ≤ b)}
  set_nonempty := by
    use -1
    left
    simp
  set_ne_univ := by
    rcases A.bddAbove' with ⟨a, ha⟩
    rcases B.bddAbove' with ⟨b, hb⟩
    have : IsUpperBound ({x | x < 0} ∪ {a * b | (a ∈ A.set) (_ : 0 ≤ a) (b ∈ B.set) (_ : 0 ≤ b)}) (a * b) := by
      rintro x (hx | ⟨a', ha'₁, ha'₂, b', hb'₁, hb'₂, rfl⟩)
      · have := mul_nonneg (A.nonneg_upperBound_nonneg hA ha) (B.nonneg_upperBound_nonneg hB hb)
        simp at hx
        linarith
      · exact mul_le_mul (ha a' ha'₁) (hb b' hb'₁) hb'₂ (A.nonneg_upperBound_nonneg hA ha)
    rw [Set.ne_univ_iff_exists_not_mem]
    use a * b + 1
    intro h
    linarith [this (a * b + 1) h]
  mem_of_gt_mem := by
    rintro x y hxy (hy | ⟨a, ha₁, ha₂, b, hb₁, hb₂, hab⟩)
    · simp at hy ⊢
      left
      linarith
    · rcases lt_or_le x 0 with h | h
      · left
        exact h
      right
      use x / b
      have : y ≠ 0 := by linarith
      rw [←hab, mul_ne_zero_iff] at this
      constructor
      · apply A.mem_of_gt_mem _ _ _ ha₁
        rwa [←mul_div_cancel_right₀ a this.2, hab, div_lt_div_iff_of_pos_right]
        rw [lt_iff_le_and_ne]
        exact ⟨hb₂, this.2.symm⟩
      use (div_nonneg h hb₂), b, hb₁, hb₂
      exact div_mul_cancel₀ x this.2
  exists_gt := by
    simp
    rintro x (hx | ⟨a, ha₁, ha₂, b, hb₁, hb₂, hab⟩)
    · use x / 2
      constructor
      · left
        linarith
      · linarith
    · rcases A.exists_gt a ha₁ with ⟨a', ⟨ha'₁, ha'₂⟩⟩
      rcases B.exists_gt b hb₁ with ⟨b', ⟨hb'₁, hb'₂⟩⟩
      use a' * b'
      constructor
      · right
        use a', ha'₁, (by linarith), b', hb'₁, (by linarith)
      · rw [←hab]
        exact mul_lt_mul' (le_of_lt ha'₂) hb'₂ hb₂ (lt_of_le_of_lt ha₂ ha'₂)

My question is two-fold

1. What ways can I improve this proof specifically?
2. What advice do you have in general for improving proofs in Lean after the first draft?

[Kevin Buzzard]

Multiplication is necessarily janky for Dedekind cuts, that's why mathlib goes with Cauchy sequences. One nice way to make the reals with Dedekind cuts is to start by defining the positive naturals inductively, then the positive rationals as quotients, then the positive reals as Dedekind cuts and only then introduce 0 and subtraction.

[Kevin Buzzard]

Just looking at the proof now, it doesn't look too bad at all (as I say, the problem is with the strategy not the proof) but you do have non-terminal simps in the proofs of exists_gt and mem_of_gt_mem.

[Kevin Buzzard]

Regarding improving proofs, you should formalise stuff which mathlib wants and then make PRs. Then experts will review your code

[shortc1rcuit]

Kevin Buzzard said:

Just looking at the proof now, it doesn't look too bad at all (as I say, the problem is with the strategy not the proof) but you do have non-terminal simps in the proofs of exists_gt and mem_of_gt_mem.

Oh is that not a thing I should do?

[Chris Wong]

The problem with non-terminal simps is that the set of simp lemmas changes all the time, so if you depend on a particular result, it's likely to break later on.

[Kevin Buzzard]

It makes the proofs harder to maintain, because if someone adds a simp lemma later on then your code can break in hard-to-understand ways; basically it's hard to predict what simp did if it didn't close the goal. It used to be the case that people encouraged suffices <what simp does to the goal today> by simpa but nowadays people seem to prefer simp? and then replacing simp? with its code action output.