Require Import Arith.
Require Import Axioms.
Require Import AuxLib.
Require Import Nominal.
Require Import STLC.
Require Import Wf_nat.
Module MakeSTLC <: STLC.
Basic definitions |
| Term variables. |
Definition tmvar := mkAtomRec 0.
Definition tmvarP := mkAtomPset tmvar.
| STLC types. |
Inductive ty : Set :=
| unit : ty
| arrow : ty -> ty -> ty.
Definition tyP := mkIdPset tmvar ty.
Phi n is the set of all terms whose bound variables have index
less than n. Thus, Phi 0 corresponds to those terms with no
dangling bound variables. Free variables are still represented
using names.
|
Inductive Phi : nat -> Set :=
| pdot : forall (n : nat), Phi n
| pfree : forall (n : nat), tmvar -> Phi n
| pbound : forall (n i : nat), i < n -> Phi n
| papp : forall (n : nat), Phi n -> Phi n -> Phi n
| plam : forall (n : nat), ty -> Phi (S n) -> Phi n.
We need to take advantage of proof irrelevance when considering
equality on Phi.
|
Lemma pbound_eq :
forall (n i i': nat), (i = i') ->
forall (p : i < n) (q : i' < n),
pbound n i p = pbound n i' q.
Hint Resolve pbound_eq : core nominal.
| Free variables. |
Fixpoint Phi_fv (n : nat) (x : Phi n) {struct x} : aset tmvar :=
match x with
| pdot _ => empty
| pfree _ a => singleton a
| pbound _ _ _ => empty
| papp _ s t => union (Phi_fv _ s) (Phi_fv _ t)
| plam _ _ s => Phi_fv _ s
end.
Implicit Arguments Phi_fv [n].
Size. The fact that 1 + x converts to S x is helpful when defining
the recursion combinator below, since it proceeds by induction on natural
numbers (the initial value being the size of a term).
|
Fixpoint Phi_size (n : nat) (x : Phi n) {struct x} : nat :=
match x with
| pdot _ => 1
| pfree _ _ => 1
| pbound _ _ _ => 1
| papp _ s t => 1 + (Phi_size _ s) + (Phi_size _ t)
| plam _ _ s => 1 + (Phi_size _ s)
end.
Implicit Arguments Phi_size [n].
Lemma Phi_size_eq_O :
forall (T : Type) (n : nat) (x : Phi n), Phi_size x = 0 -> T.
Lemma Phi_size_lt_O :
forall (T : Type) (n : nat) (x : Phi n), Phi_size x <= 0 -> T.
We need ``weakening'' on terms in order to define substitution:
Any term in Phi n is also a term in Phi (S n) modulo the proofs
carried by pbound subterms.
|
Fixpoint Phi_weaken (n : nat) (x : Phi n) {struct x} : Phi (S n) :=
match x in Phi n return Phi (S n) with
| pdot _ => pdot _
| pfree _ a => pfree _ a
| pbound _ i pf => pbound _ i (le_S _ _ pf)
| papp _ s t => papp _ (Phi_weaken _ s) (Phi_weaken _ t)
| plam _ T s => plam _ T (Phi_weaken _ s)
end.
Implicit Arguments Phi_weaken [n].
Case analysis. This lemma is useful when built-in tactics fail to provide
similar functionality, for example when you want to analyze x : Phi (S n)
and case fails.
|
Lemma Phi_case :
forall (n : nat) (P : Phi n -> Type),
(P (pdot n)) ->
(forall a, P (pfree n a)) ->
(forall i pf, P (pbound n i pf)) ->
(forall s t, P (papp n s t)) ->
(forall T s, P (plam n T s)) ->
(forall x, P x).
| Well-founded induction on size. |
Lemma Phi_ind_size_multi :
forall (P : forall (n : nat), Phi (S n) -> Type),
(forall n x, (forall m y, Phi_size y < Phi_size x -> P m y) -> P n x) ->
(forall n x, P n x).
Lemma Phi_ind_size_single :
forall (n : nat) (P : Phi n -> Type),
(forall x, (forall y, Phi_size y < Phi_size x -> P y) -> P x) ->
(forall x, P x).
Permutations |
Fixpoint Phi_perm
(n : nat) (p : permt tmvar) (x : Phi n) {struct x} : Phi n
:=
match x in Phi n return Phi n with
| pdot _ => pdot _
| pfree _ a => pfree _ (perm tmvarP p a)
| pbound _ i pf => pbound _ i pf
| papp _ s t => papp _ (Phi_perm _ p s) (Phi_perm _ p t)
| plam _ T s => plam _ T (Phi_perm _ p s)
end.
Implicit Arguments Phi_perm [n].
Definition PhiPermR (n : nat) : PsetT tmvar (Phi n).
| Permutation preserves the size of a term. |
Lemma Phi_size_perm :
forall (n : nat) (p : permt tmvar) (x : Phi n),
Phi_size (Phi_perm p x) = Phi_size x.
Abstraction and instantiation |
Turn a free variable into a bound variable (an index). We turn a term
in Phi n into a term in Phi (S n) and choose n as the new index.
|
Fixpoint abs
(n : nat) (a : tmvar) (x : Phi n) {struct x}
: Phi (S n)
:=
match x in Phi n return Phi (S n) with
| pdot _ => pdot _
| pfree i a' =>
if atom_eqdec tmvar a a' then pbound (S i) i (lt_n_Sn _)
else pfree _ a'
| pbound i m pf => pbound (S i) m (lt_S _ _ pf)
| papp _ s t => papp _ (abs _ a s) (abs _ a t)
| plam _ T s => plam _ T (abs _ a s)
end.
Implicit Arguments abs [n].
| Turn the greatest index (bound variable) in a term into a free variable. A more general version of this function would instantiate the index with an arbitrary term. |
Definition inst_aux
(n' : nat) (a : tmvar) (x : Phi n') (n : nat) (wf : n' = S n) : Phi n.
Definition inst (n : nat) (a : tmvar) (x : Phi (S n)) : Phi n :=
inst_aux (S n) a x n (refl_equal _).
Implicit Arguments inst [n].
The following rewrites make it easier to work with inst. It is
not usually helpful to unfold inst to inst_aux.
|
Lemma inst_papp :
forall (n : nat) (a : tmvar) (s t : Phi (S n)),
inst a (papp _ s t) = papp _ (inst a s) (inst a t).
Lemma inst_plam :
forall (n : nat) (a : tmvar) (s : Phi (S (S n))) (T : ty),
inst a (plam _ T s) = plam _ T (inst a s).
abs preserves the size of terms.
|
Lemma Phi_size_abs :
forall (n : nat) (x : Phi n) (a : tmvar),
Phi_size (abs a x) = Phi_size x.
inst preserves the size of terms.
|
Lemma Phi_size_inst :
forall (n : nat) (x : Phi (S n)) (a : tmvar),
Phi_size (inst a x) = Phi_size x.
Permutations commute with abs.
|
Lemma Phi_perm_abs :
forall n p c (s : Phi n),
Phi_perm p (abs c s) = abs (perm tmvarP p c) (Phi_perm p s).
Swapping pseudo-commutes with inst under certain conditions.
|
Lemma Phi_swap_inst :
forall (n : nat) (x : Phi (S n)) (a c d : tmvar),
~ In c (Phi_fv x) -> ~ In d (Phi_fv x) ->
perm (PhiPermR n) [(c, d)] (inst a x) = inst (perm tmvarP [(c, d)] a) x.
Swapping commutes with inst under certain conditions.
|
Lemma Phi_swap_inst_commute :
forall (n : nat) (x : Phi (S n)) (a c d : tmvar),
a <> c -> a <> d ->
perm (PhiPermR n) [(c, d)] (inst a x) =
inst a (perm (PhiPermR (S n)) [(c, d)] x).
inst is the inverse of abs.
|
Lemma inst_abs_inv :
forall (n : nat) (x : Phi n) (a : tmvar), inst a (abs a x) = x.
abs is the inverse of inst under certain conditions.
|
Lemma abs_inst_inv :
forall (n : nat) (x : Phi (S n)) (a : tmvar),
~ In a (Phi_fv x) -> abs a (inst a x) = x.
The free variables of abs a x are the obvious ones.
|
Lemma Phi_fv_abs :
forall (n : nat) (x : Phi n) (a : tmvar),
Phi_fv (abs a x) = remove a (Phi_fv x).
User-level abstraction for terms |
Definition tm : Set := Phi 0.
Definition tmP := PhiPermR 0.
Definition dot : tm := pdot 0.
Definition var (a : tmvar) : tm := pfree 0 a.
Definition app (s t : tm) : tm:= papp 0 s t.
Definition lam (x : tmvar) (T : ty) (b : tm) : tm := plam 0 T (abs x b).
Permutations |
Section STLCPermutations.
Variable p : permt tmvar.
Variable c : tmvar.
Variable T : ty.
Variables s t : tm.
Theorem perm_dot : perm tmP p dot = dot.
Theorem perm_var : perm tmP p (var c) = var (perm tmvarP p c).
Theorem perm_app :
perm tmP p (app s t) = app (perm tmP p s) (perm tmP p t).
Theorem perm_lam :
perm tmP p (lam c T s) = lam (perm tmvarP p c) T (perm tmP p s).
End STLCPermutations.
Free variables |
Definition fvar : tm -> aset tmvar := Phi_fv (n:= 0).
Theorem fvar_dot : fvar dot = empty.
Theorem fvar_var : forall a, fvar (var a) = singleton a.
Theorem fvar_app : forall s t, fvar (app s t) = union (fvar s) (fvar t).
Theorem fvar_lam : forall a T s, fvar (lam a T s) = remove a (fvar s).
Alpha-equality |
Lemma swap_in_abs :
forall (n : nat) (s : Phi n) (a b : tmvar),
b <> a ->
~ In a (Phi_fv (Phi_perm [(a, b)] s)) ->
abs b (Phi_perm [(a, b)] s) = abs a s.
Lemma eq_lam_diff :
forall a b T T' s s',
T = T' ->
a <> b ->
~ In b (fvar s) ->
s = perm tmP [(a, b)] s' ->
lam a T s = lam b T' s'.
Theorem eq_lam :
forall a b T s,
~ In b (fvar s) ->
lam a T s = lam b T (perm tmP [(a, b)] s).
Structural induction |
Theorem tm_induction_weak :
forall (P : tm -> Type),
(P dot) ->
(forall a, P (var a)) ->
(forall s, P s -> forall t, P t -> P (app s t)) ->
(forall a T s, P s -> P (lam a T s)) ->
forall x : tm, P x.
Theorem tm_induction :
forall (P : tm -> Type) (F : aset tmvar),
(P dot) ->
(forall a, P (var a)) ->
(forall s, P s -> forall t, P t -> P (app s t)) ->
(forall a, ~ In a F -> forall T, forall s, P s -> P (lam a T s)) ->
forall x : tm, P x.
Recursion |
Section Recursion.
Variables (R : Set) (RP : PsetT tmvar R).
Variable (f_dot : R).
Variable (f_var : tmvar -> R).
Variable (f_app : tm -> R -> tm -> R -> R).
Variable (f_lam : tmvar -> ty -> tm -> R -> R).
Variable (F : aset tmvar).
Variable (supp_dot : supports RP F f_dot).
Variable (supp_var : supports (tmvarP ^-> RP) F f_var).
Variable (supp_app : supports (tmP ^-> RP ^-> tmP ^-> RP ^-> RP) F f_app).
Variable (supp_lam : supports (tmvarP ^-> tyP ^-> tmP ^-> RP ^-> RP) F f_lam).
Variable (fcb :
exists b, ~ In b F /\ forall x y z, freshP RP b (f_lam b x y z)).
Derive Dependent Inversion tm_inv with (Phi 0) Sort Set.
Lemma Phi_size_lt_papp_fun :
forall n m s t, Phi_size (papp n s t) <= S m -> Phi_size s <= m.
Implicit Arguments Phi_size_lt_papp_fun [n m s t].
Lemma Phi_size_lt_papp_arg :
forall n m s t, Phi_size (papp n s t) <= S m -> Phi_size t <= m.
Implicit Arguments Phi_size_lt_papp_arg [n m s t].
Lemma Phi_size_lt_plam :
forall n m a T s, Phi_size (plam n T s) <= S m -> Phi_size (inst a s) <= m.
Implicit Arguments Phi_size_lt_plam [n m a T s].
Our goal here is to define recursive functions over terms by induction
on their size. This translates to induction on a natural number which
bounds the size of the term. All the arguments here are important: n
is required since the function is defined by induction on the structure
of n, x is the term we actually care about, and the proof ensures
that we don't have to deal with non-sensical combinations of n and x.
The proof is of an le relation and not an eq relation due to how
recF makes recursive calls. We could, in theory, use an eq relation
if we were willing to define recF by well-founded induction on n, but
that seems to pose its own problems.
|
Definition recF :
forall (n : nat) (x : Phi 0), Phi_size x <= n -> R.
The particular n and proof supplied to recF don't matter.
|
Lemma recF_stable :
forall (n m : nat) (x : tm) (pfn : Phi_size x <= n) (pfm : Phi_size x <= m),
recF n x pfn = recF m x pfm.
Lemma recF_stable_gen :
forall (n m : nat) (x y : tm), x = y ->
forall (pfn : Phi_size x <= n) (pfm : Phi_size y <= m),
recF n x pfn = recF m y pfm.
Hint Resolve recF_stable_gen : core.
| Define the recursion combinator, as seen by the user. Most of the cases for how it evaluates are straightforward. |
Definition tm_rec (x : tm) : R := recF (Phi_size x) x (le_n _).
Theorem tm_rec_dot : tm_rec dot = f_dot.
Theorem tm_rec_var : forall a, tm_rec (var a) = f_var a.
Theorem tm_rec_app :
forall s t, tm_rec (app s t) = f_app s (tm_rec s) t (tm_rec t).
Proving the rewrite rule for the lam case requires that we prove
the following two properties simultaneously. There may be an easier
way, but at least it doesn't seem that this particular method is
specific to the object-language at hand.
It's only at this point where we need to know the support of f_dot,
f_var, f_app, and f_lam, and know that fcb holds.
|
Let rewrite_prop (n : nat) :=
forall a T s, Phi_size (lam a T s) <= n ->
~ In a F -> tm_rec (lam a T s) = f_lam a T s (tm_rec s).
Let swap_prop (n : nat) :=
forall x c d pf pf', ~ In c F -> ~ In d F ->
perm RP [(c, d)] (recF n x pf) = recF n (perm tmP [(c, d)] x) pf'.
Lemma rewrite_to_swap :
forall (n : nat), (forall m, m <= n -> rewrite_prop m) -> swap_prop n.
Lemma swap_to_rewrite :
forall (n : nat), (forall m, m < n -> swap_prop m) -> rewrite_prop n.
Lemma rewrite_and_swap : forall m, rewrite_prop m /\ swap_prop m.
Theorem tm_rec_lam :
forall a T s, ~ In a F -> tm_rec (lam a T s) = f_lam a T s (tm_rec s).
Theorem tm_rec_supp :
supports (tmP ^-> RP) F tm_rec.
End Recursion.
Constructor distinctness |
Section Distinctness.
Variables a b : tmvar.
Variables T : ty.
Variables s t q r : tm.
Theorem distinctness_dot_var: dot <> var a.
Theorem distinctness_dot_app : dot <> app s t.
Theorem distinctness_dot_lam : dot <> lam a T s.
Theorem distinctness_var_dot : var a <> dot.
Theorem distinctness_var_app : var a <> app s t.
Theorem distinctness_var_lam : var a <> lam b T s.
Theorem distinctness_app_dot : app s t <> dot.
Theorem distinctness_app_var : app s t <> var a.
Theorem distinctness_app_lam : app s t <> lam a T q.
Theorem distinctness_lam_dot : lam a T s <> dot.
Theorem distinctness_lam_var : lam a T s <> var b.
Theorem distinctness_lam_app : lam a T s <> app q r.
End Distinctness.
Injectivity for constructors |
Some of the lemmas in this section are needed because the injection
tactic fails to produce useful hypotheses.
|
Theorem injection_var : forall a b, var a = var b -> a = b.
Lemma injection_papp_fun :
forall n s s' t t', papp n s t = papp n s' t' -> s = s'.
Theorem injection_app_fun : forall s s' t t', app s t = app s' t' -> s = s'.
Lemma injection_papp_arg :
forall n s s' t t', papp n s t = papp n s' t' -> t = t'.
Theorem injection_app_arg : forall s s' t t', app s t = app s' t' -> t = t'.
Theorem injection_lam_ty :
forall a a' T T' s s',
lam a T s = lam a' T' s' ->
(T = T').
Lemma injection_plam :
forall (n : nat) (T T' : ty) (s s' : Phi (S n)),
plam n T s = plam n T' s' -> s = s'.
Lemma abs_eq :
forall (n : nat) (a : tmvar) (s s' : Phi n),
abs a s = abs a s' -> s = s'.
Lemma abs_neq :
forall (n : nat) (a a' : tmvar) (s s' : Phi n),
a <> a' ->
abs a s = abs a' s' ->
~ In a (Phi_fv s') /\ s = Phi_perm [(a, a')] s'.
Theorem injection_lam_body :
forall a a' T T' s s',
lam a T s = lam a' T' s' ->
(a = a' /\ s = s') \/
(a <> a' /\ ~ In a (fvar s') /\ s = perm tmP [(a, a')] s').
End MakeSTLC.