Proving termination (yet again...)

Stream: lean4

[Alexander Fasching]

I'm trying to formalize Epistemic Action Logic, and constantly run into some issues with termination.
Without posting the mess I've experimented with, I think I can resolve most of it if I know how to show termination for the examples below.

Here, height terminates:

/- Prove termination automatically. -/
namespace Inferred

inductive Tree (α : Type u) where
  | nil
  | node (pre : α → Tree α) (val : α)

def height : Tree α → Nat
  | .nil => 0
  | .node pre val => 1 + height (pre val)

end Inferred

But not in the next two examples, although they are basically the same:

/- Definition with mutual inductives. -/
namespace Mutual

mutual
  inductive Node (α : Type u) where
    | mk (pre : α → Tree α) (val : α)

  inductive Tree (α : Type u) where
    | nil
    | node (n : Node α)
end

def Node.pre : Node α → (α → Tree α) | .mk pre _ => pre
def Node.val : Node α → α            | .mk _ val => val

def height : Tree α → Nat
  | .nil => 0
  | .node n => 1 + height (n.pre n.val)

end Mutual

/- Definition with parametrized structures. -/
namespace Structure

structure Node (α : Type u) (β : Type v) where
  pre : α → β
  val : α

inductive Tree (α : Type u) where
  | nil
  | node (n : Node α (Tree α))

def height : Tree α → Nat
  | .nil => 0
  | .node n => 1 + height (n.pre n.val)

end Structure

How can I prove termination for the latter two examples?

[Joachim Breitner]

Lean does not support structural recursion, like in the first example, with mutually recursive data types (yet).

So the other way of proving termination is with well-founded recursion, e.g. using termination_by t => height t. Of course this doesn't help when you are trying to define height itself…
It seems that there is a sizeOf function defined automatically for your Tree/Node pair, but it seems to ignore function types (not unexpected, hardly possible to assign them a size measured in Nat):

def Mutual.Node._sizeOf_2.{u} : {α : Type u} → [inst : SizeOf α] → Tree α → Nat :=
fun {α} [SizeOf α] t => Tree.rec (fun pre val pre_ih => 1 + sizeOf val) 1 (fun n n_ih => 1 + n_ih) t

If you only want to prove stuff about it, but not compile or #eval, you can useTree.rec manually:

noncomputable
def height : Tree α → Nat := Tree.rec
  (mk := fun pre val ih => 1 + ih val)
  (nil := 0)
  (node := fun n ih => 1 + ih)

#reduce height (Tree.node (Node.mk (fun () => .nil) ()))

[Joachim Breitner]

With that non-computable height you can actually define a computable version:

noncomputable
def height' : Tree α → Nat := Tree.rec
  (mk := fun pre val ih => ih val)
  (nil := 0)
  (node := fun n ih => 1 + ih)

def height : Tree α → Nat
  | .nil => 0
  | .node n => 1 + height (n.pre n.val)
termination_by t => height' t
decreasing_by
  simp_wf
  cases n
  simp [Node.pre, Node.val, height']
  omega

[Joachim Breitner]

The example with a parametrized structure is not much different from the mutual one, because Lean has do implement nested inductive types using mutual types.

[Alexander Fasching]

Thanks!
I think I can work with this.

[Mario Carneiro]

Joachim Breitner said:

If you only want to prove stuff about it, but not compile or #eval, you can useTree.rec manually:

You can get the best of all worlds (except the one where you don't have to do this dance) by defining a partial computable version and use @[implemented_by] to the one defined using Tree.rec

[Joachim Breitner]

Except that implemented_by is untrusted, so if you care about that, you can define one with Tree.rec, then one using termination_by, then prove them equivalent, and then slap the csimp attribute on that proof. Then you have the best of all worlds, besides having had to far too much for a very simple function :-)