Proving termination w/ (n' < n \/ (n' = n /\ m' < m))

Stream: new members

[cbailey]

Is there any way to convince Lean that a function f (n : nat, m : nat) -> T, where each recursive call satisfies ( n' < n \/ ( n' = n /\ m' < m ) ) is indeed terminating without explicitly adding a third parameter to represent (n + m) or gas?
Thank you!

[Kenny Lau]

1. give us an example 2. custom well-founded tactic

[Jeremy Avigad]

You can do arbitrary well-founded recursion in Lean, though it doesn't always work as smoothly as one would like.

https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#well-founded-recursion-and-induction

In your case, I think the equation compiler (the system that compiles your function specification down to a function expressed in terms of the foundational primitives) will guess that you want to use lexicographic order, and with luck you'll be able to convince it that the recursive call is decreasing (as described in TPIL).

Generally speaking, though, life will be easier if you can find a structural recursion that will do the job.

[Kevin Buzzard]

https://github.com/leanprover/mathlib/blob/master/docs/extras/well_founded_recursion.md

[cbailey]

Thank you for the links @Jeremy Avigad and @Kevin Buzzard , this looks like exactly what I need.

@Kenny Lau I'm just using Euclid's algorithm. I'll try and put together a tactic with the reading material you guys referenced

Thanks!

[Wojciech Nawrocki]

I found that definining the entire recursive function as an equation-compiler-expression and then ignoring some of the match variables in cases where they don't matter works best, e.g.:

def rec_fn: ℕ → ℕ → (ℕ → ℕ) → ℕ → ℕ
| _ b f 0 := f b
| a b f (n+1) := rec_fn a (b+a) f n

but then I end up having to type things like (real example):

def applyTypeSub: ∀ {Γ Γ' T}, SubFn Γ Γ' → Term Γ T → Term Γ' T
| _ _ _ s (Var v) := s _ v
| _ _ _ _ (Nat n) := Nat n
| _ _ _ _ (Bool b) := Bool b
| _ _ _ s (Abs e) := Abs (applyTypeSub (STmL s) e)
| _ _ _ s (App fn arg) := App (applyTypeSub s fn) (applyTypeSub s arg)

in order to make all the variables unify correctly.