Proving Theorems

and

Certifying Programs

with Coq

Stephan Boyer

@stepchowfun

Ask questions! Don’t be shy!

Logic

What’s a proof?

• Informally: an argument for the truth of a proposition
• Formally: a chain of applications of inference rules starting from axioms

Inference rules

Example: modus ponens

If A → B and A then B.

​

“→” means “implies”

Inference rules

Example: modus ponens

If Stephan is at LambdaConf

→ Stephan is in Boulder

and Stephan is at LambdaConf

then Stephan is in Boulder.

Programming

Inference rules

Example: function application

If f : A → B and x : A

then f(x) : B.

​

“→” is the type constructor for functions

Modus ponens ≅ function application

Modus ponens (logic)

​

If A → B and A

then B.

Application (programming)

​

If f : A → B and x : A

then f(x) : B.

Modus ponens ≅ function application

Modus ponens (logic)

​

If f : A → B and x : A

then f(x) : B.

​

f, x, and f(x) are proofs

Application (programming)

​

If f : A → B and x : A

then f(x) : B.

​

f, x, and f(x) are programs

Conjunctions ≅ products

Conjunction (logic)

​

If p : A ∧ B then p₁ : A.

If p : A ∧ B then p₂ : B.

​

p, p₁, and p₂ are proofs

Product (programming)

​

If p : (A, B) then p₁ : A.

If p : (A, B) then p₂ : B.

​

p, p₁, and p₂ are programs

Curry–Howard correspondence

Logic Programming

propositions ≅ types

proofs ≅ programs

Coq

Coq

“Rooster” in French

• A small pure functional programming language (Gallina)
• A scripting language for proof automation (Ltac)
• Proof scripts don’t need to be trusted!

Follow along: https://github.com/stepchowfun/coq-intro