# Nested and mutual structurally recursive definitions

Example of a term structure with two constructors taking lists of terms.

Require Import Equations.Equations.
Require Import Program Arith List Compare_dec.
Import ListNotations.

A nested recursive definition of terms with lists of terms

Inductive term : Set :=
| Var (n : nat)
| Lam (t : term)
| App (t : term) (l : list term)
| MetaVar (n : nat) (l : list term).

Defining capture-avoiding substitution for this language: the case of variables.

Equations subst_var (k : nat) (u : term) (t : nat) : term :=
subst_var k u n with k ?= n
{ | Equ;
| GtVar n;
| LtVar (pred n) }.

Nested recursive definition using a top-level where definition.
The nested recursive fixpoint defined by subst_tlist can be used multiple time in subst_term, and of course recursively call itself and subst_term. The regular structural guardedness check is run on this definition to check that it is terminating. Note that one can optionally add a struct x annotation to where clauses to indicate which arguments decreases explicitely, otherwise only the last argument is tried.

Equations subst_term (k : nat) (u : term) (t : term) : term := {
subst_term k u (Var n) ⇒ subst_var k u n;
subst_term k u (Lam t) ⇒ Lam (subst_term (S k) u t);
subst_term k u (App t l) ⇒ App (subst_term k u t) (subst_tlist k u l);
subst_term k u (MetaVar t l) ⇒ MetaVar t (subst_tlist k u l) }

where subst_tlist (k : nat) (u : term) (t : list term) : list term := {
subst_tlist k u nilnil;
subst_tlist k u (cons t ts) ⇒ cons (subst_term k u t) (subst_tlist k u ts) }.

Remark that our definition of subst_tlist is equivalent to a List.map: but we need the "expanded" version to properly recognize recursive calls.

Lemma nested_map k u t : subst_tlist k u t = List.map (subst_term k u) t.
Proof.
induction t; simpl; rewrite ?IHt; trivial.
Qed.

The elimination principle generated from this definition is giving a conjunction of two predicates as result. One may want to instantiate P0 with Forall P to recover a map-like elimination principle.

Check subst_term_elim
: (P : nat term term term Type)
(P0 : nat term list term list term Type),
( (k : nat) (u : term) (n : nat), P k u (Var n) (subst_var k u n))
( (k : nat) (u t : term),
P (S k) u t (subst_term (S k) u t) P k u (Lam t) (Lam (subst_term (S k) u t)))
( (k : nat) (u t0 : term) (l : list term),
P k u t0 (subst_term k u t0)
P0 k u l (subst_tlist k u l)
P k u (App t0 l) (App (subst_term k u t0) (subst_tlist k u l)))
( (k : nat) (u : term) (n0 : nat) (l0 : list term),
P0 k u l0 (subst_tlist k u l0) P k u (MetaVar n0 l0) (MetaVar n0 (subst_tlist k u l0)))
( (k : nat) (u : term), P0 k u []%list []%list)
( (k : nat) (u t : term) (l : list term),
P k u t (subst_term k u t)
P0 k u l (subst_tlist k u l)
P0 k u (t :: l)%list (subst_term k u t :: subst_tlist k u l)%list)

( (k : nat) (u t : term), P k u t (subst_term k u t)) ×
( (k : nat) (u : term) (t : list term), P0 k u t (subst_tlist k u t)).

One can experiment to see that this provides the right induction hypotheses for App and MetaVar

Lemma subst_subst k u t : subst_term k u t = subst_term k u t.
Proof.
revert k u t.
refine (fst (subst_term_elim (fun k u t cc = c) (fun k u l cc = c) _ _ _ _ _ _));
trivial.
Qed.