Zulip Chat Archive

Stream: new members

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


view this post on Zulip cbailey (Jan 10 2019 at 08:33):

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!

view this post on Zulip Kenny Lau (Jan 10 2019 at 08:44):

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

view this post on Zulip Jeremy Avigad (Jan 10 2019 at 08:50):

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.

view this post on Zulip Kevin Buzzard (Jan 10 2019 at 09:32):

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

view this post on Zulip cbailey (Jan 10 2019 at 09:39):

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!

view this post on Zulip Wojciech Nawrocki (Jan 13 2019 at 20:24):

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.


Last updated: May 14 2021 at 13:24 UTC