Proving termination with List.Shortlex

Stream: general

[Mirek Olšák]

What is the right way to use List.Shortlex to prove termination? Let's consider this demo function (I don't care this is just fold in a way, I want to know the proper way to use Shortlex)

def f2 (l : List ℕ) : ℕ := match l with
  | [] => 0
  | [x] => x
  | 0::tail => f2 tail
  | (k+1)::n::tail => f2 (k::(2 ^ (n+k))::tail)

Then I was able to do it this way

local instance : WellFoundedRelation (List ℕ) where
  rel a b := List.Shortlex (· < ·) a b
  wf := List.Shortlex.wf (inferInstance : WellFoundedRelation ℕ).wf

def f2 (l : List ℕ) : ℕ := match l with
  | [] => 0
  | [x] => x
  | 0::tail => f2 tail
  | (k+1)::n::tail => f2 (k::(2 ^ (n+k))::tail)
  termination_by l
  decreasing_by
  · decreasing_tactic
  · simp [List.shortlex_def]
    apply List.Lex.rel
    simp

But it feels a bit clumsy.

• Is there a faster way to get WellFoundedRelation (List ℕ)? I would expect a simple conversion, once there is List.Shortlex.wf
• Do I have to declare it as an instance? Ideally, I would like to just tell termination_by to use this relation.

[Malvin Gattinger]

I had a similar case where docs#WellFounded.wrap could be used to avoid declaring an instance, maybe that works here too?

[Malvin Gattinger]

Yes!

import Mathlib

def f2 (l : List ℕ) : ℕ := match l with
  | [] => 0
  | [x] => x
  | 0::tail => f2 tail
  | (k+1)::n::tail => f2 (k::(2 ^ (n+k))::tail)
  termination_by
    WellFounded.wrap (List.Shortlex.wf (Nat.lt_wfRel).2) l
  decreasing_by
  · decreasing_tactic
  · simp [List.shortlex_def]
    apply List.Lex.rel
    simp

[Mirek Olšák]

Thanks! On my computer, I had to explicitly unwrap simp [WellFounded.wrap], but that might be just an old Lean version...

[Malvin Gattinger]

Ah, I made the above on live.lean-lang.org

[Mirek Olšák]

Looks much better, also the List.Shortlex.wf Nat.lt_wfRel.2. I was somehow not able to click through to get the core well foundedness on naturals.

[Malvin Gattinger]

Yes, I also would have guessed there should be a Nat.lt_wf (without Rel) :thinking:

[Aaron Liu]

Mirek Olšák said:

Thanks! On my computer, I had to explicitly unwrap simp [WellFounded.wrap], but that might be just an old Lean version...

That was batteries#1308

[Mirek Olšák]

Malvin Gattinger said:

Yes, I also would have guessed there should be a Nat.lt_wf (without Rel) :thinking:

Although if it was not Nat, getting from an existing WellFoundedRelation typeclass instance to a WellFounded assumption still feels a little more complicated than it should be...

[Malvin Gattinger]

I agree this feels overkill. It bothered me before that termination_by allows us to specify the value (and thus its type) that should be decreasing, but the choice which relation on that type is used has to be done via class inference or with wrap. Some months ago when discussing with @Andrés Goens and @Haitian Wang I was dreaming of a way to prove termination without going via a WellFoundedRelation, something like this (NOT working Lean code):

def α : Type := sorry

def g : α → α := sorry

def f : (x : α) → α
  | x => f (g x)
termination_by
  x -- fixes value and type, but not yet the relation
with_relation
  fun x y => sorry -- define custom relation here
is_wf_by
  -- GOAL: WellFounded (fun x y => sorry)
  sorry
decreasing_by
  -- GOAL: (fun x y => sorry) (g x) x
  sorry

In particular this would be useful if this termination proof is the only place where that relation and its wellfoundedness are needed. (e.g.)

[Joachim Breitner]

That’s plausible, although I’m not sure if this is a common enough use case to justify expanding the syntax surface, when wrap is a decent escape hatch for advanced users.

[Mirek Olšák]

To me, it would also feel a bit more principled, perhaps something like

with_relation
  rel a b := ...
  is_wf := ... -- optional, with some default inference

[Mirek Olšák]

But sure, I am fine with the wrap hack for now...

[Joachim Breitner]

The whole post-function-syntax (with termination_by, decreasing_by, partial_fixpoint etc) is suffering from organic growth already…

[Mirek Olšák]

Sure, no problem. Maybe there is a more principled termination syntax in general...

[Malvin Gattinger]

Agreed! I am not suggesting/demanding that this should be done, I just wanted to mention that I thought of it before. This was right before I discovered wrap which is a good enough tool.

[Mirek Olšák]

I could imagine something like.

def f : (x : α) → α
  | x => f (g x)
termination_by
  key := x
  rel := LT.lt
  is_wf := inferWF
  proof := by decreasing_tactic

almost copying a syntax of a structure with default fields, only the key would be a bit of a hack, and keeping a shortcut when only key is presented. On the other hand, I agree refactoring this is low priority.