# Zulip Chat Archive

## Stream: new members

### Topic: termination_by

#### Hungry Applicative (Nov 24 2021 at 22:18):

Hi! I'm completely new to Lean, currently exploring Lean 4.

I'm trying to define factorial like this:

```
def fac(n : Nat): Nat :=
if n == 0
then 1
else n * fac (n - 1)
```

However I get the following error:

```
fail to show termination for
fac
with errors
argument #1 was not used for structural recursion
failed to eliminate recursive application
fac (n - 1)
structural recursion cannot be used
'termination_by' modifier missing
```

So I understand that I can change my definition to use structural recursion, but I would like to prove termination using `termination_by`

. I've tried adding `termination_by Nat.lt_wfRel`

at the end, but I don't understand how to discharge the resulting goals:

```
unsolved goals
x : Nat
⊢ x - 1 < x
```

Does anyone have any pointers?

#### Kevin Buzzard (Nov 24 2021 at 22:22):

Note that the goal as presented is not provable because x can be 0. Try `if h : x = 0 then...`

? That might add the relevant hypothesis to the context

#### Kevin Buzzard (Nov 24 2021 at 22:24):

And I trust you understand that you're making things much more difficult for yourself because you can just do a case spilt with the equation compiler and this problem wouldn't arise (i guess that is structural recursion)

#### Hungry Applicative (Nov 24 2021 at 22:37):

Thank you! I will give it a go tomorrow.

#### Hungry Applicative (Nov 26 2021 at 15:08):

I got stuck on this problem. Is the decreasing_by construct mature yet? I haven't been able to find any documentation and it doesn't seem to be behave as nicely as a normal "tactic block". Here is what I have so far.

```
def fac(n : Nat): Nat :=
if h: n = 0
then 1
else n * fac (n - 1)
termination_by Nat.lt_wfRel
decreasing_by
skip
```

Last updated: Dec 20 2023 at 11:08 UTC