Sanity check: error in textbook?

Stream: general

[Jia Ming]

I was reading Constructive Analysis by Errett Bishop and Douglas Bridger when I thought I noticed a tiny mistake in the inequalities of their very first proof of the textbook. I decided to formalize it in Lean just to make sure I'm not going crazy since this textbook is very old and extremely well regarded (it's a revision of Foundations of Constructive Analysis, which used the exact same proof). But in Lean it really looks like it doesn't work... Here's my lean proof (100 lines) and an extract from the textbook. Any critique of the style of my lean file will be gladly appreciated

https://gist.github.com/jiaminglimjm/5237c81909d638e0655dfae3eb320863
constructive_analysis_chap_2.jpg

[Jia Ming]

Can someone assure me that I've not gone mad? If the inequality underlined red in the picture was m > max{j, Nⱼ} the the proof would work. I commented the parts of the proof which would fail in the lean file, which should load with any decent version of mathlib.

[Kyle Miller]

You're right that there's a problem: if $j=m$ then the very last inequality is obviously false. If you change that last $<$ to a $\leq$, then everything is fine:

import tactic
import algebra.archimedean

def regular (x : ℕ → ℚ) : Prop :=
∀ m n, abs (x m - x n) ≤ (m + 1)⁻¹ + (n + 1)⁻¹

/-- Definition 2.1
A `myreal` number is a `regular` sequence of rational numbers -/
structure myreal :=
(seq : ℕ → ℚ) (reg : regular seq)

notation `ℜ` := myreal

namespace myreal

def eq_def (x y : ℜ) : Prop :=
∀ n, abs (x.seq n - y.seq n) ≤ 2 * (n + 1)⁻¹

notation x ` ≡ ` y := eq_def x y

/-- Helper lemma for demonstration below -/
lemma le_of_add_le_all' (x y : ℚ) : (∀ n : ℕ, x ≤ y + 3 * (n + 1)⁻¹) → x ≤ y :=
begin
  intro h,
  contrapose! h, -- Should be constructive since `rat.le` is decidable?
  cases exists_nat_one_div_lt (by linarith : 0 < (x - y) / 6) with n hn,
  use n,
  calc y + 3 * (n + 1)⁻¹
      = y + 3 * (1 / (n + 1)) : by ring
  ... < y + 3 * ((x - y) / 6) : by { apply add_lt_add_left _, rwa mul_lt_mul_left _, norm_num }
  ... = (x + y) / 2 : by ring
  ... < x         : by linarith,
end

/-- Lemma 2.3
Two `myreal` numbers `x` and `y` are equal if and only if for each natural
number `j` there exists a natural number `N` such that |xₙ - yₙ| ≤ j.succ⁻¹
for all `n ≥ N`. -/
lemma eq_iff (x y : ℜ) : x ≡ y ↔
  ∀ j : ℕ, ∃ N, ∀ n ≥ N, abs (x.seq n - y.seq n) ≤ (j + 1)⁻¹ :=
begin
  split,
  { intros heq j,
    use 2 * j + 1,
    intros n hn,
    apply le_trans (heq n),
    have pos : ∀ (k : ℕ), 0 < (k + 1 : ℚ),
    { norm_cast, exact nat.succ_pos },
    rw ←mul_le_mul_right (pos n),
    field_simp,
    rw mul_div_cancel,
    rw ←mul_le_mul_left (pos j),
    field_simp,
    rw mul_comm _ (n + 1 : ℚ),
    rw mul_div_cancel,
    repeat { norm_cast, linarith }, },
  intros h n,
  apply le_of_add_le_all',
  intro j,
  cases x, cases y, dsimp at *, unfold regular at *,
  cases h j with N hN,
  let m := max j N,
  specialize x_reg n m,
  specialize hN m (le_max_right _ _),
  specialize y_reg m n,
  have : ((m + 1)⁻¹ : ℚ) ≤ (j + 1)⁻¹,
  { field_simp only [nat.cast_succ],
    rw [div_le_iff _, div_mul_comm', mul_one, le_div_iff],
    { norm_cast, simp only [one_mul],
      linarith [le_max_left j N], },
    { exact_mod_cast nat.succ_pos _ },
    { exact_mod_cast nat.succ_pos _ }, },
  calc  abs (x_seq n - y_seq n)
      ≤ abs (x_seq n - x_seq m) +
        abs (x_seq m - y_seq n)   : abs_sub_le _ _ _
  ... ≤ abs (x_seq n - x_seq m) +
        (abs (x_seq m - y_seq m)+
         abs (y_seq m - y_seq n)) : add_le_add (le_refl _) (abs_sub_le _ _ _)
  ... ≤ (n + 1)⁻¹ + (m + 1)⁻¹ + (j + 1)⁻¹ + (m + 1)⁻¹ + (n + 1)⁻¹ : by linarith
  ... ≤ (n + 1)⁻¹ + (j + 1)⁻¹ + (j + 1)⁻¹ + (n + 1)⁻¹ + (j + 1)⁻¹ : by linarith
  ... = 2 * (n + 1)⁻¹ + 3 * (j + 1)⁻¹ : by { norm_cast, ring, }
end

end myreal

[Jia Ming]

awesomee, yeah that's another way to do it!

[Kyle Miller]

I'm guessing what happened is that they were thinking about how $2n^{-1}+3j^{-1}$ is bigger than $2n^{-1}$ and then accidentally wrote $<$.

[Kevin Buzzard]

Jia Ming said:

Any critique of the style of my lean file will be gladly appreciated

  contrapose! h, -- Should be constructive since `rat.le` is decidable?

#print axioms le_of_add_lt_all' tells you it isn't. Probably there will some theorem in logic.basic or whatever that you can apply explicitly which will invoke decidability.

by rw inv_nonneg; apply le_of_lt; exact_mod_cast nat.succ_pos n

The preferred style now is by {rw inv_nonneg, apply le_of_lt, exact_mod_cast nat.succ_pos n}

rw ←hm at *,

The preferred style now seems to be rw ← hm at *,

    { apply div_le_div,
      norm_num,
      norm_num,
      ...

It's considered bad style to just turn one goal into 4 and then knock them off. You might want to knock off e.g. the first proof with something like apply div_le_div (by norm_num), but this doesn't work, because of unification issues: when Lean reads by norm_num it doesn't know what the theorem it's supposed to be proving. This can be fixed by using refine instead of apply. You can first replace apply div_le_div with refine div_le_div _ _ _ _ and then fill in some of the _s with proofs. Mathlib would be much happier with this proof:

    { refine div_le_div (by norm_num) (by norm_num) _ _,
      { norm_cast, simp only [nat.succ_pos] },
      { norm_cast, linarith } },

    rw ← mul_one (2:ℚ),
    rw mul_assoc,
    rw one_mul,
    rw ← mul_add (2:ℚ) j 1,
    rw mul_div_mul_left,

Mathlib would prefer all those rewrites to be on one line.

  cases x, cases y, dsimp at *, unfold regular at *,

Non-terminal dsimps considered harmful (the behaviour might change in future versions of mathlib, meaning code can break in ways which are hard to explain). Use squeeze_dsimp to figure out what it's doing and then replace with dsimp only ... by clicking on the output. Except that for some reason it doesn't work here; squeeze_dsimp reports that dsimp only works, but it seems to break the proof :-/ An ugly fix is simp_rw [nat.succ_eq_add_one, nat.cast_add, nat.cast_one] at h and then dsimp only for the goal.

have : (m.succ⁻¹ : ℚ) < j.succ⁻¹,

Again in this subproof you climb up to three goals . I try to keep the number of goals down to one by killing easy subgoals ASAP, e.g.

  have : (m.succ⁻¹ : ℚ) < j.succ⁻¹,
  { rw (inv_lt_inv
      (show (0 : ℚ) < m.succ, by {norm_cast, simp})
      (show (0 : ℚ) < j.succ, by {norm_cast, simp})),
    norm_cast,
    simp only [nat.succ_eq_add_one],
    linarith [le_max_left j N],

[Patrick Massot]

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/intuitionistic.20logic/near/224013270. Trying to do intuitionistic math using mathlib is a very bad idea. You should start your own library, maybe in collaboration with Beeson or switch to Coq. We're happy to see you here, but we wouldn't enjoy seeing you suffering when fighting the whole of mathlib.

[Jia Ming]

Thank you very much for the feedback Prof Buzzard! And thanks for the intuitionistic thread Patrick Massot, though I'm still very much a beginner learning the maths hahah so I'll have to wait and see where it takes me