Source: http://chargueraud.org/viewcoq.php?sFile=softs%2Fln%2Fsrc%2FCPS_Correctness.v
Timestamp: 2019-04-23 00:39:40+00:00

Document:
Require Import CPS_Definitions CPS_Infrastructure Omega.
Implicit Types x y z : var.
eval t v -> value v.
eval v v' -> value v -> v' = v.
introv E V. inverts V; inverts~ E.
eval (trm_app (trm_abs t1) v2) r.
eval (trm_app (trm_app (trm_abs t1) v2) v3) r.
introv T1 V2 V3 E. inverts E. inverts H.
cps v = trm_abs (trm_app (trm_bvar 0) (cpsval v)).
introv V. inverts V; simplfix~ cps.
introv V. inverts V; simple~.
x \notin fv (cps t).
simplfix cps; simpls; notin_simpl; auto.
name_var_gen y. destruct (x == y).
cps ([[x~>y]]t) = [[x~>y]](cps t).
introv T. gen x y. induction T using term_size; introv Fr; simpls.
simplfix cps at 2. simpl. case_var~.
simplfix~ cps. rewrite~ IHT1. rewrite~ IHT2. simplfix~ cps at 3.
simplfix cps at 2. name_var_gen z'.
pick_fresh a from (fv ta).
lets IH1: H0 of_vars (>>> ta a a z ___).
apply~ cps_fv; subst ta; rewrite~ subst_open_var].
fequals. rewrite~ close_var_rename. apply~ cps_fv.
close_var x (cps (t^x)) = close_var y (cps (t^y)).
intros. destruct (x == y). subst~.
cps (subst z v t) = subst z (cpsval v) (cps t).
introv T V. induction T; simplfix cps at 2; simpl.
simplfix cps. rewrite IHT1. rewrite~ IHT2.
pick_fresh a from (fv ([z ~> v]t1) \u fv (cpsval v)).
rewrite~ (@cps_rename_body a); [|apply* body_subst].
rewrite~ subst_open_var. rewrite~ (H0 a).
cps (t1 ^^ v) = (cps_abs_body t1) ^^ cpsval v.
introv V B. unfold cps_abs_body. name_var_gen y.
rewrite~ (@subst_intro y (close_var y (cps (t1^y)))).
eval (trm_app (cps t) k) r.
introv E. gen k r. induction E; introv EV VK.
sets_eq t3': (trm_abs (cps_abs_body t3)).
forwards H: IHE3; clear IHE3. eauto. auto.
inverts H as F1 F2 F3. inverts F1.
rewrite~ (eval_value F2) in F3.
introv E V. unfold trm_id. apply* cps_correct_ind.

References: v.

 v.

 V. 
 V. 
 V. 
 V. 
 v.

 V.