how to prove excluded middle (video)

Stream: general

[Thorsten Altenkirch]

I gave a talk with live proofs in our fp lunch meeting last Friday using lean for the first time:

https://youtu.be/SJ-_zqw5UHk

Sorry for the low level of automatisation but this is the style I am also using in my lecture. The main story is that you don't need to assume EM as an axiom but there is also some discussion about lean...

[Pedro Minicz]

Very interesting! This remembers me of the "stable propositions" exercise at the end of the negation chapter of Programming Language Foundations in Agda. Coincidentally, I have redone the exercise in Lean around a week ago (you can see it here).

[Junyan Xu]

Coincidentally I also did some similar exercises regarding stable propositions (which corresponds to regular elements in Heyting algebras): https://gist.github.com/alreadydone/7474d5000c912194d794d06192e84f1e#file-choice_and_excluded_middle-lean-L557
Basically I formalized https://en.wikipedia.org/wiki/Heyting_algebra#The_De_Morgan_laws_in_a_Heyting_algebra in Lean.