Short introduction by example to Coq1 Proof assistants are computer programs that help mathematicians to prove theorems and to formally verify the correctness of proofs. Proof assistants are nowadays one of the more exciting areas in the intersection of mathematical logic and computer science. For example, one particularly exciting achievement is the formal veri cation of the proof of the four colour theorem using the proof assistant Coq.
y ^
y , x < y _ x = y We divide the talk into the following four parts. Introduction to Coq We explain, by means of the theorems mentioned, that to formalise a proof in Coq we need to tell Coq the following four things.
Language For example, to introduce a binary relation S on N by the code Variable S : nat -> nat -> Prop and to introduce another binary relation N on N de ned as N (x; y) , S(x; y)_x = y by the code Definition N x y := S x y \/ x = y.
Axioms For example, to introduce the irre exivity axiom 8x 2 N :S(x; x) by the code Axiom irreflexivity : forall x : nat, ~S x x. Theorem For example, to introduce the re exivity theorem 8x 2 N N (x; x) by the code Theorem reflexivity : forall x : nat, N x x. Proof For example, to introduce the proof \take x, unfold N (x; x) into S(x; x) _ x = x, prove the right part x = x by the re exivity of =" of the re exivity theorem by the codes \intro x, unfold N, right, reflexivity".
Achievements of Coq We discuss what is achieved with this kind of formal veri cation.
Applications of Coq to education We address the application of Coq to education by mentioning how we can use Coq to learn the following topics.
Arithmetic For example, Peano arithmetic.
Algebra For example, group theory.
Geometry For example, Euclidean geometry.
Set theory For example, Zermelo-Fraenkel set theory.
Practical aspects We address the following practical aspects of Coq.
Using Coq How to use Coq online (no installation needed) and o ine (installation needed).
Tutorials Where to nd tutorials and manuals for Coq to learn more.
Formalising ZF
ZF" in Coq2
Jean-Louis Krivine [
ZF").
ZF" (that is, every theorem of ZF is also a theorem of
In this talk we present a little formalisation in Coq (a proof assistant) of Krivine's proof of ZF ZF". Admittedly, we are hoping for comments from Coq experts to help us to write a short article about the formalisation. The talk is divided into the following four parts.
Introduction to ZF" We brie y introduce ZF" along the lines above. Introduction to Coq example of a theory.
We brie y introduce Coq by means of a very simple Language The theory has a language with propositional variables P and Q.
Axioms The theory has the axioms P and P ) Q.
Theorem The theory proves the theorem Q.
Proof The theory proves Q by the proof \by the axiom P ) Q, to prove Q su ces to prove P , which is an axiom".
Formalisation of ZF ZF" in Coq We present our formalisation by showing key bits of the Coq code.
Language For example, the set membership " is introduced by the code Parameter epsilon : Set -> Set -> Prop.
Axioms For example, the axiom of pairing of ZF" is introduced by the code Axiom Pair : forall a b : Set, exists c : Set, a " c /\ b " c. 2Keywords: Coq; proof assistant; formal veri cation; ZF"; ZF; set theory. Theorem For example, the theorem of paring of ZF is introduced by the code Theorem Pair : forall a b : Set, exists c :
Set, a 2 c /\ b 2 c.
Proof For example, the theorem of pairing of ZF is proved by some code Proof : : : Qed that is a bit complicated so we omit it here. Contributions and problems We brie y discuss contributions to education and technical problems of our formalisation.
Contributions For example, the extremely detailed level of the formalisation provides a good exercise in applying the axiom schema of comprehension.
Problems For example, we added new axioms to Coq, and this raises the question of whether Coq with those new axioms is consistent.