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
This page has been generated by coqdoc