From 88cac698b89ea68b98df70187d119da08f74aa6b Mon Sep 17 00:00:00 2001
From: adelaett <90894311+adelaett@users.noreply.github.com>
Date: Thu, 25 Jan 2024 10:26:50 +0100
Subject: [PATCH] insucessfull atempt at show trans with conts

---
 theories/trans.v | 53 ++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 51 insertions(+), 2 deletions(-)

diff --git a/theories/trans.v b/theories/trans.v
index 1867079..5ccc9fb 100644
--- a/theories/trans.v
+++ b/theories/trans.v
@@ -486,10 +486,59 @@ Proof.
   intros; simpl; eauto.
 Qed.
 
+Definition map_cont (map_term: term -> term) (map_value: value -> value) (k: cont) : cont :=
+  match k with
+  | CAppR t2 => CAppR (map_term t2)
+  | CBinopL op v1 => CBinopL op (map_value v1)
+  | CBinopR op t2 => CBinopR op (map_term t2)
+  | CClosure t_cl sigma_cl => CClosure (t_cl) (List.map map_value sigma_cl)
+  | CReturn sigma' => CReturn (List.map map_value sigma')
+  | CDefaultBase tc => CIf (map_term tc) ENone
+  | CMatch t1 t2 => CMatch (map_term t1) (map_term t2)
+  | CSome => CSome
+  | CIf t1 t2 => CIf (map_term t1) (map_term t2)
+  | CErrorOnEmpty => CErrorOnEmpty
+  | CDefaultPure => CDefaultPure
+  | CDefault b None ts tj tc =>
+    CDefault b (None) (List.map map_term ts) (map_term tj) (map_term tc)
+  | CDefault b (Some v) ts tj tc =>
+    CDefault b (Some (map_value v)) (List.map map_term ts) (map_term tj) (map_term tc)
+  end.
+
+Fixpoint map_conts_until_return
+  map_term map_value (kappa: list cont) : list cont :=
+  match kappa with
+  | CReturn sigma :: kappa =>
+    CReturn (List.map map_value sigma) :: kappa
+  | h :: t =>
+    (map_cont map_term map_value h) :: (map_conts_until_return map_term map_value t)
+  | [] => [] 
+  end.
+
+Definition lift_state a s :=
+  match s with
+  | mode_eval t kappa sigma =>
+    mode_eval (lift 1 t) (map_conts_until_return (fun t => lift 1 t) (fun x => x) kappa) (a::sigma)
+  | mode_cont kappa sigma r =>
+    mode_cont (map_conts_until_return (fun t => lift 1 t) (fun x => x) kappa) (a::sigma) r
+  end.
+
+Goal
+  forall {v s1 s2},
+  cred s1 s2 ->
+  cred (lift_state v s1) (lift_state v s2).
+Proof.
+  induction 1.
+  all: try solve [simpl; econstructor].
+  all: admit.
+Abort.
+
+
+
 Lemma thing:
-  forall {t sigma sigma' r a},
+  forall {t sigma sigma' r v},
   star cred (mode_eval t [] sigma) (mode_cont [] sigma' r ) ->
-  star cred (mode_eval (lift 1 t) [] (a :: sigma)) (mode_cont [] (a:: sigma') r).
+  star cred (mode_eval (lift 1 t) [] (v :: sigma)) (mode_cont [] (v:: sigma') r).
 Admitted.
 
 Require Import simulation_sred_to_cred.