To do: Include general info about ICL and a link to the script/book.
Introductory Videos
The following videos work through several examples of proofs both informally and in the proof assistant Coq.
In the first videos we describe how to prove addition on the natural numbers is commutative.
This also serves as a first simple example for proving in the system Coq.
We next describe how proofs can be represented as certain kinds of terms.
We prove a few simple propositions and then look at the corresponding proof terms.
We then work through the same examples in Coq.
In these videos we again prove a simple proposition and look at the corresponding proof term.
Unlike the examples above, the example here contains a universal quantifier which must be
instantiated during the proof.
Here we prove that the triple negation of a proposition implies the single negation of a proposition.
We also look at the corresponding proof term.
Here we prove a disjunction (or) is left-distributive over conjunction (and).
In this video we prove Leibniz equality corresponds to Coq's equality.
Finally, we prove the surjective Cantor theorem.
In addition to streaming them via youtube, you have the option of downloading the video files to watch or rewatch
when you are offline.