Require Export Nominal.
Module Type STLC.
| Datatypes. |
Parameter tmvar : AtomT.
Definition tmvarP := mkAtomPset tmvar.
Inductive ty : Set :=
| unit : ty
| arrow : ty -> ty -> ty.
Definition tyP : PsetT tmvar ty := mkIdPset tmvar ty.
Parameter tm : Set.
Parameter tmP : PsetT tmvar tm.
Parameter dot : tm.
Parameter var : tmvar -> tm.
Parameter app : tm -> tm -> tm.
Parameter lam : tmvar -> ty -> tm -> tm.
| Constructor distinctness. |
Section Distinctness.
Variables a b : tmvar.
Variables T : ty.
Variables s t q r : tm.
Axiom distinctness_dot_var : dot <> var a.
Axiom distinctness_dot_app : dot <> app s t.
Axiom distinctness_dot_lam : dot <> lam a T s.
Axiom distinctness_var_dot : var a <> dot.
Axiom distinctness_var_app : var a <> app s t.
Axiom distinctness_var_lam : var a <> lam b T s.
Axiom distinctness_app_dot : app s t <> dot.
Axiom distinctness_app_var : app s t <> var a.
Axiom distinctness_app_lam : app s t <> lam a T q.
Axiom distinctness_lam_dot : lam a T s <> dot.
Axiom distinctness_lam_var : lam a T s <> var b.
Axiom distinctness_lam_app : lam a T s <> app q r.
End Distinctness.
Ltac stlc_discriminate :=
match goal with
| [H : (var _ = dot) |- _] =>
pose (distinctness_var_dot _ H); intuition; fail
| [H : (app _ _ = dot) |- _] =>
pose (distinctness_app_dot _ _ H); intuition; fail
| [H : (lam _ _ _ = dot) |- _] =>
pose (distinctness_lam_dot _ _ _ H); intuition; fail
| [H : (dot = var _) |- _] =>
pose (distinctness_dot_var _ H); intuition; fail
| [H : (app _ _ = var _) |- _] =>
pose (distinctness_app_var _ _ _ H); intuition; fail
| [H : (lam _ _ _ = var _) |- _] =>
pose (distinctness_lam_var _ _ _ _ H); intuition; fail
| [H : (dot = app _ _) |- _] =>
pose (distinctness_dot_app _ _ H); intuition fail
| [H : (var _ = app _ _) |- _] =>
pose (distinctness_var_app _ _ _ H); intuition; fail
| [H : (lam _ _ _ = app _ _) |- _] =>
pose (distinctness_lam_app _ _ _ _ _ H); intuition; fail
| [H : (dot = lam _ _ _) |- _] =>
pose (distinctness_dot_lam _ _ _ H); intuition; fail
| [H : (var _ = lam _ _ _) |- _] =>
pose (distinctness_var_lam _ _ _ _ H); intuition; fail
| [H : (app _ _ = lam _ _ _) |- _] =>
pose (distinctness_app_lam _ _ _ _ _ H); intuition; fail
end.
| Permutation on terms. |
Section STLCPermutations.
Variable p : permt tmvar.
Variable c : tmvar.
Variable T : ty.
Variables s t : tm.
Axiom perm_dot : perm tmP p dot = dot.
Axiom perm_var : perm tmP p (var c) = var (perm tmvarP p c).
Axiom perm_app :
perm tmP p (app s t) = app (perm tmP p s) (perm tmP p t).
Axiom perm_lam :
perm tmP p (lam c T s) = lam (perm tmvarP p c) T (perm tmP p s).
End STLCPermutations.
| Free variables. |
Section FreeVariables.
Variables a : tmvar.
Variables T : ty.
Variables s t : tm.
Parameter fvar : tm -> aset tmvar.
Axiom fvar_dot : fvar dot = empty.
Axiom fvar_var : fvar (var a) = singleton a.
Axiom fvar_app : fvar (app s t) = union (fvar s) (fvar t).
Axiom fvar_lam : fvar (lam a T s) = remove a (fvar s).
End FreeVariables.
| Alpha-Equality. |
Axiom eq_lam :
forall (a b : tmvar) (T : ty) (t : tm),
~ In b (fvar t) ->
lam a T t = lam b T (perm tmP [(a, b)] t).
| Injectivity for constructors. |
Section Injectivity.
Variables a a' : tmvar.
Variables T T' : ty.
Variables s s' t t' : tm.
Axiom injection_var : var a = var a' -> a = a'.
Axiom injection_app_fun : app s t = app s' t' -> s = s'.
Axiom injection_app_arg : app s t = app s' t' -> t = t'.
Axiom injection_lam_ty : lam a T s = lam a' T' s' -> T = T'.
Axiom injection_lam_body :
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 Injectivity.
Ltac stlc_injection :=
match goal with
| [H : (var _ = var _) |- _] =>
pose (injection_var _ _ H)
| [H : (app _ _ = app _ _) |- _] =>
pose (injection_app_fun _ _ _ _ H);
pose (injection_app_arg _ _ _ _ H)
| [H : (lam _ _ _ = lam _ _ _) |- _] =>
pose (injection_lam_ty _ _ _ _ _ _ H);
pose (injection_lam_body _ _ _ _ _ _ H)
end.
| Structural induction. |
Axiom 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.
| Primitive recursion. |
Parameter tm_rec
: forall R : Set,
R ->
(tmvar -> R) ->
(tm -> R -> tm -> R -> R) ->
(tmvar -> ty -> tm -> R -> R) -> aset tmvar -> tm -> R.
Axiom tm_rec_dot
: forall (R : Set) (f_dot : R) (f_var : tmvar -> R)
(f_app : tm -> R -> tm -> R -> R)
(f_lam : tmvar -> ty -> tm -> R -> R) (F : aset tmvar),
tm_rec R f_dot f_var f_app f_lam F dot = f_dot.
Axiom tm_rec_var
: forall (R : Set) (f_dot : R) (f_var : tmvar -> R)
(f_app : tm -> R -> tm -> R -> R)
(f_lam : tmvar -> ty -> tm -> R -> R) (F : aset tmvar) (a : tmvar),
tm_rec R f_dot f_var f_app f_lam F (var a) = f_var a.
Axiom tm_rec_app
: forall (R : Set) (f_dot : R) (f_var : tmvar -> R)
(f_app : tm -> R -> tm -> R -> R)
(f_lam : tmvar -> ty -> tm -> R -> R) (F : aset tmvar) (s t : tm),
tm_rec R f_dot f_var f_app f_lam F (app s t) =
f_app s (tm_rec R f_dot f_var f_app f_lam F s) t
(tm_rec R f_dot f_var f_app f_lam F t).
Axiom tm_rec_lam
: forall (R : Set) (RP : PsetT tmvar R) (f_dot : R) (f_var : tmvar -> R)
(f_app : tm -> R -> tm -> R -> R)
(f_lam : tmvar -> ty -> tm -> R -> R) (F : aset tmvar),
supports RP F f_dot ->
supports (tmvarP ^-> RP) F f_var ->
supports (tmP ^-> RP ^-> tmP ^-> RP ^-> RP) F f_app ->
supports (tmvarP ^-> tyP ^-> tmP ^-> RP ^-> RP) F f_lam ->
(exists b : tmvar,
~ In (e:=asetR tmvar) b F /\
(forall (x : ty) (y : tm) (z : R), freshP RP b (f_lam b x y z))) ->
forall (a : tmvar) (T : ty) (s : tm),
~ In (e:=asetR tmvar) a F ->
tm_rec R f_dot f_var f_app f_lam F (lam a T s) =
f_lam a T s (tm_rec R f_dot f_var f_app f_lam F s).
Axiom tm_rec_supp
: forall (R : Set) (RP : PsetT tmvar R) (f_dot : R) (f_var : tmvar -> R)
(f_app : tm -> R -> tm -> R -> R)
(f_lam : tmvar -> ty -> tm -> R -> R) (F : aset tmvar),
supports RP F f_dot ->
supports (tmvarP ^-> RP) F f_var ->
supports (tmP ^-> RP ^-> tmP ^-> RP ^-> RP) F f_app ->
supports (tmvarP ^-> tyP ^-> tmP ^-> RP ^-> RP) F f_lam ->
(exists b : tmvar,
~ In (e:=asetR tmvar) b F /\
(forall (x : ty) (y : tm) (z : R), freshP RP b (f_lam b x y z))) ->
supports (tmP ^-> RP) F (tm_rec R f_dot f_var f_app f_lam F).
| Automation hints. |
Hint Resolve distinctness_dot_var : stlc.
Hint Resolve distinctness_dot_app : stlc.
Hint Resolve distinctness_dot_lam : stlc.
Hint Resolve distinctness_var_dot : stlc.
Hint Resolve distinctness_var_app : stlc.
Hint Resolve distinctness_var_lam : stlc.
Hint Resolve distinctness_app_dot : stlc.
Hint Resolve distinctness_app_var : stlc.
Hint Resolve distinctness_app_lam : stlc.
Hint Resolve distinctness_lam_dot : stlc.
Hint Resolve distinctness_lam_var : stlc.
Hint Resolve distinctness_lam_app : stlc.
Hint Resolve perm_dot : stlc.
Hint Resolve perm_var : stlc.
Hint Resolve perm_app : stlc.
Hint Resolve perm_lam : stlc.
Hint Rewrite perm_dot : stlc.
Hint Rewrite perm_var : stlc.
Hint Rewrite perm_app : stlc.
Hint Rewrite perm_lam : stlc.
Hint Resolve fvar_dot : stlc.
Hint Resolve fvar_var : stlc.
Hint Resolve fvar_app : stlc.
Hint Resolve fvar_lam : stlc.
Hint Rewrite fvar_dot : stlc.
Hint Rewrite fvar_var : stlc.
Hint Rewrite fvar_app : stlc.
Hint Rewrite fvar_lam : stlc.
Hint Immediate injection_var : stlc.
Hint Immediate injection_app_fun : stlc.
Hint Immediate injection_app_arg : stlc.
Hint Immediate injection_lam_ty : stlc.
Hint Immediate injection_lam_body : stlc.
Hint Resolve tm_rec_dot tm_rec_var tm_rec_app : stlc.
Hint Rewrite tm_rec_dot tm_rec_var tm_rec_app : stlc.
Hint Immediate tm_rec_lam : stlc.
Hint Rewrite tm_rec_lam using (auto with stlc nominal; fail) : stlc.
End STLC.