Require Import STLC.
Require Import Axioms.
Module UseSTLC (STLCImpl : STLC).
Import STLCImpl.
| Prove a specialized induction principle for terms |
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 s, P s -> P (lam a T s)) ->
forall x : tm, P x.
We can also show, trivially, that tm_induction_weak is derivable
from tm_induction.
|
Theorem tm_induction_weak_derived :
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.
| Support |
Theorem supports_tm : forall t : tm, supports tmP (fvar t) t.
Hint Resolve supports_tm : stlc.
| Define substitution |
Section Substitution.
Variable y : tmvar.
Variable s : tm.
Definition subst : tm -> tm :=
tm_rec tm
dot
(fun x => if atom_eqdec tmvar x y then s else (var x))
(fun s s' t t' => app s' t')
(fun x T t t' => lam x T t')
(add y (fvar s)).
Lemma subst_supp_dot :
supports tmP (add y (fvar s)) dot.
Lemma subst_supp_var :
supports (tmvarP ^-> tmP) (add y (fvar s))
(fun x : tmvar => if atom_eqdec tmvar x y then s else var x).
Lemma subst_supp_app :
supports (tmP ^-> tmP ^-> tmP ^-> tmP ^-> tmP)
(add y (fvar s)) (fun _ s' _ t' : tm => app s' t').
Lemma subst_supp_lam :
supports (tmvarP ^-> tyP ^-> tmP ^-> tmP ^-> tmP)
(add y (fvar s))
(fun (x : tmvar) (T : ty) (_ t' : tm) => lam x T t').
Hint Resolve subst_supp_dot subst_supp_var subst_supp_app subst_supp_lam : stlc.
Theorem subst_dot : subst dot = dot.
Theorem subst_var_eq : subst (var y) = s.
Theorem subst_var_neq : forall x, x <> y -> subst (var x) = (var x).
Theorem subst_app :
forall q r, subst (app q r) = app (subst q) (subst r).
Theorem subst_lam :
forall x T t, x <> y -> ~ In x (fvar s) ->
subst (lam x T t) = lam x T (subst t).
Theorem supports_subst :
supports (tmP ^-> tmP) (add y (fvar s)) subst.
End Substitution.
Hint Resolve subst_dot subst_var_eq subst_var_neq subst_app subst_lam : stlc.
Hint Rewrite subst_dot subst_var_eq subst_app : stlc.
Hint Rewrite subst_var_neq using congruence : stlc.
Hint Rewrite subst_lam using (auto with stlc nominal; fail) : stlc.
Simple substitution lemmas |
Notation "'existsType' x : t , p" :=
(sigT (fun x : t => p))
(at level 200, x ident, format "'existsType' '/ ' x : t , '/ ' p") :
type_scope.
Lemma tm_induction' :
forall (P : tm -> Type),
(P dot) ->
(forall (a : tmvar), P (var a)) ->
(forall s : tm, P s-> forall t : tm, P t -> P (app s t)) ->
(existsType E : aset tmvar,
forall (a : tmvar), ~ In a E -> forall (T : ty) (s : tm),
P s -> P (lam a T s)) ->
forall x : tm, P x.
Notation "M ^[ x := N ]" := (subst x N M) (at level 59, left associativity).
Lemma subst_var_same' :
forall (x : tmvar) (e : tm) (y : tmvar),
y = x -> (var y) ^[x := e] = e.
Proof.
intros x e y H; rewrite H; apply subst_var_eq.
Qed.
Hint Rewrite subst_var_same' using congruence : stlc.
Ltac subst_var_simpl H x y :=
match goal with
| |- context [subst x ?e (var y)] =>
(progress (repeat
(rewrite (subst_var_same' x e y); [idtac | congruence]))) ||
(progress (repeat
(rewrite (subst_var_neq x e y); [idtac | congruence]))) ||
(case (atom_eqdec _ x y); intro H;
[repeat (rewrite (subst_var_same' x e y)); [idtac | congruence] |
repeat (rewrite (subst_var_neq x e y)); [idtac | congruence]])
end.
Ltac stlc_simpl :=
repeat (
progress (
unfold tmvarP ||
rewrite perm_atom ||
autorewrite with stlc nominal ||
swapa_simpl)).
Lemma fvar_swap :
forall x y z t,
z <> x -> z <> y ->
~ In z (fvar t) ->
~ In z (fvar (perm tmP [(x, y)] t)).
Hint Resolve fvar_swap : stlc.
Lemma subst_equivariant :
forall z v x y t,
perm tmP [(x, y)] (t ^[z := v]) =
(perm tmP [(x, y)] t) ^[(perm tmvarP [(x, y)] z) := (perm tmP [(x, y)] v)].
Proof.
intros z v x y t.
pattern t; apply tm_induction'.
stlc_simpl; trivial.
intros a.
subst_var_simpl za z a; stlc_simpl; trivial.
swapa_case xa ya x y a;
swapa_case xz yz x y z; stlc_simpl; trivial.
intros u1 IHu1 u2 IHu2.
rewrite subst_app.
rewrite perm_app.
rewrite IHu1.
rewrite IHu2.
stlc_simpl; trivial.
exists (add x (add y (add z (fvar v)))).
intros a Ha T s IHs.
destruct_neg_add Ha ax Ha1.
destruct_neg_add Ha1 ay Ha2.
destruct_neg_add Ha2 az av.
stlc_simpl.
rewrite IHs.
unfold tmvarP;
swapa_case xz yz x y z;
stlc_simpl; trivial.
Qed.
Hint Rewrite subst_equivariant : stlc.
Lemma fvar_subst :
forall (x : tmvar) (M N : tm),
Subset (fvar (M ^[x := N])) (union (remove x (fvar M)) (fvar N)).
Proof.
intros x M N.
pattern M; apply tm_induction'.
autorewrite with stlc; auto with sets.
intros y.
subst_var_simpl xy x y.
auto with sets.
autorewrite with stlc.
unfold Subset; intros z H.
destruct_singleton H; rewrite H; auto with sets.
intros s IHs t IHt.
autorewrite with stlc.
autorewrite with sets.
rewrite union_union_distrib.
auto with sets.
exists (add x (fvar N)).
intros y y_fresh T s IHs.
destruct_neg_add y_fresh yx y_fresh'.
autorewrite with stlc.
unfold Subset; intros z H.
destruct_remove H J K.
assert (L:= IHs z K).
destruct_union L.
destruct_remove L L1 L2; auto with sets.
auto with sets.
Qed.
Lemma subst_not_fv :
forall (x : tmvar) (N M: tm),
~ In x (fvar M) ->
M ^[x := N] = M.
Proof.
intros x N M.
pattern M; apply tm_induction'.
autorewrite with stlc; trivial.
intros a H.
rewrite fvar_var in H.
destruct_neg_singleton H.
autorewrite with stlc; trivial.
intros s IHs t IHt H.
rewrite fvar_app in H.
destruct_neg_union H Hs Ht.
autorewrite with stlc.
rewrite IHs; trivial.
rewrite IHt; trivial.
exists (add x (fvar N)).
intros y y_fresh T s IHs H.
destruct_neg_add y_fresh yx yN.
autorewrite with stlc.
rewrite IHs; trivial.
rewrite fvar_lam in H.
destruct_neg_remove H; [congruence | trivial].
Qed.
Hint Rewrite subst_not_fv using solve [auto with stlc] : stlc.
Ltac fresh_atom name set hyp_name :=
let H := fresh in (
assert (H:= atom_infinite _ set);
elim H; clear H;
intros name hyp_name
).
Lemma subst_commute :
forall (x y : tmvar) (M N L : tm),
x <> y ->
~ In x (fvar L) ->
M ^[x := N] ^[y := L] = M ^[y := L] ^[x := N ^[y := L]].
Proof.
intros x y M N L xy xL.
pattern M; apply tm_induction'.
autorewrite with stlc; trivial.
intro z.
subst_var_simpl xz x z;
subst_var_simpl yz y z;
autorewrite with stlc; trivial.
intros s IHs t IHt.
autorewrite with stlc.
rewrite IHs; trivial.
rewrite IHt; trivial.
exists (union (add x (fvar N)) (add y (fvar L))).
intros z z_fresh T s IHs.
destruct_neg_union z_fresh z_fresh1 z_fresh2.
destruct_neg_add z_fresh1 zx zN.
destruct_neg_add z_fresh2 zy zL.
autorewrite with stlc.
rewrite IHs; trivial.
rewrite subst_lam; trivial.
intro J.
assert (J':= fvar_subst _ _ _ _ J).
destruct_union J'.
destruct_remove J' J1 J2; contradiction.
contradiction.
Qed.
Lemma subst_fresh_var :
forall (x y : tmvar) (M : tm),
~ In y (fvar M) ->
M ^[x := var y] = perm tmP [(x, y)] M.
Proof.
intros x y M.
pattern M; apply tm_induction'.
autorewrite with stlc; trivial.
intros z y_fresh.
rewrite fvar_var in y_fresh.
destruct_neg_singleton y_fresh.
subst_var_simpl xz x z; stlc_simpl; trivial.
intros s IHs t IHt y_fresh.
rewrite fvar_app in y_fresh.
destruct_neg_union y_fresh ys yt.
autorewrite with stlc.
rewrite IHs; trivial; rewrite IHt; trivial.
exists (add x (fvar (var y))).
intros z z_fresh T s IHs y_fresh.
destruct_neg_add z_fresh zx z_var_y.
rewrite fvar_lam in y_fresh.
destruct_neg_remove y_fresh.
absurd (z <> x); trivial.
rewrite fvar_var in z_var_y.
destruct_neg_singleton z_var_y.
congruence.
autorewrite with stlc.
rewrite IHs; trivial.
rewrite fvar_var in z_var_y.
destruct_neg_singleton z_var_y.
stlc_simpl; trivial.
Qed.
Lemma subst_equal :
forall (x y : tmvar) (M N : tm),
~ In y (fvar M) ->
M ^[x := N] = (perm tmP [(y, x)] M) ^[y := N].
Proof.
intros x y M N.
pattern M; apply tm_induction'.
autorewrite with stlc; trivial.
intros z y_fresh.
rewrite fvar_var in y_fresh.
destruct_neg_singleton y_fresh.
subst_var_simpl xz x z; stlc_simpl; trivial.
intros s IHs t IHt y_fresh.
rewrite fvar_app in y_fresh.
destruct_neg_union y_fresh ys yt.
autorewrite with stlc.
rewrite IHs; trivial; rewrite IHt; trivial.
exists (add x (add y (fvar N))).
intros z z_fresh T s IHs y_fresh.
destruct_neg_add z_fresh zx z_fresh'.
destruct_neg_add z_fresh' zy zN.
rewrite fvar_lam in y_fresh.
destruct_neg_remove y_fresh.
congruence.
stlc_simpl.
rewrite IHs; trivial.
Qed.
| CBV Reduction |
Inductive value : tm -> Prop :=
| unit_value :
value dot
| abs_value :
forall (x : tmvar) (T : ty) (t : tm),
value (lam x T t).
Inductive cbv : tm -> tm -> Prop :=
| cbv_left :
forall (t t' u : tm),
cbv t t' ->
cbv (app t u) (app t' u)
| cbv_right :
forall (t u u' : tm),
value t ->
cbv u u' ->
cbv (app t u) (app t u')
| cbv_beta :
forall (x : tmvar) (T : ty) (t u : tm),
value u ->
cbv (app (lam x T t) u) (t ^[x := u]).
Lemma values_are_normal_forms :
forall (t t' : tm), value t -> ~ cbv t t'.
Lemma cbv_deterministic :
forall (t t' t'' : tm),
cbv t t' -> cbv t t'' -> t' = t''.
Lemma value_equivariant :
forall x y t,
value t -> value (perm tmP [(x, y)] t).
Lemma cbv_equivariant :
forall x y t t',
cbv t t' -> cbv (perm tmP [(x, y)] t) (perm tmP [(x, y)] t').
| Size function |
Inductive size : tm -> nat -> Prop :=
| size_unit : size dot 1
| size_var : forall x, size (var x) 1
| size_app :
forall t u m n,
size t m -> size u n -> size (app t u) (m + n + 1)
| size_lam :
forall x T t m,
size t m -> size (lam x T t) (m + 1).
Lemma size_total :
forall t, {n : nat | size t n}.
Lemma size2 : forall x T, proj1_sig (size_total (lam x T (var x))) = 2.
| Compiling to SK-combinators |
Inductive SKtm : Set :=
| SKvar : tmvar -> SKtm
| S : SKtm
| K : SKtm
| SKapp : SKtm -> SKtm -> SKtm.
Fixpoint SKperm (p : permt tmvar) (s : SKtm) {struct s} : SKtm :=
match s with
| SKvar z => SKvar (perm tmvarP p z)
| S => S
| K => K
| SKapp q r => SKapp (SKperm p q) (SKperm p r)
end.
Definition SKP : PsetT tmvar SKtm.
Fixpoint SKfvar (s : SKtm) : aset tmvar :=
match s with
| SKvar x => singleton x
| S => empty
| K => empty
| SKapp q r => union (SKfvar q) (SKfvar r)
end.
Inductive SKabs : tmvar -> SKtm -> SKtm -> Prop :=
| SKabs_I :
forall x,
SKabs x (SKvar x) (SKapp (SKapp S K) K)
| SKabs_K :
forall x s,
~ In x (SKfvar s) ->
SKabs x s (SKapp K s)
| SKabs_S :
forall x r s r' s',
SKabs x r r' ->
SKabs x s s' ->
SKabs x (SKapp r s) (SKapp (SKapp S r') s').
Inductive SKcomp : tm -> SKtm -> Prop :=
| SKcomp_var :
forall x,
SKcomp (var x) (SKvar x)
| SKcomp_app :
forall t u q r,
SKcomp t q ->
SKcomp u r ->
SKcomp (app t u) (SKapp q r)
| SKcomp_lam :
forall x T t s s',
SKcomp t s ->
SKabs x s s' ->
SKcomp (lam x T t) s'.
Lemma SKvar_equivariant :
forall p z,
perm SKP p (SKvar z) = SKvar (perm tmvarP p z).
Hint Rewrite SKvar_equivariant : stlc.
Lemma S_equivariant :
forall p,
perm SKP p S = S.
Hint Rewrite S_equivariant : stlc.
Lemma K_equivariant :
forall p,
perm SKP p K = K.
Hint Rewrite K_equivariant : stlc.
Lemma SKapp_equivariant :
forall p r s,
perm SKP p (SKapp r s) =
SKapp (perm SKP p r) (perm SKP p s).
Hint Rewrite SKapp_equivariant : stlc.
Lemma SKfvar_equivariant :
forall p z s,
In z (SKfvar s) ->
In (perm tmvarP p z) (SKfvar (perm SKP p s)).
Lemma SKabs_equivariant :
forall p z s s',
SKabs z s s' ->
SKabs (perm tmvarP p z) (perm SKP p s) (perm SKP p s').
Lemma SKcomp_equivariant :
forall p t s,
SKcomp t s ->
SKcomp (perm tmP p t) (perm SKP p s).
End UseSTLC.