## Stream: new members

### Topic: Intermediate Value Theorem

#### 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 :(

#### 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

#### Rob Lewis (Feb 12 2020 at 19:34):

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

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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

@Elizabeth :up:

#### 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!

#### Johan Commelin (Feb 12 2020 at 20:38):

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

#### 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

#### Jason KY. (Feb 12 2020 at 20:40):

Ah yes, that's what I want :D

#### 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.

#### Johan Commelin (Feb 12 2020 at 20:41):

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

#### 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.

#### 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

Nice

#### 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.

#### Jason KY. (Feb 12 2020 at 20:43):

Is there a way to make it go faster?

Ok, I see.

#### Johan Commelin (Feb 12 2020 at 20:43):

Do you have a pre-compiled mathlib?

#### Johan Commelin (Feb 12 2020 at 20:43):

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

#### Jason KY. (Feb 12 2020 at 20:44):

I believe so, yeah

#### Jason KY. (Feb 12 2020 at 20:44):

I followed all the steps on the website atleast

#### 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

#### Johan Commelin (Feb 12 2020 at 20:45):

Unless your pc is > 10 yrs old.

#### 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

#### Johan Commelin (Feb 12 2020 at 20:46):

There is squeeze_simp to tell you what simp did

#### 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

#### Jason KY. (Feb 12 2020 at 20:47):

Ah! I'm gonna try it out

#### Jason KY. (Feb 12 2020 at 20:48):

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

#### 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

#### 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