Library UseSTLC
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.
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.
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.
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)].
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)).
Lemma subst_not_fv :
forall (x : tmvar) (N M: tm),
~ In x (fvar M) ->
M ^[x := N] = M.
Hint Rewrite subst_not_fv using solve [auto with stlc] : stlc.
This is a useful tactic (I think), but not needed in anywhere here.
Ltac fresh_atom name set hyp_name :=
let H := fresh in (
assert (H := atom_infinite _ set);
elim H; clear H;
intros name hyp_name
).
This lemma isn't used later. It's just here as an example.
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]].
This lemma isn't used later. It's just here as an example.
Lemma subst_fresh_var :
forall (x y : tmvar) (M : tm),
~ In y (fvar M) ->
M ^[x := var y] = perm tmP [(x, y)] M.
This is the critical lemma for detminacy of the evaluation relation.
Lemma subst_equal :
forall (x y : tmvar) (M N : tm),
~ In y (fvar M) ->
M ^[x := N] = (perm tmP [(y, x)] M) ^[y := N].
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').
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}.
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.
Defined.
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.