# The equation compiler and WellFoundedRelation #

To define functions and proofs recursively you can use the equation compiler, if you have a well founded relation on that type

For example the definition of gcd on naturals uses well founded recursion

```
def gcd (m n : Nat) : Nat :=
if m = 0 then
n
else
gcd (n % m) m
termination_by m
decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
```

Because < is a well founded relation on naturals, and because `¬m = 0 → n % m < m`

this recursive function is well-founded.

Whenever you use the equation compiler, there will be a default well founded relation on the type being recursed on (given by the `WellFoundedRelation`

instance) and the equation compiler will automatically attempt to prove the function is well founded under said relation.

When the equation compiler fails, there are two main causes.

- It could not find a decreasing measure.
- It has failed to prove the required inequality.

## Proving required inequality #

If we modify the gcd example above, by removing the `termination_by`

& `decreasing_by`

, we get an error.

```
def gcd (m n : Nat) : Nat :=
if m = 0 then
n
else
gcd (n % m) m
```

```
fail to show termination for
Nat.gcd
with errors
argument #1 was not used for structural recursion
failed to eliminate recursive application
(n % m).gcd m
argument #2 was not used for structural recursion
failed to eliminate recursive application
(n % m).gcd m
structural recursion cannot be used
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
m n
1) 93:4-18 ? ?
Please use `termination_by` to specify a decreasing measure.
```

The error message says us to use `termination_by`

to specify decreasing measure, so we use `m`

as a decreasing measure, but we get an another error.

```
def gcd (m n : Nat) : Nat :=
if m = 0 then
n
else
gcd (n % m) m
termination_by m
```

```
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
m n : ℕ
h✝ : ¬m = 0
⊢ n % m < m
```

We specified the correct decreasing measure, so our options are to use `have`

-expressions or to use `decreasing_by`

.
Here, we use `decreasing_by tactics`

to prove the termination of this function.
At the first, let's placeholder by `sorry`

to show the goal.

```
def gcd (m n : Nat) : Nat :=
if m = 0 then
n
else
gcd (n % m) m
termination_by m
decreasing_by sorry
```

```
m n : ℕ
h✝ : ¬m = 0
⊢ (invImage (fun x ↦ PSigma.casesOn x fun m n ↦ m) instWellFoundedRelationOfSizeOf).1 ⟨n % m, m⟩ ⟨m, n⟩
```

This goal is compiler-generated so difficult to read, so we simplify the goal with `simp_wf`

.

```
def gcd (m n : Nat) : Nat :=
if m = 0 then
n
else
gcd (n % m) m
termination_by m
decreasing_by simp_wf; sorry
```

```
m n : ℕ
h✝ : ¬m = 0
⊢ n % m < m
```

By the way, where the hypothesis `h✝ : ¬m = 0`

come from? Indeed, during a proof of termination, `if p then t else f`

is rewritten into `if h : p then t else f`

, so
the hypothesis `p`

becomes available.

The remained task is only to prove this goal:

```
def gcd (m n : Nat) : Nat :=
if m = 0 then
n
else
gcd (n % m) m
termination_by m
decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
```

For your information, if we use the option to use `have`

-expressions, the function is the following form:

```
def gcd (m n : Nat) : Nat :=
if h : m = 0 then
n
else
have := mod_lt n (zero_lt_of_ne_zero h)
gcd (n % m) m
```

But the `have`

-expressions may be an obstacle when we use the equation lemma.

Another example is the following function in `Data.Multiset.Basic`

.

```
def strongInductionOn {p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s, (∀ t < s, p t) → p s) :
p s :=
(ih s) fun t _h =>
strongInductionOn t ih
termination_by card s
decreasing_by exact card_lt_card _h
```

This example uses `card s`

as a decreasing measure instead of the argument itself.

## WellFoundedRelation instance #

We can specify not only an `Nat`

value but also any types with `WellFoundedRelation`

as a decreasing measure, as you can see in `Data.List.Defs`

:

```
def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
(H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
| [], is => H0 is
| t :: ts, is =>
H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
termination_by ts is => (length ts + length is, length ts)
decreasing_by all_goals (simp_wf; omega)
```

This example uses an `Nat × Nat`

value as a decreasing measure. The `WellFoundedRelation`

on this type is a lexicographical order on natural numbers,
defined by the following instance in `Init.WF`

:

```
instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β) :=
lex ha hb
```