Click on a command or tactic to see a detailed view of its use.

Specification "stlc".

Close tm, ty.

% Mapping of source variables into terms
Kind map       type.
Kind map_list  type.
Type map     tm -> tm -> map.
Type mnil    map_list.
Type mcons   map -> map_list -> map_list.

% Application of the source substitutions
Define subst : map_list -> tm -> tm -> prop by
  subst mnil M M;
  nabla x, subst (mcons (map x V) ML) (R x) M :=
    subst ML (R V) M.

Theorem subst_app_comm : forall ML M1 M2 M',
  subst ML (app M1 M2) M' -> exists M1' M2', M' = app M1' M2' /\
    subst ML M1 M1' /\ subst ML M2 M2'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem subst_abs_comm : forall ML R T M',
  subst ML (abs T R) M' -> 
    exists R', M' = abs T R' /\ nabla x, subst ML (R x) (R' x).
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Define name : tm -> prop by
  nabla x, name x.

Theorem mem_tm_prune : forall M L, nabla (x:tm),
  member (M x) L -> exists M', M = y\M'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Define tm_ctx  : olist -> prop by
  tm_ctx nil;
  nabla x, tm_ctx (tm x :: L) := tm_ctx L.

Theorem tm_ctx_mem : forall L E,
  tm_ctx L -> member E L -> exists X, E = tm X /\ name X.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to _ H3. search.
Theorem closed_tm_prune : forall L M, nabla (x:tm),
  tm_ctx L -> {L |- tm (M x)} -> exists M', M = y\M'.
induction on 2. intros. case H2.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. search.
  apply tm_ctx_mem to _ H4. case H3. case H5.
    search.
    apply mem_tm_prune to H4.
  
Theorem subst_closed_tm : forall M ML M',
  {tm M} -> subst ML M M' -> M = M'.
induction on 2. intros. case H2.
  search.
  apply closed_tm_prune to _ H1. apply IH to H1 H3. search.
Theorem subst_inst : forall ML M M' V, nabla (x:tm),
  {tm V} -> subst ML (M x) (M' x) -> subst ML (M V) (M' V).
induction on 2. intros. case H2.
  search.
  apply closed_tm_prune to _ H1. apply IH to _ H3. search.
Theorem explct_meta_subst_assoc : forall ML M M' V, nabla n,
  {tm V} -> subst ML (M n) (M' n) -> subst (mcons (map n V) ML) (M n) (M' V).
intros. unfold. intros. 
  backchain subst_inst with M = M, M' = M', x = n1.