Zulip Chat Archive

Stream: new members

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


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!

Kenny Lau (Jan 10 2019 at 08:44):

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

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.

Kevin Buzzard (Jan 10 2019 at 09:32):

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

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!

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: Dec 20 2023 at 11:08 UTC