show termination in an if statement

Stream: lean4

[yannis monbru]

Hi, i am dealing with a function like 'exemple' in the mwe where i do stuff and recurcively apply a function 'step' if the argument has decreased

To show the terminaison, i found that it was accepted by provinding in the else part the evidence that the argument has decreased.

I would like to know if there is a better way to show the terminaison, or if it the correct way to think about it.

Thank you very much

def step (n:Nat): Bool × Nat:= match n with
  |0 => (true,0)
  |n + 1 => (false, n)

def exemple (n:Nat): Nat :=
  let res:= step n
  if res.1 then
    n
  else
    have : res.2 < n:= by
      sorry
    exemple res.2

[Damiano Testa]

Does using

  if h : res.1 then

work? Note that I added a "name" to the hypothesis.
Maybe I misunderstood the question.

[yannis monbru]

My non-minimal exemple of this is accepted by lean, and my question is about if it’s the way i should do it or if it’s working but not optimal

[Edward van de Meent]

you can probably avoid the entire thing by simply matching on n in the function body of example rather than defining the auxilary function step...

[yannis monbru]

I am struggling to do that, because in this example you can recover the value of the bolean from the 'Nat' you get as an output but in my code i couldn't and then i needed to return a bolean to know if i had to stop in the function 'exemple'

[Edward van de Meent]

yannis monbru said:

in this example you can recover the value of the bolean from the 'Nat' you get as an output but in my code i couldn't

could you then maybe give a clearer idea of what logic your version of the step function entails? because it's hard to judge if lean can tell if a function terminates, when the example doesn't use the same logical decision structure...

[yannis monbru]

My version of step is manipulating two list and the bolean is there to tell if 'step' changed the size of one of the list
what matters to me is the fact of having the bolean to know if you can apply step or if you will enter an infinite loop

In my version lean is happy (and there is no sorry)

[Patrick Massot]

@Joachim Breitner do you have any comment here?

[Joachim Breitner]

Sorry, I am not sure what the question is.

In my version lean is happy (and there is no sorry)

So is this resolved?

[Patrick Massot]

I think part of the question is how to write something like:

def step (n:Nat): Bool × Nat:= match n with
  |0 => (true,0)
  |n + 1 => (false, n)

def exemple (n:Nat): Nat :=
  let res:= step n
  if res.1 then
    n
  else
    exemple res.2
termination_by sorry

[Patrick Massot]

But termination_by is not happy here.

[Patrick Massot]

My understanding after our lunch was that termination_by would happily give two goals, one for each branch of the if.

[Joachim Breitner]

Like this?

def step (n:Nat): Bool × Nat:= match n with
  |0 => (true,0)
  |n + 1 => (false, n)

def exemple (n:Nat) : Nat :=
  let res:= step n
  if res.1 then
    n
  else
    exemple res.2
termination_by n
decreasing_by cases n <;> simp_all [step, res]

[Joachim Breitner]

Are you confusing termination_by and decreasing_by? (Not unreasonable to confuse the two)

Also, it’s one branch for each recursive call, not necessarily for each branch.

[Patrick Massot]

Thanks, that helps a lot.