I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators?
In particular, normalizing the application of an eliminator to an inductive value "obviously" halts, since the head of the elimination is structurally smaller each time.
But, I'm wondering, how does it fit into the structurally-shrinking argument of hereditary substitution? For example, in Harper and Licata's presentation, hereditary substitution is always strictly decreasing, structurally in the value being substituted into, or in the shape of the type of the variable being replaced.
But, if we have:
$natElim: (m : Nat \to Set) \to m\ 0 \to (k : Nat \to m\ k \to m (succ\ k) ) \to (k : Nat) \to m\ k$
and we are computing $[1/x](natElim\ m\ z\ (\lambda k\ p\ldotp t_1)\ x)$, we must compute:
- $[0/x](natElim\ m\ z\ s\ x) = t_2$,
- $[0/k]t_2 = t_3$
- $[t_2/p]t_3 =t_4$ to get a result of $t_4$.
But these are not decreasing in either the type of $x$ or the term being substituted into. The first two are decreasing in the value replacing the variable, but the third is not.
Is their prior work on this? I can think of ad-hoc ways to make the decreasing size argument work for Nat, Vec, etc. But is there a general argument for inductive types?
This is possibly related to my previous question question: I'm not sure if this falls under the "large eliminators" described there. If this only works for "small eliminators", I'm still interested in a reference for this.