Unconference Coq
summary
Proofs are built interactively: start with a goal like n + 0 = n, use intro/induction/simple/reflexivity tactics to move variables, reduce and close base cases, then apply the induction hypothesis and rewrite to finish. Equality is the inductive EQ type with eq_refl constructor and rewrite uses its induction principle. Examples show when one direction reduces by definition and when double induction (or a lemma) is needed; the demos complete, including a worked proof that addition is commutative.
AI-written summary · about
chapters (8)
- 0:00Start
- 0:15Example of a Proof
- 4:56The Induction Principle for Natural Numbers
- 29:54Definitional Equality
- 30:17Liveness Equality
- 31:29Induction Principle
- 32:18The Induction Principle
- 49:24Proof by Contradiction
related talks
01h 34mFormal Logic Undressed
35mHow to make ad hoc proof automation less ad hoc
35mUsing the Design Recipe in Theory of Computation
30mThe conatural numbers form an exponential commutative semiring
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
42mLive-Coding Mathematics Your First Clojure Proof
21mWell-founded recursion done right
52mWhat logic can teach us, Scala programmers