# Functions and Inductive Propositions in Lean 4

Published on

Updated on

7 minute reading time

This blog post is inspired by the book Logical Foundations 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.

```
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. Instead, we can represent the collatz procedure as an inductive proposition.

```
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.

```
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.

```
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:

```
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`

.

```
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

```
#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: $$ \exists t, collatzfun(n , t) = some(r) \iff collatz(n, r) $$ 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.

```
theorem collatz_sound (n r : Nat) : (∃ t, collatz_fun n t = some r) → collatz n r := by
intro (H: ∃ t, collatz_fun n t = some r)
obtain ⟨t, H⟩ := H
revert H n r
show ∀ (n r : Nat), collatz_fun n t = some r → collatz n r
let motive := fun x : Nat => ∀ (n r: Nat), collatz_fun n x = some r → collatz n r
apply Nat.recOn (motive := motive) t
-- t = 0
case intro.zero =>
intro r n
intro (HFalse : collatz_fun r 0 = some n)
contradiction
-- t = S t1
case intro.succ =>
intro t
intro (IH : ∀ (n r : ℕ), collatz_fun n t = some r → collatz n r)
intro n r
intro (H : collatz_fun n (t + 1) = some r)
show collatz n r
unfold collatz_fun at H
-- Go into else case since (t1 + 1 ≠ 0)
simp [ite_false] at H
-- Consider each case for n
split at H
-- n = 0
case h_1 =>
-- H : some 0 = some r
have H : 0 = r := by
rewrite [Option.some.injEq] at H; assumption
suffices collatz 0 0 by
rewrite [<- H]; assumption
apply collatz.c0
-- n = 1
case h_2 =>
-- H : some 1 = some r
have H : 1 = r := by
rewrite [Option.some.injEq] at H; assumption
suffices collatz 1 1 by
rewrite [<- H]; assumption
apply collatz.c1
case h_3 N0 N1 =>
-- N0 : n ≠ 0
-- N1 : n ≠ 1
split at H
-- n % 2 = 0
case inl NE =>
-- NE : n % 2 = 0
-- H : collatz_fun (n / 2) t = some r
suffices collatz (n / 2) r by
apply collatz.ceven n r N0 NE; assumption
apply IH (n / 2) r H
-- n % 2 = 1
case inr NO =>
-- NO : n % 2 = 1
-- H : collatz_fun (3 * n + 1) t = some r
suffices collatz (3 * n + 1) r by
apply collatz.codd n r N1 NO; assumption
apply IH (3 * n + 1) r H
```