Proving termination in nested inductives

Stream: lean4

[Daniel Fabian]

I'm working on taking inspiration from some Coq code and implementing something similar in Lean. And I hit some trouble proving termination for something that coq seems to have no trouble at all.

The context is, that I've got an n-ary tree to work with. Here's a MWE:

Inductive nelist (A : Type) : Type :=
| nil : A -> nelist A
| cons : A -> nelist A -> nelist A.

Section f.
Variable A: Type.
Variable B: Type.
Variable f: A -> B.
Variable g: B -> B -> B.
Fixpoint foldMap (l : nelist A) : B :=
  match l with
    | nil _ x => f x
    | cons _ x xs => g (f x) (foldMap xs)
  end.
End f.


Inductive tree : Type :=
  | node : nelist tree -> tree
  | leaf : tree.

Fixpoint count (t : tree) : nat :=
  match t with
    | node xs => foldMap _ _ count (fun x y => x + y) xs
    | leaf => 1
  end.

inductive nelist (α : Type u) : Type u
| nil : α → nelist α
| cons : α → nelist α → nelist α

def foldMap (f : α → β) (g : β → β → β) : nelist α → β
| nelist.nil a => f a
| nelist.cons x xs => g (f x) (foldMap f g xs)

inductive tree
| node : nelist tree → tree
| leaf : tree

def count : tree → Nat
| tree.node xs => foldMap count Nat.add xs
| tree.leaf => 1

and when I try using well-founded recursion I just get an unexpected occurrence of recursive application.

Any idea how to prove these nicely?

[Sebastian Ullrich]

The generic solution is to equip foldMap's fold function with a proof that the passed element is part of the given list, from which you can derive that its sizeOf size is smaller. The simpler solution is to specialize foldMap to count, yielding mutually recursive definitions. I pushed an example of the latter a few days ago https://github.com/leanprover/lean4/blob/master/tests/lean/run/mut_ind_wf.lean

[Leonardo de Moura]

And I hit some trouble proving termination for something that coq seems to have no trouble at all.

Recall that Lean does not have a termination checker in the kernel.
In Lean, we have to justifiy the termination using structural or well founded recursion.
This kind of example is quite verbose right now because of missing features:

• lineararith is missing
• Heuristics for guessing good well founded relations is missing
• Better support for combinators such as map and fold is missing.

[Daniel Fabian]

yeah I see that:

tactic 'assumption' failed,
xs : nelist tree
⊢ sizeOf xs < 1 + sizeOf xs

[Daniel Fabian]

in fact all of the proofs would go away with a bit of linear arithmetic.

[Leonardo de Moura]

We are working on that as we described in our last dev meeting that included you :stuck_out_tongue_wink:

[Daniel Fabian]

I know, I know. ;-) I'm working on the other feature and am kinda forced to prove termination. FWIW, the termination_by experience doesn't even compare to Lean 3 in how convenient and much less confusing it is.

[Daniel Fabian]

working on this I found something I don't understand. It looks like a bug to me, but maybe I'm misusing it somehow.

The general idea is to define a definitional reduction to reify objects. And rfl need help in a way that makes absolutely no sense to me. calling #reduce behaves as I'd hope, but rfl needs what looks to me like an unnecessary simp step just to unfold the definition. I even tried marking the def as @[reducible], but I don't think it should be needed to begin with.

Here's the most hatchety job I could do, deleting most of the code:

def arrow (α : Type u) : Nat → Type u
| 0 => α
| n+1 => α → arrow α n

structure Symbol (α : Type u) where
  arity : Nat
  value : arrow α arity

inductive NonEmptyList (α : Type u)
| nil (a : α)
| cons (a : α) (as : NonEmptyList α)

syntax "![" term ", " sepBy(term, ", ") "]" : term
syntax "![" term "]" : term

def NonEmptyList.ofList : α → List α → NonEmptyList α
| a, [] => NonEmptyList.nil a
| a, b::bs => NonEmptyList.cons a (ofList b bs)

macro_rules
  | `(![ $elem, $elems,* ]) => `(NonEmptyList.ofList $elem [ $elems,* ])
  | `(![ $elem ]) => `(NonEmptyList.nil $elem)

infixr:67 " !:: " => NonEmptyList.cons

def NonEmptyList.get! : NonEmptyList α → Nat → α
| ![a], _ => a
| _ !:: as, n+1 => as.get! n
| a !:: _, 0 => a

structure Context (α : Type u) where
  symbols : NonEmptyList $ Symbol α
  arbitrary : α

inductive Expr
| Sym (idx : Nat) (args : List Expr)

def eval {α : Type u} (ctx : Context α) : Expr → α
| Expr.Sym idx args =>
  let sym := ctx.symbols.get! idx
  have : sizeOf args < 1 + idx + sizeOf args := by
    rw [Nat.add_assoc, Nat.add_comm 1]
    apply Nat.lt_succ_of_le
    apply Nat.le_add_left
  reduceSym sym args
where
  reduceSym : Symbol α → List Expr → α
  | ⟨0, f⟩, [] => f
  | ⟨n+1, f⟩, a::as =>
    have : sizeOf a < 1 + sizeOf a + sizeOf as := by
      rw [Nat.add_assoc, Nat.add_comm 1]
      apply Nat.lt_succ_of_le
      apply Nat.le_add_right
    have : sizeOf as < 1 + sizeOf a + sizeOf as := by
      rw [Nat.add_assoc, Nat.add_comm 1]
      apply Nat.lt_succ_of_le
      apply Nat.le_add_left
    reduceSym ⟨n, f (eval ctx a)⟩ as
  | _, _ => ctx.arbitrary

termination_by
  eval e => sizeOf e
  reduceSym _ xs => sizeOf xs

def myCtx (x y z : Nat) : Context Nat := {
  symbols := ![
    { arity := 0, value := (x : Nat) },
    { arity := 0, value := (y : Nat) },
    { arity := 0, value := (z : Nat) }
    ]
  arbitrary := 42
}

example (x y z : Nat) : eval (myCtx x y z) (Expr.Sym 0 []) = x := by
  --simp [myCtx]
  --simp [NonEmptyList.get!]
  --simp [NonEmptyList.ofList]
  simp [eval] -- !!!!!!! commenting this out breaks. The previous simps are just there to prettify the goal
  rfl

example (x y z) : (myCtx x y z).symbols.get! 0 = ⟨0, x⟩ := rfl

constant x : Nat
constant y : Nat
constant z : Nat

#reduce eval (myCtx x y z) (Expr.Sym 0 []) -- !!!!!!! this here happily reduces to x

[Sebastian Ullrich]

Likely the same issue as in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport.3Awhnf-power - the (elaborator) unifier is very conservative about unfolding well-founded recursion

[Daniel Fabian]

ok... so how can I make progress then? The functions I'm defining are unlikely going to work as pure structural recursion. And if well-founded recursion is not unfolded automatically, how can I produce a proof automatically? The idea is to take variables from a local ctx and pass them into these objects, let lean perform a computation to verify the objects are equal modulo AAC. Then, in the end we can reify the proof into the terms the user wanted.

In fact, when I tried a simp [eval] on the actual definition it fails, claiming the motive is not type correct.

[Leonardo de Moura]

@Daniel Fabian I am assuming you are trying to "proof by reflection", correct?
If yes, then you should not use well-found recursion anyway since they are very expensive to reduce in the kernel.
Another reason is that, as Sebastian pointed out, the elaborator unifier is conservative about them.

ok... so how can I make progress then?

If the goal is proof by reflection, you can always use structural recursion + Nat fuel argument, and then set the argument with a big enough value.

[Daniel Fabian]

yes, correct on all accounts. We can basically make a fake structural with enough fuel. Just need to give a upper bound on the steps. I noticed it when looking at the existing sample code. I still do want to use n-ary trees, though. They should make other things easier.