# Library UseSTLC

``` 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. ```
Index