Zulip Chat Archive

Stream: general

Topic: how to prove excluded middle (video)

view this post on Zulip Thorsten Altenkirch (Sep 27 2020 at 14:10):

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


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

view this post on Zulip Pedro Minicz (Sep 27 2020 at 17:47):

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

view this post on Zulip Junyan Xu (Sep 28 2020 at 05:12):

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.

Last updated: May 12 2021 at 05:19 UTC