Library f2cps_proof
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_pre.
Require Import f2cps_help.
Ltac DO_IT :=
match goal with
| [ |- context[lt_ge_dec ?a ?b] ] =>
case_eq (lt_ge_dec a b); intros; simpl; auto; DO_IT
| [ |- context[compare_dec ?a ?b] ] =>
case_eq(compare_dec a b); intros; simpl; auto; DO_IT
| [ |- context[match ?x with Some _ => _ | None => _ end] ] =>
case_eq x; intros; simpl; auto; DO_IT
| [ |-context[compare_bd_dec ?a ?b ?c] ] =>
case_eq (compare_bd_dec a b c);intros;simpl;auto;DO_IT
| _ =>
omega || (elimtype False; omega) || (progress f_equal; auto; DO_IT; fail) ||
(progress intuition;DO_IT;fail) ||intuition || auto
end.
Simulation scheme
Definition ctrad_Correct_prop (t:term) (v:term):Prop:=
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 ->
ceval_term (unApp (ctrad t) k) r.
Definition ctrad_list_Correct_Prop (tl : list term) (vl : list term):Prop:=
forall i t v,
nth_error tl i = Some t -> nth_error vl i = Some v ->
ctrad_Correct_prop t v.
Lemma mu_correct:
forall (ari : nat) (t : term),
ctrad_Correct_prop (Mu ari t) (Mu ari t).
Lemma lamb_correct:
forall (ari : nat) (t : term), ctrad_Correct_prop (Lamb ari t) (Lamb ari t).
Lemma mkargs2_1:
forall t2 vb k r,
eval_list t2 vb ->
(forall (i : nat) (t v : term),
nth_error t2 i = Some t ->
nth_error vb i = Some v -> ctrad_Correct_prop t v ) ->
Cvalid_at_depth (length t2) k ->
ceval_term (CTsubst_rec (rev (ctrad_atom_list vb)) nil k O O) r ->
ceval_term (mkargs2 (ctrad_list t2) k) r.
Lemma app_correct:
forall (t1 : term) (t2 vb : list term) (t v : term) (ari : nat),
eval_term t1 (Lamb ari t) ->
ctrad_Correct_prop t1 (Lamb ari t) ->
length t2 = S ari ->
eval_list t2 vb ->
ctrad_list_Correct_Prop t2 vb ->
eval_term (subst_rec (rev vb) t 0) v ->
ctrad_Correct_prop (subst_rec (rev vb) t 0) v ->
ctrad_Correct_prop (App t1 t2) v.
Lemma appr_correct:
forall (t1 : term) (t2 vb : list term) (t v : term) (ari : nat),
eval_term t1 (Mu ari t) ->
ctrad_Correct_prop t1 (Mu ari t) ->
length t2 = S ari ->
eval_list t2 vb ->
ctrad_list_Correct_Prop t2 vb ->
eval_term (subst_rec (rev vb ++ Mu ari t :: nil) t 0) v ->
ctrad_Correct_prop (subst_rec (rev vb ++ Mu ari t :: nil) t 0) v ->
ctrad_Correct_prop (App t1 t2) v.
Lemma let_correct:
forall t1 t2 v1 v2 : term,
eval_term t1 v1 ->
ctrad_Correct_prop t1 v1 ->
eval_term (subst_rec (v1 :: nil) t2 0) v2 ->
ctrad_Correct_prop (subst_rec (v1 :: nil) t2 0) v2 ->
ctrad_Correct_prop (tLet t1 t2) v2.
Lemma constr_correct:
forall (n : nat) (l vl : list term),
eval_list l vl ->
ctrad_list_Correct_Prop l vl ->
ctrad_Correct_prop (Con n l) (Con n vl).
Lemma match_correct:
forall (t : term) (n : nat) (lv : list term) (p : list pat)
(ca v : term),
eval_term t (Con n lv) ->
ctrad_Correct_prop t (Con n lv) ->
nth_error p n = Some (Patc (length lv) ca) ->
eval_term (subst_rec (rev lv) ca 0) v ->
ctrad_Correct_prop (subst_rec (rev lv) ca 0) v ->
ctrad_Correct_prop (Match t p) v.
Lemma nil_correct: ctrad_list_Correct_Prop nil nil.
Lemma cons_correct:
forall (a va : term) (m vm : list term),
eval_term a va ->
ctrad_Correct_prop a va ->
eval_list m vm ->
ctrad_list_Correct_Prop m vm ->
ctrad_list_Correct_Prop (a :: m) (va :: vm).
Theorem ctrad_correct:
forall t t0 : term, eval_term t t0 -> ctrad_Correct_prop t t0.
Definition cps (t:term) := unApp (ctrad t) (TLamb 0 (CVar O)).
Semantics preservation of the naive CPS conversion
Theorem cps_correct:
forall t v,
eval_term t v ->
ceval_term (cps t) (ctrad_atom v).