Tree with finite map of children

Stream: new members

[Jules Jacobs]

I would like to define a tree data type where a node consists of a finite map from naturals to children:

inductive tree where
  | leaf : Bool → tree
  | node : finmap Nat tree → tree

A finmap K V should be like K → Option V but with the constraint that only finitely many K map to Some. I am having trouble arranging this in such a way that I can write functions by recursion and prove theorems by induction. For example, a function that negates all the booleans at the leaves, and prove that doing this twice is the identity. What is the right approach in this situation?

[Matt Diamond]

maybe something like this?

inductive tree where
  | leaf (b : Bool) : tree
  | node {n} (f : Fin n → tree) : tree

[Matt Diamond]

import Mathlib

inductive tree where
| leaf (b : Bool) : tree
| node {n} (f : Fin n → tree) : tree

def negate : tree → tree
| .leaf b => .leaf !b
| .node f => .node (fun n => negate (f n))

example : (negate ∘ negate) = id := by
  ext t
  rw [Function.comp_apply, id_eq]
  induction' t with l n f IH
  · simp [negate]
  · simp [negate, IH]

[Timo Carlin-Burns]

If you really need Nat -> Option Tree it's going to be a pain. Lean's limited support for nested inductive types does allow you to write | node : (Nat → (Option Tree)) → Tree, but it doesn't allow you to add any further arguments which depend on that function, so you'll have trouble adding a finiteness condition. In the future, hopefully we'll have a proper datatypes package which supports use cases like this, but for now we're stuck with some ugly workarounds. The best way I know is to create an initial inductive type without the side conditions and then define Tree as a subtype of that.

-- A tree data type which doesn't quite meet the specification - each node can have potentially infinite children
inductive PreTree where
  | leaf : Bool → PreTree
  | node : (Nat → Option PreTree) → PreTree

def IsFinmap (f : Nat → Option α) : Prop :=
  ∃ n, ∀ i, i ≥ n → f i = none

namespace PreTree

inductive IsFinite : PreTree → Prop
| leaf (b : Bool) : IsFinite (leaf b)
| node {f : Nat → Option PreTree} : IsFinmap f → (∀ i c, f i = some c → IsFinite c) → IsFinite (node f)

end PreTree

structure Tree where
  toPreTree : PreTree
  isFinite : toPreTree.IsFinite

[Matt Diamond]

I suspect the Option requirement is an #xy problem... if the requirement is only "a finite map from naturals to children" then there are better ways to handle it, I think

[Timo Carlin-Burns]

If you do need nested Option Tree, the other annoying thing is that it becomes impossible to use structural recursion. The typical way of doing recursive definitions with a nested inductive type is to establish a well-founded relation like so:

import Std

inductive PreTree where
  | leaf : Bool → PreTree
  | node : (Nat → Option PreTree) → PreTree

namespace PreTree

def IsChildOf (x y : PreTree) : Prop :=
  ∃ f, y = node f ∧ ∃ i, x ∈ f i

@[simp]
theorem not_isChildOf_leaf (x : PreTree) (b : Bool) : ¬x.IsChildOf (leaf b) := by
  simp [IsChildOf]

@[simp]
theorem isChildOf_node (x : PreTree) (f : Nat → Option PreTree) : x.IsChildOf (node f) ↔ ∃ i, x ∈ f i := by
  simp [IsChildOf]

#check PreTree.rec -- Nested inductive types have recurses with multiple motives

-- Luckily, once we define this well-founded relation, we'll never have to use the recursor again.
theorem wellFounded_IsChildOf : WellFounded IsChildOf := by
  constructor
  intro x
  apply PreTree.rec (motive_1 := Acc IsChildOf) (motive_2 := fun o : Option PreTree ↦ ∀ y ∈ o, Acc IsChildOf y)
  · intro b
    constructor
    simp
  · intro f ih
    constructor
    intro y h
    suffices ∃ i, y ∈ f i by
      rcases this with ⟨i, hi⟩
      exact ih i y hi
    simpa using h
  · simp
  · simp

instance : WellFoundedRelation PreTree where
  rel := IsChildOf
  wf := wellFounded_IsChildOf

def flip : PreTree → PreTree
  | leaf b => leaf !b
  | node f => node fun i ↦
      match h : f i with
      | some c =>
        have : ∃ i, c ∈ f i := ⟨i, h⟩
        some (flip c)
      | none => none
termination_by t => t

theorem flip_flip : (t : PreTree) → flip (flip t) = t
  | leaf b => by simp [flip]
  | node f => by
    simp [flip]
    funext i
    match h : f i with
    | some c =>
      have : ∃ i, c ∈ f i := ⟨i, h⟩
      simp [flip_flip c]
    | none => simp
termination_by t => t

[Timo Carlin-Burns]

Another option if you need the mapping from naturals to children to be sparse is to split the Nat -> Option Tree into two components apply : Nat -> Tree and contains : Nat -> Bool. Then apply i is a garbage value whenever contains i is false.

inductive PreTree where
  | leaf : Bool → PreTree
  | node' (apply : Nat → PreTree) (contains : Nat → Bool) (isFinite : ∃ n, ∀ i, i ≥ n → contains i = ff)

This avoids nested inductives so gives you nice structural recursion again. You could then define Tree as a quotient of PreTree to ignore the garbage values.

[Jules Jacobs]

Thanks for the helpful answer, that's exactly what I needed!