Executable Specification

[View trans]

Reasoning

[View typing]

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

Specification "trans".

Import "util". [View util]

Close nat, ty, tm, tm', map, tm_list, tm'_list, map_list.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Source typing context with unique type assignments %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typing context
Define sctx : olist -> prop by
  sctx nil;
  nabla x, sctx (of x T :: L) := sctx L /\ {is_sty T}.

Define vars_of_sctx : olist -> tm_list -> prop by
  vars_of_sctx nil snil;
  nabla x, vars_of_sctx (of x T :: L) (scons x L') :=
    vars_of_sctx L L'.

% Lemmas of Typing
Theorem sctx_mem : forall SL O,
  sctx SL -> member O SL -> exists X T, O = of X T /\ name X /\ {is_sty T}.

Theorem sctx_var_mem : forall L T M,
  sctx L -> {L |- of M T} -> name M -> member (of M T) L.

Theorem sof_nat_inv : forall L N T,
  sctx L -> {L |- of (nat N) T} -> T = tnat.

Theorem sof_pair_inv : forall L M1 M2 T,
  sctx L -> {L |- of (pair M1 M2) T} -> exists T1 T2, T = prod T1 T2.

Theorem sof_unit_inv : forall L T,
  sctx L -> {L |- of unit T} -> T = tunit.

Theorem sctx_focus_inv : forall L D G,
  sctx L -> member D L -> {L, [D] |- G} -> exists A T, G = of A T /\ name A.

Theorem s_is_sty_str : forall L T,
  sctx L -> {L |- is_sty T} -> {is_sty T}.

Theorem sof_is_sty : forall L M T,
  sctx L -> {L |- of M T} -> {is_sty T}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Properties about well-formed terms in the source lanugage (with duplications) %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Term context
Define tm_sctx : olist -> prop by
  tm_sctx nil;
  nabla x, tm_sctx (tm x :: L) := tm_sctx L.

Define vars_of_tm_sctx : olist -> tm_list -> prop by
  vars_of_tm_sctx nil snil;
  nabla x, vars_of_tm_sctx (tm x :: L) (scons x L') :=
    vars_of_tm_sctx L L'.

Theorem tm_sctx_mem : forall E L,
  tm_sctx L -> member E L -> exists X, E = tm X /\ name X.

Theorem sctx_to_tm_sctx : forall L Vs,
  sctx L -> vars_of_sctx L Vs -> 
    exists SL, tm_sctx SL /\ vars_of_tm_sctx SL Vs.

Theorem sctx_tm_sctx_sync : forall L Vs SL M T,
  vars_of_sctx L Vs -> vars_of_tm_sctx SL Vs -> member (of M T) L -> 
    member (tm M) SL.

Theorem sclosed_tm_prune_aux : forall M L, nabla (x:tm),
  tm_sctx L -> {L |- tm (M x)} -> exists M', M = y\ M'.

Theorem sclosed_tm_prune : forall M, nabla (x:tm),
  {tm (M x)} -> exists M', M = y\ M'.

Theorem sof_to_tm : forall L Vs SL M T,
  {is_sty T} -> sctx L -> vars_of_sctx L Vs -> tm_sctx SL -> vars_of_tm_sctx SL Vs ->
    {L |- of M T} -> {SL |- tm M}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Source typing context with possibly duplicated type assignments %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typing contexts
Define ctx : olist -> prop by
  ctx nil;
  ctx (of X T :: L) := ctx L /\ name X /\ {is_sty T} /\
         forall T', (member (of X T') L -> T = T').

% Accumulate the variables in the source context
Define vars_of_ctx : olist -> tm_list -> prop by
  vars_of_ctx nil snil;
  vars_of_ctx (of X T :: L) (scons X Vs) := vars_of_ctx L Vs.

Theorem ctx_islist : forall L,
  ctx L -> is_list L.

Theorem ctx_mem : forall SL O,
  ctx SL -> member O SL -> exists X T, O = of X T /\ name X /\ {is_sty T}.

Theorem ctx_mem_sync : forall L X T T',
  ctx L -> member (of X T) L -> member (of X T') L -> T = T'.

Theorem ctx_extend : forall L T, nabla x, 
  ctx L -> {is_sty T} -> ctx (of x T :: L).

Theorem is_sty_str : forall L T,
  ctx L -> {L |- is_sty T} -> {is_sty T}.

Theorem of_is_sty : forall L M T,
  ctx L -> {L |- of M T} -> {is_sty T}.

Theorem sty_to_cty : forall T,
  {is_sty T} -> {is_cty T}.

Theorem ctx_name : forall L Vs X,
  ctx L -> vars_of_ctx L Vs -> {smember X Vs} -> name X.

Theorem ctx_subset : forall L L',
  ctx L -> subset L' L -> ctx L'.
  
% Lemmas of typing
Theorem of_nat_inv : forall L N T,
  ctx L -> {L |- of (nat N) T} -> T = tnat.

Theorem of_var_inv : forall M L T,
  ctx L -> {L |- of M T} -> name M -> member (of M T) L.

Theorem of_weakening : forall L L' M T,
  ctx L -> subset L L' -> {L |- of M T} -> {L' |- of M T}.

Theorem ctx_focus_inv : forall L D G,
  ctx L -> member D L -> {L, [D] |- G} -> exists A T, G = of A T /\ name A.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Properties about well-formed terms in the source lanugage (with duplications) %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Well-formed term contexts
Define tm_ctx : olist -> prop by
  tm_ctx nil;
  tm_ctx (tm X :: L) := tm_ctx L /\ name X.

Define vars_of_tm_ctx : olist -> tm_list -> prop by
  vars_of_tm_ctx nil snil;
  vars_of_tm_ctx (tm X :: L) (scons X L') :=
    vars_of_tm_ctx L L'.

Theorem tm_ctx_mem : forall E L,
  tm_ctx L -> member E L -> exists X, E = tm X /\ name X.

Theorem ctx_mem_to_lst_mem : forall L Vs X T,
  vars_of_ctx L Vs -> member (of X T) L -> {smember X Vs}.

Theorem lst_mem_to_ctx_mem : forall L Vs X,
  vars_of_ctx L Vs -> {smember X Vs} -> 
    exists T, member (of X T) L.

Theorem ctx_to_tm_ctx : forall L Vs,
  ctx L -> vars_of_ctx L Vs -> 
    exists SL, tm_ctx SL /\ vars_of_tm_ctx SL Vs.

Theorem ctx_tm_ctx_sync : forall L Vs SL M T,
  vars_of_ctx L Vs -> vars_of_tm_ctx SL Vs -> member (of M T) L -> 
    member (tm M) SL.

Theorem tm_cut : forall L M V, nabla x,
  {tm V} -> tm_ctx (L x) -> {L x, tm x |- tm (M x)} ->  {L x |- tm (M V)}.

% closed terms do not contain nominal constants
Theorem closed_tm_prune_aux : forall M L, nabla (x:tm),
  tm_ctx L -> {L |- tm (M x)} -> exists M', M = y\ M'.

Theorem closed_tm_prune : forall M, nabla (x:tm),
  {tm (M x)} -> exists M', M = y\ M'.

Theorem of_to_tm : forall L Vs SL M T,
  ctx L -> vars_of_ctx L Vs -> tm_ctx SL -> vars_of_tm_ctx SL Vs ->
    {L |- of M T} -> {SL |- tm M}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Target typing context with unique type assignments %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typing contexts
Define ctx' : olist -> prop by
  ctx' nil;
  nabla x, ctx' (of' x T :: L) := ctx' L /\ {is_cty T}.

Define vars_of_ctx' : olist -> tm'_list -> prop by
  vars_of_ctx' nil cnil;
  vars_of_ctx' (of' X T :: L) (ccons X Vs) := vars_of_ctx' L Vs.

Theorem ctx'_islist : forall L,
  ctx' L -> is_list L.

Theorem ctx'_mem : forall E L,
  ctx' L -> member E L -> exists M T, E = of' M T /\ name' M /\ {is_cty T}.

Theorem ctx'_var_mem : forall L T M,
  ctx' L -> {L |- of' M T} -> name' M -> member (of' M T) L.

Theorem ctx'_mem_sync : forall L X T T',
  ctx' L -> member (of' X T) L -> member (of' X T') L -> T = T'.

Theorem vars_of_ctx'_prune2 : forall L Vs, nabla (x:tm'),
  vars_of_ctx' L (Vs x) -> exists Vs', Vs = y\Vs'.

% Lemmas of typing
Theorem of'_nat_inv : forall L N T,
  ctx' L -> {L |- of' (nat' N) T} -> T = tnat.

Theorem is_cty_str : forall L T,
  ctx' L -> {L |- is_cty T} -> {is_cty T}.

Theorem of'_is_cty : forall L M T,
  ctx' L -> {L |- of' M T} -> {is_cty T}.

Theorem of'_str: forall L M T1 T, nabla x,
  ctx' L -> {is_cty T1} -> {L, of' x T1 |- of' M T} -> {L |- of' M T}.

Theorem of''_env_str: forall L FE T TE, nabla x,
  ctx' L -> {is_cty T} -> {L, of' x T |- of''_env FE TE} -> 
    {L |- of''_env FE TE}.

Theorem ctx'_focus_inv : forall L D G,
  ctx' L -> member D L -> {L, [D] |- G} -> exists A T, G = of' A T /\ name' A.

Theorem of''_env_is_cty : forall L FE TE,
  ctx' L -> {L |- of''_env FE TE} -> {is_cty TE}.

Theorem of''_env_tm'_list : forall L FE1 TE,
  ctx' L -> {L |- of''_env FE1 TE} -> is_tm'_list FE1.

Theorem of''_body_is_cty : forall L TE M T,
  ctx' L -> {is_cty TE} -> {L |- of''_body TE M T} -> {is_cty T}.

Theorem of''_is_cty: forall L M T,
  ctx' L -> {L |- of'' M T} -> {is_cty T}.

Theorem of''_to_alter_ver : forall L FE M T,
  ctx' L -> {L |- of'' (htm FE M) T} -> exists TE,
    {L |- of''_env FE TE} /\ {L |- of''_body TE M T}.
 
Theorem of''_from_alter_ver : forall L FE TE M T,
  ctx' L -> {L |- of''_env FE TE} -> {L |- of''_body TE M T} ->
  {L |- of'' (htm FE M) T}.
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Properties about well-formed terms in the target lanugage %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Define tm'_ctx : olist -> prop by
  tm'_ctx nil;
  nabla x, tm'_ctx (tm' x :: L) := tm'_ctx L.

Define vars_of_tm'_ctx : olist -> tm'_list -> prop by
  vars_of_tm'_ctx nil cnil;
  nabla x, vars_of_tm'_ctx (tm' x :: L) (ccons x L') :=
    vars_of_tm'_ctx L L'.

Theorem vars_of_tm'_ctx_prune1 : forall L Vs, nabla (x:tm'),
  vars_of_tm'_ctx (L x) Vs -> exists L', L = y\L'.

Theorem tm'_ctx_mem : forall E L,
  tm'_ctx L -> member E L -> exists X, E = tm' X /\ name' X.

Theorem ctx'_to_tm'_ctx : forall L Vs,
  ctx' L -> vars_of_ctx' L Vs -> 
    exists SL, tm'_ctx SL /\ vars_of_tm'_ctx SL Vs.

Theorem ctx'_tm'_ctx_sync : forall L Vs SL M T,
  vars_of_ctx' L Vs -> vars_of_tm'_ctx SL Vs -> member (of' M T) L -> 
    member (tm' M) SL.

% closed terms do not contain nominal constants
Theorem closed_tm'_prune_aux : forall M L, nabla (x:tm'),
  tm'_ctx L -> {L |- tm' (M x)} -> exists M', M = y\ M'.

Theorem closed_tm'_prune : forall M, nabla (x:tm'),
  {tm' (M x)} -> exists M', M = y\ M'.

Theorem of'_to_tm' : forall L Vs CL M T,
  ctx' L -> vars_of_ctx' L Vs -> tm'_ctx CL -> vars_of_tm'_ctx CL Vs ->
    {L |- of' M T} -> {CL |- tm' M}.

Theorem of''_body_to_tm'' : forall L Vs CL M T TE,
  ctx' L -> vars_of_ctx' L Vs -> tm'_ctx CL -> vars_of_tm'_ctx CL Vs ->
    {L |- of''_body TE M T} -> {CL |- tm''_body M}.

Theorem of''_to_tm'' : forall L Vs CL M T FE,
  ctx' L -> vars_of_ctx' L Vs -> tm'_ctx CL -> vars_of_tm'_ctx CL Vs ->
    {L |- of'' (htm FE M) T} -> {CL |- tm'' (htm FE M)}.


% Closedness lemmas for hoisted terms
Theorem closed_tm''_prune_aux : forall M L, nabla (x:tm'),
  tm'_ctx L -> {L |- tm'' (M x)} -> exists M', M = y\ M'.

Theorem closed_tm''_prune : forall M, nabla (x:tm'),
  {tm'' (M x)} -> exists M', M = y\ M'.

Theorem closed_tm''_body_prune_aux : forall M L, nabla (x:tm'),
  tm'_ctx L -> {L |- tm''_body (M x)} -> exists M', M = y\ M'.

Theorem closed_tm''_body_prune : forall M, nabla (x:tm'),
  {tm''_body (M x)} -> exists M', M = y\ M'.