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

Last updated: Dec 20 2023 at 11:08 UTC