Intermediate Value Theorem

Stream: new members

[Elizabeth]

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

[Rob Lewis]

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]

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

[Elizabeth]

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]

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

[Johan Commelin]

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]

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]

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

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

[Johan Commelin]

@Elizabeth :up:

[Rob Lewis]

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]

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

[Johan Commelin]

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

Ah yes, that's what I want :D

[Johan Commelin]

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]

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

[Johan Commelin]

(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.]

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

[Johan Commelin]

Nice

[Jason KY.]

(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.]

Is there a way to make it go faster?

[Johan Commelin]

Ok, I see.

[Johan Commelin]

Do you have a pre-compiled mathlib?

[Johan Commelin]

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

[Jason KY.]

I believe so, yeah

[Jason KY.]

I followed all the steps on the website atleast

[Johan Commelin]

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

[Johan Commelin]

Unless your pc is > 10 yrs old.

[Jason KY.]

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

[Johan Commelin]

There is squeeze_simp to tell you what simp did

[Johan Commelin]

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

[Jason KY.]

Ah! I'm gonna try it out

[Jason KY.]

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

[Kevin Buzzard]

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]

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