Zulip Chat Archive

Stream: new members

Topic: Intermediate Value Theorem


view this post on Zulip Elizabeth (Feb 12 2020 at 19:11):

Has anyone formalized the Intermediate Value Theorem on Lean? I'm confused about some steps of the proof :(

view this post on Zulip Rob Lewis (Feb 12 2020 at 19:34):

There are some versions of the IVT in this file here, but I'm not sure how explanatory they are: https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/ordered.lean

view this post on Zulip Rob Lewis (Feb 12 2020 at 19:34):

If you post some code, maybe we can give you specific advice.

view this post on Zulip Elizabeth (Feb 12 2020 at 19:44):

Well, I'm just revising for a test and confused for the proof my lecturer showed me, so I wonder if Lean could help to explain the idea more clearly. Anyway, thank you very much.

view this post on Zulip Johan Commelin (Feb 12 2020 at 19:45):

In principle, the answer should be yes. However, with the way mathlib works, I'm afraid it won't really work.

view this post on Zulip Johan Commelin (Feb 12 2020 at 19:45):

mathlib focuses on getting the most general statement with the shortest proof. So it doesn't aim for readability or explaining ideas/details.

view this post on Zulip Johan Commelin (Feb 12 2020 at 19:46):

In other words, all the information is there (there can't be any gaps in the proofs), but you'll probably have to work in order to understand what's going on.

view this post on Zulip Reid Barton (Feb 12 2020 at 20:01):

You could try applying a procedure like
(0. Obtain a built copy of mathlib)

  1. Find a theorem whose proof you want to understand. Probably is_connected_Icc is a good starting place.
  2. Open the file in an IDE, step through the lines of the tactic proof and watch how the tactic state changes. Ignore the actual tactics and try to justify the steps for yourself just looking at the tactic state.
  3. If there's a step you don't understand, hopefully the corresponding tactic names a relevant theorem. Look at the type of that theorem and if you don't understand why it is true then go back to step 1.

view this post on Zulip Jason KY. (Feb 12 2020 at 20:29):

Elizabeth, you're in my class right?
I have proved the intermediate value theorem in LEAN the same way our professor had taught us so it might be helpful?
Here it is (scroll down to line 237): https://github.com/JasonKYi/M4000x_LEAN_formalisation/blob/master/src/M40002/M40002_C5.lean

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:34):

@Elizabeth :up:

view this post on Zulip Rob Lewis (Feb 12 2020 at 20:34):

I think it's super cool that @Elizabeth even thought to ask this question, and even cooler that @Jason KY. has an answer!

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:38):

@Jason KY. Wow, that's a monster proof (-;

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:39):

Typo at https://github.com/JasonKYi/M4000x_LEAN_formalisation/blob/master/src/M40002/M40002_C5.lean#L453
You want -- closed interval is compact

view this post on Zulip Jason KY. (Feb 12 2020 at 20:40):

Ah yes, that's what I want :D

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:40):

Two remarks: (1) Do you know about the lean formatter that Patrick wrote? Kevin used it for the Sandwich theorem at some point.

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:41):

If you sprinkle some comments in your proofs, that could turn this into a beautiful page

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:42):

(2) Do you know about simp? You have lots of theorems of the form slightly_complicated = easier. If you tag them with @[simp] then the simplifier can use them when you call the simp tactic.

view this post on Zulip Jason KY. (Feb 12 2020 at 20:42):

Yeah! I formalised our intro module using it!
I think this was an earlier version
http://wwwf.imperial.ac.uk/~buzzard/M40001/html/M40001/M40001_4.html

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:43):

Nice

view this post on Zulip Jason KY. (Feb 12 2020 at 20:43):

(2) Do you know about simp? You have lots of theorems of the form slightly_complicated = easier. If you tag them with @[simp] then the simplifier can use them when you call the simp tactic.

I don't know why but simp seems to slow my pc down quite a lot so I try to avoid it.

view this post on Zulip Jason KY. (Feb 12 2020 at 20:43):

Is there a way to make it go faster?

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:43):

Ok, I see.

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:43):

Do you have a pre-compiled mathlib?

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:43):

I would assume so. I think otherwise you would see other slowdowns already.

view this post on Zulip Jason KY. (Feb 12 2020 at 20:44):

I believe so, yeah

view this post on Zulip Jason KY. (Feb 12 2020 at 20:44):

I followed all the steps on the website atleast

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:44):

I'm not an expert on such performance issues. But simp should make a pc so slow that it becomes annoying

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:45):

Unless your pc is > 10 yrs old.

view this post on Zulip Jason KY. (Feb 12 2020 at 20:46):

I normally just use simp and then convert it back with set_option trace.simplify.rewrite true so it becomes fast again

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:46):

There is squeeze_simp to tell you what simp did

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:47):

You can then call simp only [foo, bar] which is usually an order of magnitude faster than simp

view this post on Zulip Jason KY. (Feb 12 2020 at 20:47):

Ah! I'm gonna try it out

view this post on Zulip Jason KY. (Feb 12 2020 at 20:48):

Nice! That's way better than writing set_option trace.simplify.rewrite true every time

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 21:31):

Two remarks: (1) Do you know about the lean formatter that Patrick wrote? Kevin used it for the Sandwich theorem at some point.

Jason has written a bunch of stuff in the format of Patrick's formatter, but we couldn't get the formatter to work :-( https://github.com/leanprover-community/format_lean/issues/7

view this post on Zulip Elizabeth (Feb 12 2020 at 21:31):

OMG!!! Thank you very much!!! It really helps! (Good luck for tomorrow's test @Jason KY. :))))


Last updated: May 15 2021 at 00:39 UTC