move gen_ctx_rel to separate file

_CoqProject

@@ -39,6 +39,7 @@ theories/simplang/heapbij.v
 theories/simplang/parallel_subst.v
 theories/simplang/gen_log_rel.v
 theories/simplang/gen_adequacy.v
+theories/simplang/behavior.v
 
 theories/simplang/examples/sum.v
 

theories/simplang/behavior.v

+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import iprop.
+
+From simuliris.logic Require Import satisfiable.
+From simuliris.simulation Require Import behavior.
+From simuliris.simplang Require Import lang notation parallel_subst wf gen_val_rel.
+
+(** Define "observable behavior" and a generic notion of contextual refinement.
+*)
+Section ctx_rel.
+  Context (expr_head_wf : expr_head → Prop).
+
+  (* TODO: generalize *)
+  Let init_state (σ_t σ_s : state) : Prop := σ_t = state_empty ∧ σ_s = state_empty.
+
+  Fixpoint obs_val (v_t v_s : val) {struct v_s} : Prop :=
+    match v_t, v_s with
+    | LitV (LitLoc l_t), LitV (LitLoc l_s) =>
+      True (* the details of locations are not observable *)
+    | LitV l_t, LitV l_s =>
+      l_t = l_s
+    | PairV v1_t v2_t, PairV v1_s v2_s =>
+      obs_val v1_t v1_s ∧ obs_val v2_t v2_s
+    | InjLV v_t, InjLV v_s =>
+      obs_val v_t v_s
+    | InjRV v_t, InjRV v_s =>
+      obs_val v_t v_s
+    | _,_ => False
+    end.
+
+  (** The simplang instance of [beh_rel]. *)
+  Definition beh_rel := beh_rel init_state "main" #() obs_val.
+
+  (** Contextual refinement:
+      The two [e] can be put into an arbitrary context in an arbitrary function.
+      [λ: x, e] denotes an evaluation context [let x = <hole> in e]; then the
+      <hole> will be the function argument. *)
+  Definition gen_ctx_rel (e_t e_s : expr) :=
+    ∀ (C : ctx) (fname x : string) (p : prog),
+      gen_ctx_wf expr_head_wf C →
+      map_Forall (const (gen_ectx_wf expr_head_wf)) p →
+      free_vars (fill_ctx C e_t) ∪ free_vars (fill_ctx C e_s) ⊆ {[x]} →
+      beh_rel (<[fname := (λ: x, fill_ctx C e_t)%E]> p) (<[fname := (λ: x, fill_ctx C e_s)%E]> p).
+
+  Lemma gen_val_rel_obs {Σ} loc_rel v_t v_s :
+    gen_val_rel loc_rel v_t v_s ⊢@{iPropI Σ} ⌜obs_val v_t v_s⌝.
+  Proof.
+    iInduction v_t as [[| | | | |]| | |] "IH" forall (v_s);
+      destruct v_s as [[| | | | |]| | |]; try by eauto.
+    - simpl. iIntros "[Hv1 Hv2]". iSplit.
+      + by iApply "IH".
+      + by iApply "IH1".
+  Qed.
+End ctx_rel.

theories/simplang/gen_adequacy.v

-(** Adequacy of our logical relation: it implies contextual refinement. *)
-
 From simuliris.logic Require Import satisfiable.
-From simuliris.simulation Require Import slsls behavior global_sim adequacy.
-From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst gen_log_rel gen_val_rel wf.
-
-(** Generic notion of contextual refinement. *)
-Section ctx_rel.
-  Context (expr_head_wf : expr_head → Prop).
-
-  (* TODO: generalize *)
-  Let init_state (σ_t σ_s : state) : Prop := σ_t = state_empty ∧ σ_s = state_empty.
-
-  Fixpoint obs_val (v_t v_s : val) {struct v_s} : Prop :=
-    match v_t, v_s with
-    | LitV (LitLoc l_t), LitV (LitLoc l_s) =>
-      True (* the details of locations are not observable *)
-    | LitV l_t, LitV l_s =>
-      l_t = l_s
-    | PairV v1_t v2_t, PairV v1_s v2_s =>
-      obs_val v1_t v1_s ∧ obs_val v2_t v2_s
-    | InjLV v_t, InjLV v_s =>
-      obs_val v_t v_s
-    | InjRV v_t, InjRV v_s =>
-      obs_val v_t v_s
-    | _,_ => False
-    end.
-
-  (** The simplang instance of [beh_rel]. *)
-  Definition beh_rel := beh_rel init_state "main" #() obs_val.
-
-  (** Contextual refinement:
-      The two [e] can be put into an arbitrary context in an arbitrary function.
-      [λ: x, e] denotes an evaluation context [let x = <hole> in e]; then the
-      <hole> will be the function argument. *)
-  Definition gen_ctx_rel (e_t e_s : expr) :=
-    ∀ (C : ctx) (fname x : string) (p : prog),
-      gen_ctx_wf expr_head_wf C →
-      map_Forall (const (gen_ectx_wf expr_head_wf)) p →
-      free_vars (fill_ctx C e_t) ∪ free_vars (fill_ctx C e_s) ⊆ {[x]} →
-      beh_rel (<[fname := (λ: x, fill_ctx C e_t)%E]> p) (<[fname := (λ: x, fill_ctx C e_s)%E]> p).
-
-  Lemma gen_val_rel_obs {Σ} loc_rel v_t v_s :
-    gen_val_rel loc_rel v_t v_s ⊢@{iPropI Σ} ⌜obs_val v_t v_s⌝.
-  Proof.
-    iInduction v_t as [[| | | | |]| | |] "IH" forall (v_s);
-      destruct v_s as [[| | | | |]| | |]; try by eauto.
-    - simpl. iIntros "[Hv1 Hv2]". iSplit.
-      + by iApply "IH".
-      + by iApply "IH1".
-  Qed.
-End ctx_rel.
+From simuliris.simulation Require Import slsls global_sim adequacy.
+From simuliris.simplang Require Import proofmode tactics behavior.
+From simuliris.simplang Require Import parallel_subst gen_val_rel.
 
 (** Generic adequacy theorem for sheap-based logical relations. *)
 Section adequacy.

theories/simplang/simple_inv/adequacy.v

+(** The logical relation implies contextual refinement. *)
+
 From iris.algebra.lib Require Import gset_bij.
 From iris.base_logic.lib Require Import gset_bij.
 
 From simuliris.logic Require Import satisfiable.
 From simuliris.simulation Require Import slsls global_sim.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import gen_adequacy.
+From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst.
 From simuliris.simplang.simple_inv Require Import inv refl.
 
+(** Instantiate our notion of contextual refinement. *)
+Notation ctx_rel := (gen_ctx_rel expr_head_wf).
+
+(** Whole-program adequacy. *)
 Class simpleGpreS Σ := {
   sbij_pre_heapG :> sheapGpreS Σ;
   sbij_pre_bijG :> heapbijGpreS Σ;
@@ -17,7 +23,7 @@ Global Instance subG_sbijΣ Σ :
   subG simpleΣ Σ → simpleGpreS Σ.
 Proof. solve_inG. Qed.
 
-Lemma adequacy `{!simpleGpreS Σ} p_t p_s :
+Lemma prog_rel_adequacy `{!simpleGpreS Σ} p_t p_s :
   isat (∀ `(simpleGS Σ), prog_rel p_t p_s) →
   beh_rel p_t p_s.
 Proof.
@@ -33,3 +39,11 @@ Proof.
   iSplitR; first done.
   iIntros (??) "$".
 Qed.
+
+(** Adequacy for open terms. *)
+Theorem log_rel_adequacy `{!simpleGpreS Σ} e_t e_s :
+  isat (∀ `(simpleGS Σ), log_rel e_t e_s) →
+  ctx_rel e_t e_s.
+Proof.
+  (* TODO *)
+Abort.