Contents Previous Next


Proofs as data

In type theory, mathematical proofs take a different course than the ones we’re generally familiar with. Since in type theory everything, including proofs themselves, are types, the correctness of a proof translates to the ability to create an object of that proof’s type. In simpler terms, if one claims a proposition, one has to show the proposition (which is a type) is valid. A type can be shown to be valid if one can construct an object of that type. Thus, in order to prove something, we need to create an object having the type of the proposition.

Propositions can be defined in a recursive way such that termination of computation proves the correctness of the proof. We recursively dismantle the input until the trivial case is left which completes the recursion process and our proof is done. This also implies that in cases where termination is not reached, one can say that the proof does not apply to, or, is invalid for such inputs.

Usually, a proof consists of: - trivial cases, serving as termination markers - recursive pattern matchers, for (de) constructing the proof from (to) the trivial cases

module Types.proofsAsData where

open import Lang.dataStructures

Order

For example, the <= operator can be defined as consisting of two constructors:

After applying lz sufficient number of times, if we end up at 0 <= x where ltz is invoked, computation terminates and our theorem is proved.

data _<=_ : Set where
  ltz : {n :}  zero <= n
  lt : {m :}  {n :}  m <= n  (succ m) <= (succ n)

infix 4 _<=_

Some examples:

idLess₁ : one <= ten
idLess₁ = lt ltz

idLess₂ : two <= seven
idLess₂ = lt (lt ltz)

idLess₃ : three <= nine
idLess₃ = lt (lt (lt ltz))

If we try to compile something that is not true, the compiler will throw an error:

idLess' : ten <= three
idLess' = lt lt lt lt lt lt lt lt lt ltz
proofsAsData.lagda.md:68,14-16
(_m_30 <= _n_31 → succ _m_30 <= succ _n_31) !=< (nine <= two) of
type Set

Odd or Even

The odd or even proofs can be defined as in the previous proof. Here we successively decrement n till we:

data Even : Set
data Odd : Set

data Even where
  zeroIsEven : Even zero
  succ : {n :}  Even n  Even (succ (succ n))

data Odd where
  oneIsOdd : Odd one
  succ : {n :}  Odd n  Odd (succ (succ n))

by which we could prove:

twoisEven : Even two
twoisEven = succ zeroIsEven

isFourEven : Even four
isFourEven = succ (succ zeroIsEven)

isSevenOdd : Odd seven
isSevenOdd = succ (succ (succ oneIsOdd))

Equality of natural numbers

Equality of natural numbers can be proven by successively comparing decrements of them, till we reach 0 = 0. Else the computation never terminates:

data __ : Set where
  eq₀ : zero ≡ zero
  eq :  {n m}  (succ n)(succ m)

Similar for not equals:

data __ : Set where
  neq₀ :  n  n ≠ zero
  neq₁ :  m  zero ≠ m
  neq :  { n m }  (succ n)(succ m)

Belongs to

To prove that a particular element of type A belongs to a list List' of type A, we require:

where list₁ is list without y.

data __ {A : Set}(x : A) : List A  Set where
  refl :  {xs}  x ∈ (x :: xs)
  succ∈ :  {y xs}  x ∈ xs  x ∈ (y :: xs)

infixr 4 __

Example:

theList : List ℕ
theList = one :: two :: four :: seven :: three :: []

threeIsInList : three ∈ theList
threeIsInList = succ∈ (succ∈ (succ∈ (succ∈ refl)))

Curry-Howard Isomorphism

The relationship we saw earlier between formal proofs and computer programs is called the Curry-Howard isomorphism, also known as the Curry-Howard correspondence. This states that a proof is a program and the formula it proves is the type of the program. Broadly, they discovered that logical operations have analogues in types as can be seen below:

Type Theory Logic
A proposition
x : A proof
ϕ, 1 ⟂, ⊤
A × B A ∧ B (and / conjunction)
A + B A ∨ B (or / disjunction)
A → B A ⟹ B (implication)
x : A ⊢ B(x) predicate
x : A ⊢ b : B(x) conditional proof
\(\Pi_{x:A} B(x)\) ∀ x B(x)
\(\Sigma_{x:A} B(x)\) ∃ x B(x)
\(p : x =_A y\) proof of equality
\(\Sigma_{x,y:A} x =_A y\) equality relation

Thus, type theory can be considered a proof writing system in a standard programming language as an alternative to formal logic. This essentially open up a new medium of doing mathematics as well will be seeing in subsequent sections.


Kinds of Type Theories