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

%%%%%%%%%%%%%%%%
% Proof for semantics preservation of code generation
%%%%%%%%%%%%%%%%

Specification "trans".

Import "eval". [View eval]
Import "subst". [View subst]

Define sim : ty -> nat -> tm' -> (tm' -> tm') -> state -> tm' -> prop,
       equiv : ty -> nat -> tm' -> state -> tm' -> prop by
  sim T I M K S M' := 
    forall J V, le J I -> {nstep' J M V} -> {val' V} ->
      exists N V' S' N', {nstep'' N' S M' S' (K V')} /\ 
                         {add J N I} /\ equiv T N V S' V';
  equiv tnat I (nat' N) S (nat' N);
  equiv tunit I unit' S unit';
  equiv (prod T1 T2) I (pair' V1 V2) (st N H) (loc' L) :=
    exists V1' V2', {lookup_heap H L (pair' V1' V2')} /\
      equiv T1 I V1 (st N H) V1' /\ equiv T2 I V2 (st N H) V2' /\
      {tm' V1} /\ {tm' V2} /\ {tm' V1'} /\ {tm' V2'};
  equiv (arr' T1 T2) z (abs' R) S (abs' R') :=
     {tm' (abs' R)} /\ {tm' (abs' R')};
  equiv (arr' T1 T2) (s K) (abs' R) S (abs' R') :=
     equiv (arr' T1 T2) K (abs' R) S (abs' R') /\
     forall V V', equiv T1 K V S V' -> sim T2 K (R V) (x\x) S (R' V');
  equiv (arr T1 T2) z (clos' (abs' R) VE) (st N H) (loc' L) :=
    exists R' VE', {lookup_heap H L (pair' (abs' R') VE')} /\
      {tm' (clos' (abs' R) VE)} /\ {tm' (pair' (abs' R') VE')} /\
      {val' VE} /\ {val' VE'};
  equiv (arr T1 T2) (s K) (clos' (abs' R) VE) (st N H) (loc' L) :=
    equiv (arr T1 T2) K (clos' (abs' R) VE) (st N H) (loc' L) /\
    exists R' VE', {lookup_heap H L (pair' (abs' R') VE')} /\
      forall V1 V1' V2 V2', 
        equiv T1 K V1 (st N H) V1' -> equiv (arr T1 T2) K V2 (st N H) V2' ->
          sim T2 K (R (pair' V2 (pair' V1 VE))) (x\x) (st N H)
                   (R' (pair' V2' (pair' V1' VE'))).


Define cg_ctx : olist -> prop by
  cg_ctx nil;
  nabla x, cg_ctx ((pi k\ cgen x k (k x)) :: L) := cg_ctx L.

Define vars_of_cg_ctx : olist -> list tm' -> prop by
  vars_of_cg_ctx nil nil;
  nabla x, vars_of_cg_ctx ((pi k\ cgen x k (k x)):: L) (x :: L') :=
    vars_of_cg_ctx L L'.

Define subst_equiv : olist -> nat -> list (map tm' tm') -> state -> list (map tm' tm') -> prop by
  subst_equiv nil I nil S nil;
  nabla x, subst_equiv (of' x T :: L) I (map x V :: ML) S (map x V' :: ML') :=
    equiv T I V S V' /\ subst_equiv L I ML S ML'.


% Semantics preservation
% Theorem cg_sem_pres : forall ML ML' L CL Vs M T K K' M' P P' I S,
%   {is_nat I} -> ctx' L -> cg_ctx CL -> 
%   vars_of_ctx' L Vs -> vars_of_cg_ctx CL Vs ->
%   subst' ML -> subst' ML' -> subst_equiv L I ML S ML' ->
%   {L |- of' M T} -> {CL |- cgen M K M'} -> 
%   app_subst ML M P -> app_subst ML' M' P' ->    
%   (nabla x, app_subst ML' (K x) (K' x)) ->
%     sim T I P K' S P'.
% skip.

% Theorem nat_sem_pres : forall P P' V,
%   {of'' P tnat} -> {hcgen P P'} -> {eval'' P V} -> 
%     exists St,{eval''' P' St V}.
% intros. case H2. case H1.

% Define fun_equiv : olist -> nat -> list (map tm' tm') -> state -> list (map tm' tm') -> prop by
%   subst_equiv nil I nil S nil;
%   nabla x, subst_equiv (of' x T :: L) I (map x V :: ML) S (map x V' :: ML') :=
%     equiv T I V S V' /\ subst_equiv L I ML S ML'.


Theorem cg_nat_sem_pres : forall M M' V,
  {of'' M tnat} -> {hcgen M M'} -> {eval'' M V} -> {eval'' M' V}.
intros. case H2. search.