Showing termination with high-order inductive

Stream: new members

[Jakub Nowak]

Is it possible to show that this terminates in Lean?

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

mutual

  def ListSchema.eval_flatten : List (ListSchema α) → List α
  | [] => []
  | xs :: xss => List.append xs.eval (eval_flatten xss)

  def ListSchema.eval : ListSchema α → List α
  | nil => []
  | cons x xs => x :: xs.eval
  | fmap xs f => eval_flatten (xs.eval.map f)

end


-- example

def range : Nat → ListSchema Nat
| 0 => .nil
| n + 1 => .cons n (range n)

def ex : ListSchema Nat := .fmap (.cons 3 (.cons 4 .nil)) range

#eval! ex.eval

[Jakub Nowak]

I think, this requires defining size measure such that for x ∈ xs.eval we have sizeOf (f x) < sizeOf (fmap xs f).

[Jakub Nowak]

This kinda works, but requires explicitly stating upper bound for fmap:

inductive ListSchema' : Type → Nat → Type 1 where
| nil : ListSchema' α 0
| cons (x : α) (xs : ListSchema' α n) : ListSchema' α n
| fmap (xs : ListSchema' α n) (f : α → ListSchema' β m) : ListSchema' β (n + m + 1)

mutual

  def ListSchema'.eval_flatten : List (ListSchema' α n) → List α
  | [] => []
  | xs :: xss => List.append xs.eval (eval_flatten xss)

  def ListSchema'.eval : ListSchema' α n → List α
  | nil => []
  | cons x xs => x :: xs.eval
  | fmap xs f => eval_flatten (xs.eval.map f)

end


structure ListSchema (α : Type) : Type 1 where
  n : Nat
  val : ListSchema' α n

def ListSchema.nil : ListSchema α where
  n := 0
  val := .nil

def ListSchema.cons (x : α) (xs : ListSchema α) : ListSchema α where
  n := xs.n
  val := .cons x xs.val

-- doesn't work
-- is it possible to define this?
def ListSchema.fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β where
  n := xs.n + _ + 1
  val := .fmap xs.val (fun x => ListSchema.val (f x))


-- example

def range : Nat → ListSchema' Nat 0
| 0 => .nil
| n + 1 => .cons n (range n)

def ex : ListSchema' Nat 1 := .fmap (.cons 3 (.cons 4 .nil)) range

#eval ex.eval

[Jakub Nowak]

So I think I need to somehow tell Lean, that f will be called finitely many times, each call can return ListSchema with some value of n. And it's fine, because maximum of finitely many finite numbers is finite.
(That argument also requires some kind of ListSchema' α n → ListSchema' α (n + m) lifting)

[Aaron Liu]

I think this doesn't let you do certain infinitely wide trees that were possible before

[Jakub Nowak]

Aaron Liu said:

I think this doesn't let you do certain infinitely wide trees that were possible before

I was thinking the same, but now I'm not so sure. Certainly what I defined above is limited, but with additional lifting, like below, I think it's fine? Can you show an example?

inductive ListSchema' : Type → Nat → Type 1 where
| nil : ListSchema' α 0
| cons (x : α) (xs : ListSchema' α n) : ListSchema' α n
| fmap (xs : ListSchema' α n) (f : α → ListSchema' β m) : ListSchema' β (max n m + c + 1)

[Jakub Nowak]

I don't think you can create infinite tree with this?

[Aaron Liu]

yeah ListSchema can do certain infinite trees that ListSchema' can't do

[Mirek Olšák]

Is this what you want?

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

def ListSchema.eval (l : ListSchema α) : List α := match l with
| nil => []
| cons x xs => x :: xs.eval
| fmap xs f => List.flatten (xs.eval.map (fun x ↦ eval (f x)))

-- example

def range : Nat → ListSchema Nat
| 0 => .nil
| n + 1 => .cons n (range n)

def ex : ListSchema Nat := .fmap (.cons 3 (.cons 4 .nil)) range

#eval! ex.eval

[Mirek Olšák]

To be honest, I am not sure how termination proving works with mutual recursion. Also, infinite-branching trees are tricky for well-founded recursion because the default sizeOf mechanism can only handle natural numbers, and well founded recursion on infinite-branching trees require ordinals. Fortunatelly, Lean managed to figure out a way how to capture the definition above as a structural recursion.

[Mirek Olšák]

It doesn't mean it is impossible, only that there seems to be some missing infrastructure to prove it conveniently.

[Jakub Nowak]

Mirek Olšák said:

Is this what you want?

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

def ListSchema.eval (l : ListSchema α) : List α := match l with
| nil => []
| cons x xs => x :: xs.eval
| fmap xs f => List.flatten (xs.eval.map (fun x ↦ eval (f x)))

-- example

def range : Nat → ListSchema Nat
| 0 => .nil
| n + 1 => .cons n (range n)

def ex : ListSchema Nat := .fmap (.cons 3 (.cons 4 .nil)) range

#eval! ex.eval

Indeed, thanks! I wonder, why this works, and my implementation doesn't, they look pretty much the same. Is it possible to somehow print what terminating_by measure did Lean use, or have Lean somehow explain its reasoning in some other way? I'm particulary interested how Lean proved that eval (f x) call is decreasing.

[Aaron Liu]

it's structural recursion

[Jakub Nowak]

Is it? There's eval (f x), for an arbitrary x, is that structural recursion too?

[Aaron Liu]

since f comes from the argument it has to give a structurally smaller value for any x

[Jakub Nowak]

If I add

termination_by sizeOf l

then Lean fails to prove that eval (f x) call is decreasing. How can I perform the proof manually?

[Aaron Liu]

Jakub Nowak said:

Is it possible to somehow print what terminating_by measure did Lean use, or have Lean somehow explain its reasoning in some other way?

I have two ways

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

/--
info: Try this:
  [apply] termination_by structural l
-/
#guard_msgs in
def ListSchema.eval (l : ListSchema α) : List α := match l with
| nil => []
| cons x xs => x :: xs.eval
| fmap xs f => List.flatten (xs.eval.map (fun x ↦ eval (f x)))
termination_by?

or you can print it directly

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

def ListSchema.eval (l : ListSchema α) : List α := match l with
| nil => []
| cons x xs => x :: xs.eval
| fmap xs f => List.flatten (xs.eval.map (fun x ↦ eval (f x)))

/--
info: def ListSchema.eval : {α : Type} → ListSchema α → List α :=
fun {α} l =>
  ListSchema.brecOn l fun {α} l f =>
    (match (motive := (l : ListSchema α) → ListSchema.below l → List α) l with
      | ListSchema.nil => fun x => []
      | ListSchema.cons x xs => fun x_1 => x :: x_1.1
      | xs.fmap f => fun x => (List.map (fun x_1 => (x.2 x_1).1) x.1.1).flatten)
      f
-/
#guard_msgs in
#print ListSchema.eval

[Mirek Olšák]

sizeOf is a wrong measure

[Aaron Liu]

you can't show it's decreasing with sizeOf

[Aaron Liu]

there's not enough natural numbers to fit all the kinds of infinite trees that can be constructed

[Jakub Nowak]

I see, the error message that shows with termination_by l says to try sizeOf. I didn't know about structural, maybe the error message should mention it?

[Jakub Nowak]

Isn't structural always better choice than sizeOf?

[Aaron Liu]

sometimes you have to jump through hoops to make it structural

[Aaron Liu]

but generally I think it's usually always better when it works

[Mirek Olšák]

No, well founded recursion is in general much stronger

Jakub Nowak said:

Isn't structural always better choice than sizeOf?

[Jakub Nowak]

Hm, I guess when you decrease one argument of constructor but increase another than structural fails, but sizeOf could work.

[Mirek Olšák]

import Mathlib

inductive ListSchema : Type → Type 1 where
| nil : ListSchema α
| cons (x : α) (xs : ListSchema α) : ListSchema α
| fmap (xs : ListSchema α) (f : α → ListSchema β) : ListSchema β

noncomputable
def ListSchema.ordinalLevel {α : Type} (l : ListSchema α) : Ordinal.{0} := match l with
| nil => 0
| cons _ xs => xs.ordinalLevel + 1
| fmap xs f => max (xs.ordinalLevel + 1) (⨆ a, ordinalLevel (f a) + 1)

theorem ListSchema.cons.ordinalLevel_gt (a : α) (l : ListSchema α) :
    l.ordinalLevel < (ListSchema.cons a l).ordinalLevel := by
  conv => rhs; unfold ordinalLevel
  simp

example (a b : Ordinal.{0}) (h : a < b) : a+1 ≤ b := by exact Order.add_one_le_iff.mpr h

theorem ListSchema.fmap.ordinalLevel_gt1 (xs : ListSchema α) (f : α → ListSchema β) :
    xs.ordinalLevel < (ListSchema.fmap xs f).ordinalLevel := by
  conv => rhs; unfold ordinalLevel
  simp

theorem ListSchema.fmap.ordinalLevel_gt2 (xs : ListSchema α) (f : α → ListSchema β) (a : α) :
    (f a).ordinalLevel < (ListSchema.fmap xs f).ordinalLevel := by
  conv => rhs; unfold ordinalLevel
  apply Order.add_one_le_iff.mp
  apply le_sup_of_le_right
  exact Ordinal.le_iSup ..

def ListSchema.eval (l : ListSchema α) : List α := match l with
| nil => []
| cons x xs => x :: xs.eval
| fmap xs f => List.flatten (xs.eval.map (fun x ↦ eval (f x)))
termination_by l.ordinalLevel
decreasing_by
· apply ListSchema.cons.ordinalLevel_gt
· apply ListSchema.fmap.ordinalLevel_gt2
· apply ListSchema.fmap.ordinalLevel_gt1

[Mirek Olšák]

Afaik, Lean doesn't generate ordinalLevel automatically like sizeOf. I am not sure if there is any infrastructure for it, so I did it manually.

[Jakub Nowak]

Thanks! That looks very useful.

[Aaron Liu]

you also have to import ordinals

[Aaron Liu]

unlike Nat they don't come with Lean

[Mirek Olšák]

The minimal import is

import Mathlib.SetTheory.Ordinal.Family

of course importing whole Mathlib works too.

[Mirek Olšák]

The idea is that I defined ListSchema.ordinalLevel using structural recursion, and since ordinals have a canonical WellFoundedRelation, it is later possible to use it for well-founded recursion.

[Mirek Olšák]

Under the hood, sizeOf does the same idea, only that the measure is done by natural numbers, so it is not able to measure infinite trees.