Proving termination of function which uses helper functions

Stream: new members

[Ayhon]

Consider the following example (see code)

inductive Tree: Type -> Type where
| Leaf  {A: Type}(value: A) : Tree A
| Branch{A: Type}(children: Nat -> Tree A): Tree A

def Tree.continue' {A B: Type}(f: Tree A -> Tree B): Tree A -> Tree B
| Leaf value => f (Leaf value)
| Branch children => Branch (f ∘ children)

def Tree.flatMap{A B: Type}(f: A -> Tree B):Tree A -> Tree B
| Leaf value => f value
| self@(Branch cont) =>
    self.continue' (·.flatMap f)

Lean4 complains that Tree.flatMap cannot be proven terminating in this instance. However, if I unfold the definition of continue' in the Tree.flatMap implementation (see code), then termination is accepted.

I see that this is because in the first case I'm not executing the function on a subterm on the arguments, but I don't know how to prove termination in this case in a "simple" way. I feel it shouldn't be too difficult, but proofs of termination is an area in Lean4 I'm not too familiar with yet.

Any guidance is appreciated :pray:

[Edward van de Meent]

I think lean would like to have some simp lemmas about continue'

[Ayhon]

Edward van de Meent said:

I think lean would like to have some simp lemmas about continue'

What kind of lemmas? Those supported by definitional equality? This is what I first thought of, but it doesn't seem to be enough (see code)

inductive Tree: Type -> Type where
| Leaf  {A: Type}(value: A) : Tree A
| Branch{A: Type}(children: Nat -> Tree A): Tree A

def Tree.continue' {A B: Type}(f: Tree A -> Tree B): Tree A -> Tree B
| Leaf value => f (Leaf value)
| Branch children => Branch (f ∘ children)

@[simp]
theorem Tree.continue'_branch{A B: Type}(f: Tree A -> Tree B)(children: Nat -> Tree A)
: Tree.continue' f (Branch children) = Branch (f ∘ children)
:= by rfl

def Tree.flatMap{A B: Type}(f: A -> Tree B):Tree A -> Tree B
| Leaf value => f value
| self@(Branch cont) =>
    self.continue' (·.flatMap f)

[Johannes Tantow]

Doesn't your definition allow me to encode infinite trees? Then the functions are probably not terminating in the most cases either.
def infiniteTree: Tree Nat := Tree.Branch (fun n => Tree.Leaf n)

Do you need that many children in your tree or would a list of trees suffice?

[Ayhon]

Actually, this is a simplification of some other definitions I have, but without as much context. I made the mistake of using Nat, which is infinite, where something like Fin n would have been more appropriate. However, it's still true that Lean4 accepts the definition of flatMap if I unfold continue', which is why I didn't edit my previous message. See https://live.lean-lang.org/#codez=JYOwJgrgxgLsBuBTABAFQE6MQLjQTwAcUBaAPnyOQHcALRTAKAB9kAZRAQwDNlkBvAIK5UhRAF8AFPA4AbCDmQCAlMmGYUA5sgBC6DiCg1Bw0ZMPAZYTCFwA5DjGRk06xUrVZFDBmEQ8MWAB0UAD2IHAg8gDk/AI6JkSSXB4aTuQBKNruLp5xzhk6WuzcyNJyKAC85DwSxTxl8kpauvqGyOaW1shVOnoGNMgSPIAYRO00FlaIIE0+fjmIgVwyDgCyHASC8RTiQ7h56a5Z2AX784UsdaWy8t3VV+VaAM6IMlwAAhIt/WMT1ipVDF4vC+bS4EBAyAAHrdBh1JhDoUxSItljA1gRkFwlEA

[Ayhon]

Johannes Tantow said:

Doesn't your definition allow me to encode infinite trees? Then the functions are probably not terminating in the most cases either.
def infiniteTree: Tree Nat := Tree.Branch (fun n => Tree.Leaf n)

Do you need that many children in your tree or would a list of trees suffice?

Actually, upon thinking about it more closely, while this definition does encode inifinite trees, it does so lazily so there's no worries of it being non-terminating. In the end, I'm just morphing the definition of the children function through function composition. This is evident by the generated SizeOf instance for it, which is constantly 1 (source).