Zulip Chat Archive

Stream: lean4

Topic: Structural induction for nested inductive types


Parth Shastri (Nov 22 2022 at 00:26):

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 (Nov 22 2022 at 09:46):

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 (Nov 30 2022 at 00:39):

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 (Nov 30 2022 at 00:53):

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 (Nov 30 2022 at 00:54):

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

Sebastian Ullrich (Nov 30 2022 at 08:52):

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 (Nov 30 2022 at 08:59):

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 (Mar 10 2023 at 17:02):

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?


Last updated: Dec 20 2023 at 11:08 UTC