Short Introduction by Example to Coq and Formalising ZF ⊆ ZF ε in Coq.
Jaime Gaspar · 2014
1 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 mathe-matical logic and computer science. For example, one particularly exciting achievement is the formal verification of the proof of the four colour theorem using the proof assistant Coq. In this talk we give a very elementary introduction to Coq by means of a very simple example, namely the proofs of the following theorems. • If ≤ is a non-strict partial order, then < defined by x < y ⇔ x ≤ y ∧ x 6 = y is a strict partial order. • If < is a strict partial order, then ≤ defined by x ≤ y ⇔ x < y∨x = y is a non-strict partial order. We divide the talk into the following four parts.