showing termination with pattern matching

Stream: new members

[Mark Aagaard]

I'm exploring methods of showing termination in recursive functions. Lean is able to determine that quot4 below terminates because d > 0 is in the if-then-else condition.

def quot4 : (n d : Nat) → Nat
  | 0, d => 0
  | n, d => if  n ≥ d  ∧  d > 0 then 1 + quot4 (n-d) d else 0

If I incorporate the d > 0 condition into the pattern matching, Lean needs help to show termination:

abbrev quot3 : (n d : Nat) → Nat
  | 0, 0 => 0
  | n, 0 => 0
  | n, d =>
  have : d > 0 := sorry
  if  n ≥ d  then 1 + quot3 (n-d) d else 0

Is there a preferred tactic to replace the sorry in quot3 or is quot4 the best method for handling this form of recursion?

-mark

[Eric Wieser]

This works:

abbrev quot3 : (n d : Nat) → Nat
  | 0, 0 => 0
  | n, 0 => 0
  | n, d@ h : (_ + 1) =>
    if  n ≥ d  then 1 + quot3 (n-d) d else 0

[Mark Aagaard]

Eric, thanks. Do you know where this @ notation is documented? I'm familiar with "@" as a prefix for a name to get at implicit arguments, but this seems different.

-mark

[Kyle Miller]

It's got to be documented somewhere, but the gist is that x@patt is a way to bind the value of the matched value to x.

[Kyle Miller]

This suffices:

def quot3 : (n d : Nat) → Nat
  | 0, 0 => 0
  | n, 0 => 0
  | n, d@(_+1) =>
    if n ≥ d then 1 + quot3 (n-d) d else 0

The key is that in a match, each match arm does not know that the previous cases do not apply, so you need the pattern _ + 1 to know for sure d is not zero.

(By the way, you probably don't want a recursive abbrev.)

[Mark Aagaard]

Kyle, thanks; that makes sense. Thanks also for the heads up about abbrev. I had remembered that there were some differences between abbrev and def, and was tinkering, then forgot to clean up my code before posting.

-mark