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. PaperCoq
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. PaperCoq
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. PaperCoq
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. PaperCoq
Here we prove a disjunction (or) is left-distributive over conjunction (and). PaperCoq
In this video we prove Leibniz equality corresponds to Coq's equality. Coq