Help with termination_by

Stream: lean4

[Marcus Rossel]

I have the following type of Terms:

inductive Term
  | bool (b : Bool)
  | nat (n : Nat)
  | ite (cond pos neg : Term)

I want to define and evaluation function on Terms in two steps.
First, I define a single evaluation step (which fails if we try to evaluate an ite with a number as condition):

def eval₁ (t : Term) : Option Term :=
  match t with
  | bool _ => t
  | nat _ => t
  | ite cond pos neg =>
    match cond with
    | .bool .true => pos
    | .bool .false => neg
    | _ =>
      match eval₁ cond with
      | some cond' => ite cond' pos neg
      | none => none

Second, I define a full evaluation by recursion on the single-step evaluation function:

def eval (t : Term) : Option Value :=
  match h : t.eval₁ with
  | none => none
  | some (.bool b) => some (.bool b)
  | some (.nat n) => some (.nat n)
  | some t'@(.ite ..) => t'.eval

For the eval function, Lean can't prove termination by itself.
I know that termination_by exists, but how could I use that (and possible decreasing_by) to show termination here?
Does it somehow involve SizeOf?

[Henrik Böving]

You would use termination_by eval t => t in order to indicate to Lean that you wish to proof termination by showing that t's size decreases every step, it will then tell you that it is missing sizeOf t' < sizeOf t in the ite case which you can give it by doing:

def eval (t : Term) : Option Value :=
  match h : t.eval₁ with
  | none => none
  | some (.bool b) => some (.bool b)
  | some (.nat n) => some (.nat n)
  | some t'@(.ite ..) =>
    have : sizeOf t' < sizeOf t := by sorry
    t'.eval
  termination_by eval t => t

[Henrik Böving]

However you will fail to perform this proof since your function does not terminate, consider:

#eval eval (ite (nat 12) (nat 13) (nat 14))

which will endlessly loop. This will become evident in the proof when you arrive in the case where your input expression was a ite and the condition was a nat, after fully simplifying it presents you with False since you'd have to proof that sizeOf t < sizeOf t in this special case.

[Marcus Rossel]

Henrik Böving said:

However you will fail to perform this proof since your function does not terminate, consider:

#eval eval (ite (nat 12) (nat 13) (nat 14))

which will endlessly loop. This will become evident in the proof when you arrive in the case where your input expression was a ite and the condition was a nat, after fully simplifying it presents you with False since you'd have to proof that sizeOf t < sizeOf t in this special case.

Oh thanks! I was struggling with the proof right now :see_no_evil:

[Henrik Böving]

You could go full C style here and say that a nat condition evals to true if it is not equal to 0 to avoid this^^

[Marcus Rossel]

Henrik Böving said:

You could go full C style here and say that a nat condition evals to true if it is not equal to 0 to avoid this^^

Haha, I've decided to go with this instead:

def eval₁ (t : Term) : Option Term :=
  match t with
  | bool _ => t
  | nat _ => t
  | ite cond pos neg =>
    match cond with
    | .bool .true => pos
    | .bool .false => neg
    | .nat _ => none
    | .ite .. =>
      match eval₁ cond with
      | some cond' => ite cond' pos neg
      | none => none

[Matthew Ballard]

I am confused by the behavior in this example. Any help would be appreciated.

class IsWellFounded (α : Type _) (r : α → α → Prop) where

variable {α : Type _} (r r' : α → α → Prop)

theorem wf [IsWellFounded α r'] : WellFounded r := sorry

def foo (a : α) : α := sorry

variable [IsWellFounded α r']

def bar (a : α) : α :=
  have : r (foo a) a := sorry
  bar (foo a)
termination_by' ⟨r,wf r r'⟩  -- unknown identifier 'r''

#check r' -- α → α → Prop

[Kevin Buzzard]

def bar (a : α) : α :=
  have : IsWellFounded α r' := inferInstance -- random extra line
  have : r (foo a) a := sorry
  bar (foo a)
termination_by' ⟨r,wf r r'⟩ -- now works

My guess is that in contrast to the usual situation people complain about with variables (they're dragged in when they're not supposed to be), by the time Lean is processing termination_by' it has decided that r' is definitely not used in the declaration so has removed it from the context?

[Adam Topaz]

Right, it seems that lean chucks out everything not involved in the body of the definition before the ternimation_by'.

[Matthew Ballard]

Thanks. That makes sense. It is even more annoying when the instance has no explicit parameters.

[Matthew Ballard]

class Blah (α : Type _) where

variable {α : Type _} (r r' : α → α → Prop)

theorem wf [Blah α] : WellFounded r := sorry

def foo (a : α) : α := sorry

variable [Blah α]

def bar (a : α) : α :=
  -- have : Blah α := inferInstance
  have : r (foo a) a := sorry
  bar (foo a)
termination_by' ⟨r,wf r⟩  -- failed to synthesize instance Blah α

[Adam Topaz]

again, the instance is not part of the def

[Adam Topaz]

so it's tossed

[Matthew Ballard]

Yes, right

[Matthew Ballard]

Let me see if this "fixes" my original problem

[Matthew Ballard]

Yes it does

[Matthew Ballard]

One more question: is termination_by' the idiomatic way to use a custom WellFoundedRelation for termination?

[Gabriel Ebner]

I'd say the most idiomatic way is to add a type alias MyAlias for your relation together with a global WellFoundedRelation MyAlias instance. Then you can do termination_by _ => MyAlias.mk ... to do recursion on that well-founded relation.

[Gabriel Ebner]

In many cases, you can also just write the termination measure directly instead of defining a custom relation. You can even use Ordinal after termination_by _ =>!

[François G. Dorais]

Do you mean WellFoundedRelation MyAlias? I don't think WellFounded is a class, at least not in core.

[François G. Dorais]

How does Ordinal work exactly?

[François G. Dorais]

@Gabriel Ebner Sorry, forgot to mention you above. ^

[Gabriel Ebner]

Sorry, I'm always getting confused by the naming.

[François G. Dorais]

@Gabriel Ebner No worries, I also regularly get confused in the same way.

[Gabriel Ebner]

Ordinal is "just" a very big well-order. Every well-founded relation on a type in Type u maps into Ordinal.{u} in an order-preserving way. So you could always replace your favorite well-founded relation r : α → α → Prop by a function f : α → Ordinal.

[Gabriel Ebner]

The point that I'm trying to get across is that termination_by doesn't restrict you to natural numbers, if you can use well-founded recursion then you can express it with termination_by _ => someFunction a. And at least personally, I find termination measures much easier to read than well-founded relations that are constructed using a custom bespoke API.

[François G. Dorais]

@Gabriel Ebner Yes, I see. I tried to do that on a project of mine yesterday but I could only make termination_by' work (with a lot of additional work explaining what that wellfounded relation was and why). It looks like I was missing some WellFoundedRelation instances to make termination_by work? I think I'm just a bit confused how I should be using this termination API.

[Gabriel Ebner]

The most common way is to just write termination_by _ => value that gets smaller in recursive calls. For a lot of stuff this value can simply be a natural number. You can also put a pair there, then you get the lexicographic order.

[François G. Dorais]

But how is the relation inferred? In my use case, the default "SizeOf" is irrelevant.

[Gabriel Ebner]

We didn't have termination_by in Lean 3, so you won't find many examples in mathlib. But from what I can tell, most uses of termination_by' would be much better served by termination_by. Compare:

termination_by' invImage PSigma.fst ⟨_, degree_lt_wf⟩
-- vs.
termination_by _ => R.degree

or

termination_by' PSigma.lex (inferInstance) (fun _ ↦ inferInstance)
-- vs.
termination_by _ => (a, b, c)

[Gabriel Ebner]

François G. Dorais said:

But how is the relation inferred? In my use case, the default "SizeOf" is irrelevant.

The relation is inferred using the WellFoundedRelation (type of the termination_by value) type class. For many types (natural numbers, pairs, ordinals) this has a sensible value. SizeOf is only used as a low-priority fallback instance.

[François G. Dorais]

Here is a MWE:

structure Forest (α : Type) [DecidableEq α] where
  pred : α → Option α
  wf : WellFounded fun x y => pred y = some x

namespace Forest
variable {α} [DecidableEq α] (forest : Forest α)

instance relWF : WellFoundedRelation α where
  rel x y := forest.pred y = some x
  wf := forest.wf

def rank (x : α) : Nat :=
  match _hint : forest.pred x with
  | some y => rank y + 1
  | none => 0
termination_by' forest.relWF

How can I use termination_by here?

[Gabriel Ebner]

You can use a type alias:

structure Forest (α : Type) where
  pred : α → Option α
  wf : WellFounded fun x y => pred y = some x

def Forest.Node (_forest : Forest α) :=
  α

instance {forest : Forest α} : WellFoundedRelation forest.Node where
  rel x y := forest.pred y = some x
  wf := forest.wf

def Forest.rank (forest : Forest α) (x : α) : Nat :=
  match _hint : forest.pred x with
  | some y => forest.rank y + 1
  | none => 0
termination_by _ => (id x : forest.Node)

[Gabriel Ebner]

You might also want to look at the WellFounded.rank function.

[François G. Dorais]

Thanks for the wonderful hints!

[François G. Dorais]

I also realized that I have been overusing abbrev!
This is all very enlightening!

[Simon Hudon]

I found this thread very useful, thank you @Gabriel Ebner and @François G. Dorais!

I thought I'd add a note in case it's useful for others: it also works with mutually recursive functions on mutually inductive types. In that case the abbrev should be a _ ⊕ _ type and I have found it useful to define new cases for the decreasing_trivial tactic so that I don't have to write a decreasing_by clause for each mutually recursive function

My new cases look like

local macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply StructM.branch_tl)

StructM is an inductive relation on the _ ⊕ _ type and branch_tl is one of the constructors.