Library Cpsopt_proof

Preservation semantics of the CPS conversion

Author : Zaynah Dargaye

Created : 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import Fml.

Require Import Fml_subst.

Require Import CPS.

Require Import CPS_subst.

Require Import CPS_pre.

Require Import f2cps.

Require Import f2cps_help.

Require Import f2cps_proof.

Require Import f2cps_pre.

Require Import Cpsopt.

Require Import Cpsopt_pre1.

Require Import Cpsopt_pre.

I. beta v equivalence between the naive CPs conversion and the CPS conversion of the same term


Lemma cbv_ctrad_cps3: 

 forall t, (forall k1 k2,

     is_catom k1=true  ->

    cbveq k1 k2-> 

    cbveq (unApp (ctrad t) k1) (cps3 t k2))/\ 

  cbveq (ctrad_atom t) (cps3_atom t).

II. Semantics preservation of the CPS conversion of a term


Lemma cps3_correct2: 

 forall t v, eval_term t v -> 

  forall k r t1, 

  ceval_term k (TLamb 0 t1) ->  Cclosed (TLamb 0 t1) ->  

  ceval_term (CTsubst_rec (ctrad_atom v::nil) nil t1 O O) r -> 

  is_catom k=true ->

  exists v2, ceval_term (cps3 t k) v2 /\ cbveq r v2.

III. Semantics preservation of the CPS conversion of a program


Theorem  cps_comp_correct2: 

 forall t v, 

 eval_term t v -> 

 exists w, ceval_term (cps_comp t) w /\ cbveq (ctrad_atom v) w.