1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
(** printing elimination %\coqdoctac{elimination}% *)
(** printing <= %\rightarrow% #⇐# *)
(** * Nested and mutual structurally recursive definitions
Example of a term structure with two constructors taking lists of terms. *)
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
: forall (P : nat -> term -> term -> term -> Type)
(P0 : nat -> term -> list term -> list term -> Type),
(forall (k : nat) (u : term) (n : nat), P k u (Var n) (subst_var k u n)) ->
(forall (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))) ->
(forall (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))) ->
(forall (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))) ->
(forall (k : nat) (u : term), P0 k u []%list []%list) ->
(forall (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) ->
(forall (k : nat) (u t : term), P k u t (subst_term k u t)) *
(forall (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.
|
