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