Nested and mutual structurally recursive definitions
From Equations Require Import 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 ⇒
{ | Eq ⇒ u;
| Gt ⇒ Var n;
| Lt ⇒ Var (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 nil ⇒ nil;
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 c ⇒ c = c) (fun k u l c ⇒ c = c) _ _ _ _ _ _));
trivial.
Qed.
This page has been generated by coqdoc