Your First Proofs

A proposition is a type, and a proof is a value of that type.

13.1 The world of Prop

Ordinary programs use Bool for branching. In proofs, Prop describes the kind of propositions. P: Prop means that P is a proposition.

Just as x: A is a value of type A, if P is a proposition, p: P is its proof. This perspective is called the Curry–Howard correspondence.

import std::Base

theorem keep(A: Prop, p: A): A {
  p
}

// Return the evidence already supplied as an argument.

✓ theorem keep : ∀ A: Prop. (A) -> A

keep says that, given evidence p for A, you can return evidence for A. The body p already has the required type, making it a valid proof.

ok      keep

13.2 Build a proof of “and”

A ∧ B is a proposition containing evidence of both sides. AndIntro(a, b) combines two pieces of evidence. And::left and And::right extract the respective sides.

import std::Base

theorem and_swap(A: Prop, B: Prop, p: A ∧ B): B ∧ A {
  AndIntro(And::right(p), And::left(p))
}

// Project both pieces of evidence and rebuild them in reverse order.

✓ theorem and_swap : ∀ A: Prop. ∀ B: Prop. (And(A, B)) -> And(B, A)

Extract evidence for B and A from p, then rebuild it in the opposite order. Although the notation resembles mathematical prose, the result is a typed term.

13.3 Functions prove implication

import std::Base

theorem compose(
  A: Prop,
  B: Prop,
  C: Prop,
  f: (A) -> B,
  g: (B) -> C
): (A) -> C {
  a => g(f(a))
}

// Compose two implications as ordinary functions.

✓ theorem compose : ∀ A: Prop. ∀ B: Prop. ∀ C: Prop. ((A) -> B) -> ((B) -> C) -> (A) -> C

If f constructs evidence for B from evidence for A, and g constructs evidence for C from evidence for B, then a => g(f(a)) proves the implication from A to C. Function composition becomes a logical inference rule.

Exercise 13.1: What body proves (A) -> A?