termination_by

Stream: new members

[Hungry Applicative]

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]

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]

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]

Thank you! I will give it a go tomorrow.

[Hungry Applicative]

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