Proofs

In Pagda a type can be a statement, and a value of that type is a proof of it. This page shows how to state a fact and how to prove one, in Python syntax.

Statements as types

In an annotation, a == b is the type of proofs that a equals b. refl() is the proof that a thing equals itself. The checker works both sides out, so refl() proves any equation whose two sides come to the same thing.

def add(a: Nat, b: Nat) -> Nat:
    if a == 0:
        return b
    return add(a - 1, b) + 1


# a fact about add, for every n. The return type is the fact.
def add_zero(n: Nat) -> add(n, 0) == n:
    if n == 0:
        return refl()                      # add(0, 0) is 0 by working it out
    return cong(suc, add_zero(n - 1))      # the fact for n - 1 gives the fact for n


assert add(20, 22) == 42                   # worked out by the checker
print(add(20, 22), add_zero(7))

42 Refl()

add_zero has two cases. When n is 0, both sides work out to 0 and refl() is enough. Otherwise the recursive call proves the fact for n - 1, and cong(suc, ...) adds one to both sides of it. The checker also makes sure the recursion ends, which is what makes this a proof for every n.

Tests teach the checker

Inside if c: the checker replaces c by True in what is left to prove, and by False in the other branch. So a proof about a function that tests a < b can test a < b itself and finish each branch separately.

class Or[A, B](Data): ...


@constructor
def Left[A, B](a: A) -> Or[A, B]: ...


@constructor
def Right[A, B](b: B) -> Or[A, B]: ...


def larger(a: Nat, b: Nat) -> Nat:
    if a < b:
        return b
    return a


# larger(a, b) is always one of its two arguments
def larger_is_one(a: Nat, b: Nat) -> Or[Eq[larger(a, b), a], Eq[larger(a, b), b]]:
    if a < b:
        return Right(refl())
    return Left(refl())


print(larger(2, 5), larger_is_one(2, 5), larger_is_one(5, 2))

5 Right(Refl()) Left(Refl())

Or[A, B] is declared in the file: a proof of A or a proof of B. Inside a type, write Eq[x, y] for the statement x == y.

Getting the proof of a test

A test also gives a proof you can pass on. Inside if c: or while c:, known(c) is the proof that c is true. In the else part, known(not c) is the proof for the other way.

def at(xs: list[int], i: Nat, ok: (i < len(xs)) == True) -> int:
    return xs[i]                      # no test needed: the caller proved it


def third_or_zero(xs: list[int]) -> int:
    if 2 < len(xs):
        return at(xs, 2, known(2 < len(xs)))
    return 0


print(third_or_zero([7, 8, 9]), third_or_zero([7]))

9 0

A parameter whose type is c == True works the other way round: inside the def, the checker treats c as known.

Impossible cases

Some types have no values. Fin[n] is a number below n, so Fin[0] is empty. A match on such a value has nothing to handle, and case _: return unreachable() says so. The checker accepts it only when it can see that no value gets there.

class Vec[A, n: Nat](Data): ...


@constructor
def Nil[A]() -> Vec[A, 0]: ...


@constructor
def Cons[A, n: Nat](head: A, tail: Vec[A, n]) -> Vec[A, n + 1]: ...


class Fin[n: Nat](Data): ...          # a number below n


@constructor
def FZ[n: Nat]() -> Fin[n + 1]: ...


@constructor
def FS[n: Nat](before: Fin[n]) -> Fin[n + 1]: ...


def lookup[A, n: Nat](xs: Vec[A, n], i: Fin[n]) -> A:
    match xs:
        case Cons(x, rest):
            match i:
                case FZ():
                    return x
                case FS(j):
                    return lookup(rest, j)


def nothing_below_zero[A](i: Fin[0]) -> A:
    match i:
        case _:
            return unreachable()


v: Vec[str, 3] = Cons("a", Cons("b", Cons("c", Nil())))
print(lookup(v, FZ()), lookup(v, FS(FS(FZ()))))

a c

lookup has no case for an empty vector. An index of type Fin[n] into a Vec[A, n] cannot be out of range, and the checker sees that the missing case cannot happen.

Function types that mention their argument

Fn[A, B] is the type of functions from A to B. An argument can be named, and the types after it can then use the name. That is enough to write induction itself as a def:

def induction(P: Fn[Nat, Type], base: P(0), step: Fn[k: Nat, P(k), P(k + 1)], n: Nat) -> P(n):
    if n == 0:
        return base
    return step(n - 1, induction(P, base, step, n - 1))


def plus_zero(n: Nat) -> n + 0 == n:
    return induction(lambda k: Eq[k + 0, k], refl(), lambda k, h: cong(suc, h), n)


print(plus_zero(4))

Refl()

The step takes a number k and a proof of P(k), and gives a proof of P(k + 1).

Ready-made proofs

lemmas is a checked file that ships with Pagda. It holds facts about numbers, < and lists. Import the ones you need by name.

from lemmas import plus_comm, len_append


def swap(a: Nat, b: Nat) -> a + b == b + a:
    return plus_comm(a, b)


def joined(xs: list[str], ys: list[str]) -> len(xs + ys) == len(xs) + len(ys):
    return len_append(xs, ys)


print(swap(2, 3), joined(["a"], ["b", "c"]))

Refl() Refl()

While loops

A while loop outside the two shapes the checker handles by itself ends with decreases(measure, proof). The measure is a Nat worked out from the loop's variables. The proof shows that the measure at the end of a pass is smaller than it was at the start.

from lemmas import down_step


def halvings(n: Nat) -> Nat:
    steps = 0
    left = n
    while 0 < left:
        was = left
        left = monus(left, 1)
        steps += 1
        decreases(left, down_step(was, known(0 < was)))
    return steps


print(halvings(4))

4

Here the measure is left itself. was remembers its value at the start of the pass, known(0 < was) is the loop's own test, and down_step turns those into the proof.

Working with holes

Proofs are written a piece at a time. Put hole() where you are stuck and run the checker. It reports the type the hole needs and the names you can build it from.

def plus_zero(n: Nat) -> n + 0 == n:
    if n == 0:
        return refl()
    return cong(suc, hole())

  File "t10_hole.py", line 8
    return cong(suc, hole())
TypeCheckError: this file has 1 hole, so it was not run.
line 8: hole() needs a value of type
  n₁ + 0 ≡ n₁
with these names to build it from:
  n₁ : Nat

Here the hole needs n₁ + 0 ≡ n₁, where n₁ is n - 1. That is the fact itself for a smaller number, so the answer is the recursive call plus_zero(n - 1).

What proofs cannot reach yet

• A property of a loop's result. Write the loop as a recursive def to prove something about it.
• Types of types beyond the first level. A constructor field cannot hold a type.
• Explicit type arguments at a call. The checker always works them out.