Improve Equations wf discussing subterm relation

[thomas-lamiaux]

Currently, the subterm relation is not discussed in the tutorial about Equations and well-founded recursion, as at the moment of writing we were lacking a good example. Once, one is found, it would be good to do so.

[thomas-lamiaux]

I was thinking about a simple MLTT like theory

Inductive term : Type := 
| tVar : nat -> term 
| tApp : term -> list term -> term 
| tAbs : string -> term 
| tProd : string -> term -> term 
| tUniv : nat -> term 

and computing sth on it that would require rec call on the args of the app. Sth of the form

Fixpoint foo (t : term) : ??? := 
match t with 
| tApp u lv => fold_right ??? (map foo lv)
end.

EDIT: it didn't work

What do you think @MevenBertrand ?

[MevenBertrand]

You should try something with an infinitary-branching tree (with a constructor leaf : (nat -> tree) -> tree), say): for these, you cannot define a nat-valued depth, since you would want $\mathrm{size} (\mathrm{leaf} f) = 1 + \max_{i \in \mathbb{N}} \mathrm{size}(f i)$, but there is no reason for the max to be an integer (consider a tree where the i-th leaf has depth i). So maybe try to adapt an example from binary trees to such a setting? Maybe one where you need lexicographic order on two arguments or something like this?