## Stream: general

### Topic: Sanity check: error in textbook?

#### Jia Ming (Jan 26 2021 at 08:42):

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

#### Jia Ming (Jan 26 2021 at 08:42):

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 (Jan 26 2021 at 09:51):

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:

#### Jia Ming (Jan 26 2021 at 09:59):

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

#### Kyle Miller (Jan 26 2021 at 10:00):

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 (Jan 26 2021 at 10:38):

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,