title: "Functions and Inductive Propositions in Lean 4"
date: 2024-04-14T19:25:52-04:00
draft: false
tags: ["Formal Methods"]
math: true
medium_enabled: false
---
This blog post is inspired by the book [Logical Foundations](https://softwarefoundations.cis.upenn.edu/lf-current/index.html) where it goes over similar content in the Coq proof assistant. Instead, we will look at Lean 4.
Functions in Lean are required to be total and terminating. This means that there are some mathematical functions that cannot be represented. An example of which is the collatz conjecture.
```lean
def collatz_fail (n : Nat) : Nat :=
match n with
| (0: Nat) => (0: Nat)
| (1: Nat) => (1: Nat)
| x =>
if x % 2 = 0 then collatz_fail (x / 2)
else collatz_fail (3 * x + 1)
```
If you type the above function in Lean, you'll get the following error:
```
fail to show termination for
collatz_fail
```
I can't tell you how we would go about showing termination. After all, many brilliant mathematicians are attempting to solve this [conjecture](https://en.wikipedia.org/wiki/Collatz_conjecture). Instead, we can represent the collatz procedure as an inductive proposition.
```lean
inductive collatz : Nat → Nat → Prop where
| c0 : collatz 0 0
| c1 : collatz 1 1
| ceven (n r : Nat) : ¬(n = 0) → n % 2 = 0 → collatz (n / 2) r → collatz n r
| codd (n r : Nat) : ¬(n = 1) → ¬(n % 2 = 0) → collatz (3 * n + 1) r → collatz n r
```
Our inductive proposition `collatz` is built with the first argument representing our input `n` and the second argument representing the result. Note that the first two constructors `c0` and `c1` denote the base cases. The second two constructors `ceven` and `codd` have various conditions on them:
- For `ceven`, we first require that $n \ne 0$, and that $n$ is even. If that's the case, then whatever `r` is in the inductive proposition `collatz (n / 2) r`, that `r` will be the result in `collatz n r`.
- Similarly, for `codd`, the inductive proposition requires that $n \ne 1$ and that $n$ is odd. Then `r` holds whatever value `collatz (3 * n + 1) r` holds.
To use this inductive proposition, we need to build up a proof.
```lean
example : collatz 5 1 := by
apply collatz.codd; trivial; trivial
show collatz 16 1
apply collatz.ceven; trivial; trivial
show collatz 8 1
apply collatz.ceven; trivial; trivial
show collatz 4 1
apply collatz.ceven; trivial; trivial
show collatz 2 1
apply collatz.ceven; trivial; trivial
show collatz 1 1
apply collatz.c1
```
For inductive propositions, Lean does not require that it's definition is total or terminating. In fact, in general perhaps a different ordering of constructors can be called in order to produce two different results for `r`! Our specific definition, however, only produces one `r` for a given `n`, and we can prove that in Lean.
```lean
theorem collatz_deterministic (n r1 r2: Nat) (H1: collatz n r1) (H2: collatz n r2) : r1 = r2 := by
revert r2
-- Look at each of the possible
-- constructors for collatz
induction H1
case c0 =>
intro r
intro (H: collatz 0 r)
cases H
case c0 => rfl
-- automatically detects c1 as a contradiction
case ceven => contradiction
case codd => contradiction
case c1 =>
intro r
intro (H: collatz 1 r)
cases H
-- automatically detects c0 as a contradiction
case c1 => rfl
case ceven => contradiction
case codd => contradiction
case ceven n r1 N0 NE H IH =>
-- N0 : n ≠ 0
-- NE : n % 2 = 0
-- IH : ∀ (r2 : ℕ), collatz (n / 2) r2 → r1 = r2
intro r2
intro (H: collatz n r2)
cases H
case c0 => contradiction
case c1 => contradiction
case ceven H2 => apply IH r2 H2
case codd => contradiction
case codd n r1 N1 NO H IH =>
-- N1 : n ≠ 1
-- NO : n % 2 = 1
-- IH : ∀ (r2 : ℕ), collatz (3 * n + 1) r2 → r1 = r2
intro r2
intro (H: collatz n r2)
cases H
case c0 => contradiction
case c1 => contradiction
case ceven => contradiction
case codd H2 => apply IH r2 H2
```
This means that we don't have to worry about calling the wrong constructor. If it fails, we backtrack and try a different one. This leads to an effective proof strategy:
```lean
example : collatz 5000 1 := by
repeat (first |
apply collatz.c0 |
apply collatz.c1 |
apply collatz.codd; trivial; trivial; simp |
apply collatz.ceven; trivial; trivial; simp
)
```
Let's return to our function `collatz_fail`. The reason this function didn't work is that it wasn't obvious that the function terminates. We can force it to terminate by introducing a new variable `t` that denotes the number of remaining steps before giving up and returning `none`.
```lean
def collatz_fun (n t : Nat) : Option Nat :=
if t = 0 then none else
match n with
| (0: Nat) => (0: Nat)
| (1: Nat) => (1: Nat)
| x =>
if x % 2 = 0 then collatz_fun (x / 2) (t - 1)
else collatz_fun (3 * x + 1) (t - 1)
```
Instead of having to do the proof search from above, we can call `eval` on this function
```lean
#eval collatz_fun 5 6
#eval collatz_fun 5000 29
```
Is there any relationship between the inductive proposition version and the function we just built? Ideally we would want to prove the following relationship:
Since we don't know how to show whether collatz terminates, we can't at this time prove the backwards direction. We can, however, prove the forward direction through induction on the number of steps.
```lean
theorem collatz_sound (n r : Nat) : (∃ t, collatz_fun n t = some r) → collatz n r := by
