The following document (15 pages) is an introduction to
the main features of Coq with included exercises.
Beginners with Coq should start with it. Doing all the exercises will take
more time than available for Coq-lab sessions: do not hesitate to
skip some of them.
This exercise show that the excluded middle implies proof-irrelevance.
We assume as an axiom that ∀ A, A ∨ ¬ A.
Show ∀ A, ¬ ¬ A → A.
Introduce BOOL of type Prop with two elements T and F.
Assume T≠ F, build f:Prop → BOOL such that
∀ A, A ↔ fA=T.
Load the module Hurkens in the standard library,
look at the type of theorem paradox. Deduce a proof of T=F.
Prove the proof-irrelevance property: ∀ (A:Prop) (pq:A),p=q.
The purpose of this exercise is to use Coq to verify the correctness
of a mini-compiler. The source language is a single expression
involving integer constants, variables and additions. The target
language is a assembly-like language with a single accumulator and an
infinite set of registers. A template file for this exercise is