Structural induction for nested inductive types

Stream: lean4

[Parth Shastri]

Is there a way to express structurally inductive functions without manually using rec?
In the following example, Lean is unable to show termination for not and size. I'm not sure what else I could potentially write instead of map and foldr.

inductive Tree
  | leaf : Bool → Tree
  | node : List Tree → Tree

def Tree.not : Tree → Tree
  | leaf b => leaf !b
  | node l => node (l.map not)

def Tree.size : Tree → Nat
  | leaf _ => 1
  | node l => l.foldr (λ t n => size t + n) 0

My current workaround for this is fairly verbose as it has to deal with the fact that rec is noncomputable by default.

namespace Tree

variable
  {motive₁ : Tree → Sort u}
  {motive₂ : List Tree → Sort u}
  (leaf : ∀ b, motive₁ (leaf b))
  (node : ∀ l, motive₂ l → motive₁ (node l))
  (nil : motive₂ .nil)
  (cons : ∀ head tail, motive₁ head → motive₂ tail → motive₂ (head :: tail))

mutual

private def rec' : ∀ t, motive₁ t
  | .leaf b => leaf b
  | .node l => node l (rec_1' l)

private def rec_1' : ∀ l, motive₂ l
  | .nil => nil
  | .cons head tail => cons head tail (rec' head) (rec_1' tail)

end

mutual

private theorem rec_ : ∀ t, rec leaf node nil cons t = rec' leaf node nil cons t
  | .leaf b => by unfold rec'; rfl
  | .node l => by unfold rec'; exact congrArg (node l) (rec_1_ l)

private theorem rec_1_ : ∀ l, rec_1 leaf node nil cons l = rec_1' leaf node nil cons l
  | .nil => by unfold rec_1'; rfl
  | .cons head tail => by unfold rec_1'; exact congr (congrArg (cons head tail) (rec_ head)) (rec_1_ tail)

end

@[csimp]
private theorem rec_eq_rec' : @rec = @rec' := by
  funext motive₁ motive₂ leaf node nil cons t
  apply rec_

@[csimp]
private theorem rec_1_eq_rec_1' : @rec_1 = @rec_1' := by
  funext motive₁ motive₂ leaf node nil cons t
  apply rec_1_

end Tree

def Tree.not : Tree → Tree := rec
  (λ b => leaf !b)
  (λ _ => node)
  []
  (λ _ _ => .cons)

def Tree.size : Tree → Nat := rec
  (λ _ => 1)
  (λ _ n => n)
  0
  (λ _ _ => .add)

[Jannis Limperg]

Use well-founded recursion (terminating_by and decreasing_by; I think there should be docs in the manual). Lean doesn't do structural recursion for nested inductive types.

[Parth Shastri]

For anyone else that runs into this, the solution is to copy the definitions of map and foldr:

def Tree.not : Tree → Tree
  | leaf b => leaf !b
  | node l => node (map_not l)
where
  map_not
    | [] => []
    | t :: l => not t :: map_not l

def Tree.size : Tree → Nat
  | leaf _ => 1
  | node l => foldr_size l
where
  foldr_size
    | [] => 0
    | t :: l => size t + foldr_size l

[James Gallicchio]

Just to be clear, copying the List stuff is exactly what Lean is doing to compile the nested inductive in the first place :P but it would be nice if Lean had a computable, autogenerated rec for nested inductives for exactly this reason

[James Gallicchio]

(I assume this is one of the things on the dev list for after the new code generator is done)

[Sebastian Ullrich]

What surface-level recursion syntax is accepted is basically completely orthogonal to what it's compiled down to. The above code follows the structure of the underlying mutual inductive types, but it's still compiled down to well-founded recursion as there is no elaboration support for mutual structural recursion either. So whether there is a computable recursor does not directly impact what Lean accepts.

[Sebastian Ullrich]

A different solution to mutual recursion is to use dependently typed versions of map etc. that come with a proof that the element is part of the list, which can be used to prove well-founded recursion automatically. One idea for making the initial code just work is to have the WF elaborator do such function substitutions automatically.

[Logan Murphy]

I'm trying to show termination for functions on a similar rosetree type to Parth's. I'm trying to figure out how I'm meant to use termination_by and decreasing_by. I get the motivation behind them, but it seems like I'm misunderstanding how to use them in practice

import Mathlib

inductive Tree (α : Type u)
| node : α → List (Tree α) → Tree α

variable {α : Type u} {β : Type v}

namespace Tree

def subtrees : Tree α → List (Tree α)
| Tree.node _ l => l

def root : Tree α → α
| Tree.node x _ => x
end Tree

mutual
def treeSize : Tree α → Nat
  | Tree.node _ l => forestSize l + 1

def forestSize : List (Tree α) → Nat
  | [] => 0
  | t :: l => treeSize t + forestSize l
end
termination_by
  treeSize t => sizeOf t
  forestSize l => sizeOf l

-- I assume this would be useful, but I'm not sure *how* I would use it
theorem tree_gt_subtrees : (t : Tree α) → forestSize t.subtrees < treeSize t
| Tree.node x l =>
  by
    rw [treeSize, Tree.subtrees]
    cases l with
    | nil => rw [forestSize, zero_add, Nat.lt_one_iff]
    | cons h t => rw [forestSize, lt_add_iff_pos_right, Nat.lt_succ]

def treeMap (f : α → β) : Tree α → Tree β
| Tree.node x l =>
  Tree.node (f x) (l.map (treeMap f))

-- I think this suggests  to Lean to use the wf relation Nat.lt on treeSize?
termination_by
  treeMap _ t => treeSize t
-- show that treeSize actually decreases?
decreasing_by
  simp_wf
  -- α: Type u
  -- a✝¹a✝: Tree α
  -- ⊢ treeSize a✝ < treeSize a✝¹
  admit

The goal I'm left with in decreasing_by doesn't seem to make sense -- any sense of what am I doing wrong here?