Zulip Chat Archive

Stream: general

Topic: Sanity check: error in textbook?


view this post on Zulip 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

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

view this post on Zulip 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.

view this post on Zulip Kyle Miller (Jan 26 2021 at 09:51):

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

view this post on Zulip Jia Ming (Jan 26 2021 at 09:59):

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

view this post on Zulip Kyle Miller (Jan 26 2021 at 10:00):

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

view this post on Zulip 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,
    simp only [nat.succ_eq_add_one],
    linarith [le_max_left j N],

view this post on Zulip Patrick Massot (Jan 26 2021 at 10:42):

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.

view this post on Zulip Jia Ming (Jan 26 2021 at 10:51):

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


Last updated: May 10 2021 at 17:39 UTC