Interactive Theorem Proving

The era of automated and interactive theorem proving is here. We have a unique opportunity to meaningfully advance the human understanding of and trust in mathematics. In this article we'll define the natural numbers inductively, the addition function recursively, and prove its group theoretic algebraic structures in Lean 4.

Group Theoretic Structures

We start with declaring group theoretic structures along with their properties. This enables a template such that the Natural number type can implement the type classes if and only if we can prove the properties at compile time.

namespace Grp

  variable (α : Type u)

  class Magma where
    op : α → α → α

  class Semigroup extends Magma α where
    associativity : ∀ (a b c : α), op (op a b) c = op a (op b c)

  class Monoid extends Semigroup α where
    identity_element : α
    identity_left : ∀ (a : α), op identity_element a = a
    identity_right : ∀ (a : α), op a identity_element = a

  class Group extends Monoid α where
    inverse : α → α
    inverse_left : ∀ (a : α), op (inverse a) a = identity_element
    inverse_right : ∀ (a : α), op a (inverse a) = identity_element

end Grp

We scope everything to the `Grp` namespace.

The variable alpha is defined as a generic type in a generic universe. If you're not familiar with lean semantics, just treat this as a generic type. We define this here so we can reference alpha directly as a type parameter in the subsequent type classes.

Group theory is beyond the scope of this article (you can find a speed run of that (here). But notice how in the Monoid type class that the first element is of type alpha but the second and third contain some unusual notation. In both of these, the `=` is not actually "assignment" in the programatic sense, it is equivalence in the mathematical sense. For example, the `identity_left` "type" is actually a proposition, it declares that in order for some type, alpha, to implement the Monoid type class, the implementor has to prove that for each element "a" in alpha, the operation "op" applied to the identity element and "a" must be equal to "a". Aka:

\(\forall a \in \alpha : op(e, a) = a\)

Notice also how each type class extends the previous, that is to say a type, alpha, may not implement Semigroup without first implementing Magma.

Natural Numbers

We define the natural numbers as an inductive aka recursive sum type. The natural numbers are either zero or the successor of another natural number. This enables a theoretic construction of the infinite set of natural numbers `[0, ∞)`.

inductive Natural : Type
  | zero
  | successor : Natural → Natural

open Natural

We follow the definition with the `open Natural` command to enable the use of `zero` and `successor` without the `Natural` namespace prefix. Consider it syntax sugar.

Addition

We define the addition of natural numbers recursively. The addition of zero and any term `n` of type Natural returns `n`. The addition of the successor of `m` and `n` returns the successor of the sum of `m` and `n`.

That is to say, either we add zero to a number or we recursively transform the nonzero left hand input toward zero until we reach the base case of zero.

def Natural.add : Natural → Natural → Natural
  | zero, n => n
  | successor m, n => successor (Natural.add m n)

Theorems

The Curry-Howard correspondence is a correspondence between programs and proofs. That is to say given a type and a term aka element of that given type, we can consider the type a proposition and its term as a proof. The type is a proposition that there exists some term with this type, that this type is constructible in some way. The term is a proof that the type can and does in fact exist.

To prove theorems, we use keywords known as tactics which represent common strategies for progressing a proposition aka goal to its proof. Given an equivalence relation between two different terms, we have to transform either or both sides through other known proofs or hypotheses until they are identical. We use two tactics in this article.

1. `rw [hypothesis]` which rewrites or substitutes a pattern in the goal with an equivalence defined by a hypothesis, proof, or axiom.

2. `induction n with ...` which attempts to prove by induction. Using Natural, we prove the base case `zero` then we prove `successor n` with the hypothesis that the proposition holds for `n`.

Add Zero

Adding any element of type Natural to zero returns the element. That is to say `add n zero = n`.

We prove this by induction, first demonstrating the zero case through equality, then the successor case with the hypothesis that the theorem holds for an arbitrary natural number.

Note: In Lean4, `--` is the comment prefix, these lines are ignored by the compiler.

theorem Natural.add_zero (n : Natural) : Natural.add n zero = n := by
  -- goal: `n + zero = n`
  -- tactic: prove by induction on `n`
  induction n with

  -- base case: `zero`
  | zero =>
    -- goal: `zero + zero = zero`
    -- tactic: rewrite `zero + zero` to `zero`
    --   with `Natural.add`
    rw [Natural.add]

  -- inductive case: `successor m` with hypothesis
  -- `hypothesis_n : m + zero = m`
  | successor m hypothesis_n =>
    -- goal: `successor m + zero = successor m`
    -- tactic: rewrite `successor m + zero` to `successor (m + zero)` with `Natural.add`
    rw [Natural.add]
    -- goal: `successor (m + zero) = successor m`
    -- tactic: rewrite `m + zero` to `m` with `hypothesis_n`
    rw [hypothesis_n]

Zero Add

Adding zero to any element of type Natural returns the element. That is to say `add zero n = n`.

The ordering of variables to a function matter unless proven otherwise. We prove both orderings of adding the identity element to another element are equivalent, but with other types this may not always be the case.

Note that we can prove this by simply rewriting via the definition of addition. This is because the zero case of addition (`| zero, n => n`) definitionally proves this.

theorem Natural.zero_add (n : Natural) : Natural.add zero n = n := by
  -- goal: `zero + n = n`
  -- tactic: rewrite `zero + n` to `n` with `Natural.add`
  rw [Natural.add]

Add is Associative

Addition of natural numbers is associative.

We prove this by induction, first demonstrating the zero case through the previously proven `zero_add` theorem, then the successor case with the hypothesis that the theorem holds for an arbitrary natural number.

theorem add_is_associative (a b c : Natural) :
    Natural.add (Natural.add a b) c =
      Natural.add a (Natural.add b c) := by

  -- goal: `a + b + c = a + (b + c)`
  -- tactic: prove by induction on `a`
  induction a with

  -- base case: `zero`
  | zero =>
    -- goal: `zero + b + c = zero + (b + c)`
    -- tactic rewrite `zero + b` to `b` with `Natural.zero_add`
    rw [Natural.zero_add]
    -- goal: `b + c = zero + (b + c)`
    -- tactic: rewrite `zero + (b + c)` to `b + c`
    --     with `Natural.zero_add`
    rw [Natural.zero_add]

  -- inductive case: `successor m` with hypothesis
  --     `hypothesis_n : n + b + c = n + (b + c)`
  | successor n hypothesis_n =>
    -- goal: `successor n + b + c = successor n + (b + c)`
    -- tactic: rewrite `successor n + b` to `successor (n + b)`
    --     with `Natural.add`
    rw [Natural.add]
    -- goal: `successor (n + b) + c = successor n + (b + c)`
    -- tactic: rewrite `successor n + (b + c)` to
    --     `successor (n + (b + c))` with `Natural.add`
    rw [Natural.add]
    -- goal: `successor (n + b + c) = successor n + (b + c)`
    -- tactic: rewrite `n + b + c` to `n + (b + c)` with `Natural.add`
    rw [Natural.add]
    -- goal: `successor (n + b + c) = successor (n + (b + c))`
    -- tactic: rewrite `n + (b + c)` to `n + b + c` with `hypothesis_n`
    rw [hypothesis_n]

Type Class Instances

We define instances of the group theoretic type classes with the natural numbers and the addition operation.

Since we have the `zero_add`, `add_zero`, and `add_is_associative` theorems proven, we can satisfy the constraints of each structure except Group.

instance : Grp.Magma Natural where
  op := Natural.add

instance : Grp.Semigroup Natural where
  associativity := add_is_associative

instance : Grp.Monoid Natural where
  identity_element := zero
  identity_left := Natural.zero_add
  identity_right := Natural.add_zero

instance : Grp.Group Natural where
  inverse := sorry
  inverse_left := sorry
  inverse_right := sorry

The natural numbers with addition do not form a Group. This is because the natural numbers with addition do not have inverses. Thus we use the `sorry` tactic for each; these are generally used for temporary placeholders in proofs that are not yet implemented. Here we use them to have the compiler generate a warning instead of an error.

To construct a Group with addition, we would need either the Integer type which admits negative numbers or a set of GaloisField elements which perform addition modulo a prime number.

Conclusion

This is a high level, example driven demonstration of the Lean4 interactive theorem prover. There are plenty of details that have been glossed over, so if you are interested in learning more, consider reading the functional programming and theorem proving mdbooks on Lean 4. Additionally, there is a more thorough implementation of the code snippets from this article on my GitHub.

• https://lean-lang.org/functional_programming_in_lean/introduction.html

• https://lean-lang.org/theorem_proving_in_lean4/title_page.html

• https://github.com/jtriley-eth/naturals-lean

Until next time!