Cleanup

_CoqProject

@@ -9,6 +9,7 @@ theories/prelude/ctx_subst.v
 theories/prelude/properness.v
 theories/prelude/asubst.v
 theories/prelude/bijections.v
+theories/prelude/lang_facts.v
 
 theories/logic/spec_ra.v
 theories/logic/spec_rules.v

theories/prelude/lang_facts.v

+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Assorted facts about operational semantics. *)
+From iris.program_logic Require Import language.
+
+Section facts.
+  Context {Λ : language}.
+  Implicit Types e : expr Λ.
+  Implicit Types σ : state Λ.
+  Implicit Types tp : list (expr Λ).
+
+  Lemma erased_step_nonempty tp σ tp' σ'  :
+    erased_step (tp, σ) (tp', σ') → tp' ≠ [].
+  Proof.
+    intros [? Hs].
+    destruct Hs as [e1 σ1' e2 σ2' efs tp1 tp2 ?? Hstep]; simplify_eq/=.
+    intros [_ HH]%app_eq_nil. by inversion HH.
+  Qed.
+
+  Lemma rtc_erased_step_nonempty tp σ tp' σ'  :
+    rtc erased_step (tp, σ) (tp', σ') → tp ≠ [] → tp' ≠ [].
+  Proof.
+    pose (P := λ (x y : list (expr Λ) * (state Λ)), x.1 ≠ [] → y.1 ≠ []).
+    eapply (rtc_ind_r_weak P).
+    - intros [tp2 σ2]. unfold P. naive_solver.
+    - intros [tp1 σ1] [tp2 σ2] [tp3 σ3]. unfold P; simpl.
+      intros ? ?%erased_step_nonempty. naive_solver.
+  Qed.
+
+
+  Lemma erased_step_ectx e e' tp tp' σ σ' K `{!LanguageCtx K} :
+    erased_step (e :: tp, σ) (e' :: tp', σ') →
+    erased_step ((K e) :: tp, σ) (K e' :: tp', σ').
+  Proof.
+    intros [κ Hst]. inversion Hst; simplify_eq/=.
+    destruct t1 as [|h1 t1]; simplify_eq/=.
+    { simplify_eq/=.
+      eapply fill_step in H1. simpl in H1.
+      econstructor. eapply step_atomic with (t1 := []); eauto. }
+    econstructor. econstructor; eauto.
+    + rewrite app_comm_cons. reflexivity.
+    + rewrite app_comm_cons. reflexivity.
+  Qed.
+
+  Local Definition ffill K `{!LanguageCtx K} :
+    (list (expr Λ) * (state Λ)) → (list (expr Λ) * (state Λ)) :=
+    fun x => match x with
+             | (e :: tp, σ) => (K e :: tp, σ)
+             | ([], σ) => ([], σ)
+             end.
+
+  Lemma rtc_erased_step_ectx e e' tp tp' σ σ' K `{!LanguageCtx K} :
+    rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
+    rtc erased_step (K e :: tp, σ) (K e' :: tp', σ').
+  Proof.
+    change (rtc erased_step (K e :: tp, σ) (K e' :: tp', σ'))
+      with (rtc erased_step (ffill K (e :: tp, σ)) (ffill K (e' :: tp', σ'))).
+    eapply (rtc_congruence (ffill K) erased_step).
+    clear e e' tp tp' σ σ'.
+    intros [tp σ] [tp' σ'].
+    destruct tp as [|e tp].
+    - inversion 1. inversion H0. exfalso.
+      simplify_eq/=. by eapply app_cons_not_nil.
+    - intros Hstep1.
+      assert (tp' ≠ []).
+      { eapply (rtc_erased_step_nonempty (e::tp)).
+        econstructor; naive_solver.
+        naive_solver. }
+      destruct tp' as [|e' tp']; first naive_solver.
+      simpl. by eapply erased_step_ectx.
+  Qed.
+
+  Lemma nice_ctx_lemma K tp1 tp2 e ρ1 ρ2 v `{!LanguageCtx K} :
+    rtc erased_step ρ1 ρ2 →
+    ρ1.1 = (K e) :: tp1 →
+    ρ2.1 = of_val v :: tp2 →
+    ∃ tp2' σ' w,
+      rtc erased_step (e :: tp1, ρ1.2) (of_val w :: tp2', σ').
+  Proof.
+    intros Hsteps.
+    revert tp1 e.
+    induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH]; intros tp1 e Hρ1 Hρ2.
+    { destruct (to_val e) as [w|] eqn:He.
+    - apply of_to_val in He as <-.
+      exists tp1, ρ.2, w. reflexivity.
+    - assert (to_val (K e) = None) by auto using fill_not_val.
+      destruct ρ as [ρ1 ρ2]. simplify_eq/=.
+      assert (of_val v = K e) as ?%of_to_val_flip; naive_solver. }
+    destruct Hstep as [κs [e1 σ1 e2 σ2 efs t1 t2 -> -> Hstep]]; simpl in *.
+    destruct t1 as [|h1 t1]; simplify_eq/=.
+    - destruct (to_val e) as [w|] eqn:He.
+      + apply of_to_val in He as <-.
+        eexists _, _, w. reflexivity.
+      + apply fill_step_inv in Hstep as (e2'&->&Hstep); last done.
+        specialize (IH (tp1++efs) e2').
+        assert (K e2' :: tp1 ++ efs = K e2' :: tp1 ++ efs) as H1 by done.
+        specialize (IH H1 Hρ2).
+        destruct IH as (tp2'&σ'&w&Hsteps1).
+        eexists _,_,w. eapply rtc_l, Hsteps1.
+        exists κs. by eapply step_atomic with (t1:=[]).
+    - specialize (IH (t1 ++ e2 :: t2 ++ efs) e).
+      assert (K e :: t1 ++ e2 :: t2 ++ efs = K e :: t1 ++ e2 :: t2 ++ efs) as H1 by done.
+    specialize (IH H1 Hρ2).
+    destruct IH as (tp2'&σ'&w&Hsteps1).
+    eexists _,_,w. eapply rtc_l, Hsteps1.
+    exists κs. econstructor; rewrite ?app_comm_cons; done.
+  Qed.
+
+  Lemma nice_ctx_lemma' K tp1 tp2 e σ1 σ2 v `{!LanguageCtx K} :
+    rtc erased_step ((K e) :: tp1, σ1) (of_val v :: tp2, σ2) →
+    ∃ tp2' σ' w,
+      rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ').
+  Proof.
+    pose (ρ1:=((K e) :: tp1, σ1)).
+    pose (ρ2:=(of_val v :: tp2, σ2)).
+    fold ρ1 ρ2. intros Hρ.
+    change σ1 with ρ1.2. eapply nice_ctx_lemma; eauto.
+  Qed.
+
+End facts.

theories/typing/contextual_refinement.v

@@ -3,6 +3,7 @@
 From Autosubst Require Import Autosubst.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
+From reloc.prelude Require Import lang_facts.
 From reloc.typing Require Export types interp fundamental.
 
 Inductive ctx_item :=
@@ -314,117 +315,6 @@ Definition ctx_refines_alt (Γ : stringmap type)
   rtc erased_step ([fill_ctx K e], σ₀) (of_val v1 :: thp, σ₁) →
   ∃ thp' σ₁' v2, rtc erased_step ([fill_ctx K e'], σ₀) (of_val v2 :: thp', σ₁').
 
-(* Helper lemmas *)
-Lemma erased_step_ectx (e e' : expr) tp tp' σ σ' K :
-  erased_step (e :: tp, σ) (e' :: tp', σ') →
-  erased_step ((fill K e) :: tp, σ) (fill K e' :: tp', σ').
-Proof.
-  intros [κ Hst]. inversion Hst; simplify_eq/=.
-  destruct t1 as [|h1 t1]; simplify_eq/=.
-  { simplify_eq/=.
-    eapply fill_prim_step in H1. simpl in H1.
-    econstructor. eapply step_atomic with (t1 := []); eauto. }
-  econstructor. econstructor; eauto.
-  + rewrite app_comm_cons. reflexivity.
-  + rewrite app_comm_cons. reflexivity.
-Qed.
-
-Lemma erased_step_nonempty  (tp : list expr) σ tp' σ'  :
-  erased_step (tp, σ) (tp', σ') → tp' ≠ [].
-Proof.
-  intros [? Hs].
-  destruct Hs as [e1 σ1' e2 σ2' efs tp1 tp2 ?? Hstep]; simplify_eq/=.
-  intros [_ HH]%app_eq_nil. by inversion HH.
-Qed.
-
-Lemma rtc_erased_step_nonempty (tp : list expr) σ tp' σ'  :
-  rtc erased_step (tp, σ) (tp', σ') → tp ≠ [] → tp' ≠ [].
-Proof.
-  pose (P := λ (x y : list expr * state), x.1 ≠ [] → y.1 ≠ []).
-  eapply (rtc_ind_r_weak P).
-  - intros [tp2 σ2]. unfold P. naive_solver.
-  - intros [tp1 σ1] [tp2 σ2] [tp3 σ3]. unfold P; simpl.
-    intros ? ?%erased_step_nonempty. naive_solver.
-Qed.
-
-
-Local Definition ffill (K : list ectx_item) :
-  (list expr * state) → (list expr * state) :=
-  fun x => match x with
-           | (e :: tp, σ) => (fill K e :: tp, σ)
-           | ([], σ) => ([], σ)
-           end.
-
-Lemma rtc_erased_step_ectx (e e' : expr) tp tp' σ σ' K :
-  rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
-  rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
-Proof.
-  change (rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ'))
-    with (rtc erased_step (ffill K (e :: tp, σ)) (ffill K (e' :: tp', σ'))).
-  eapply (rtc_congruence (ffill K) erased_step).
-  clear e e' tp tp' σ σ'.
-  intros [tp σ] [tp' σ'].
-  destruct tp as [|e tp].
-  - inversion 1. inversion H0. exfalso.
-    simplify_eq/=. by eapply app_cons_not_nil.
-  - intros Hstep1.
-    assert (tp' ≠ []).
-    { eapply (rtc_erased_step_nonempty (e::tp)).
-      econstructor; naive_solver.
-      naive_solver. }
-    destruct tp' as [|e' tp']; first naive_solver.
-    simpl.
-    by eapply erased_step_ectx.
-Qed.
-
-Lemma nice_ctx_lemma K tp1 tp2 e ρ1 ρ2 v :
-  rtc erased_step ρ1 ρ2 →
-  ρ1.1 = (fill K e) :: tp1 →
-  ρ2.1 = of_val v :: tp2 →
-  ∃ tp2' σ' w,
-    rtc erased_step (e :: tp1, ρ1.2) (of_val w :: tp2', σ').
-Proof.
-  intros Hsteps.
-  revert tp1 e.
-  induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH]; intros tp1 e Hρ1 Hρ2.
-  { destruct (to_val e) as [w|] eqn:He.
-    - apply of_to_val in He as <-.
-      exists tp1, ρ.2, w. reflexivity.
-    - assert (to_val (fill K e) = None) by auto using fill_not_val.
-      destruct ρ as [ρ1 ρ2]. simplify_eq/=.
-      assert (of_val v = fill K e) as ?%of_to_val_flip; naive_solver. }
-  destruct Hstep as [κs [e1 σ1 e2 σ2 efs t1 t2 -> -> Hstep]]; simpl in *.
-  destruct t1 as [|h1 t1]; simplify_eq/=.
-  - destruct (to_val e) as [w|] eqn:He.
-    + apply of_to_val in He as <-.
-      eexists _, _, w. reflexivity.
-    + apply fill_step_inv in Hstep as (e2'&->&Hstep); last done.
-      specialize (IH (tp1++efs) e2').
-      assert (fill K e2' :: tp1 ++ efs = fill K e2' :: tp1 ++ efs) as H1 by done.
-      specialize (IH H1 Hρ2).
-      destruct IH as (tp2'&σ'&w&Hsteps1).
-      eexists _,_,w. eapply rtc_l, Hsteps1.
-      exists κs. by eapply step_atomic with (t1:=[]).
-  - specialize (IH (t1 ++ e2 :: t2 ++ efs) e).
-    assert (fill K e :: t1 ++ e2 :: t2 ++ efs = fill K e :: t1 ++ e2 :: t2 ++ efs) as H1 by done.
-    specialize (IH H1 Hρ2).
-    destruct IH as (tp2'&σ'&w&Hsteps1).
-    eexists _,_,w. eapply rtc_l, Hsteps1.
-    exists κs. econstructor; rewrite ?app_comm_cons; done.
-Qed.
-
-Lemma nice_ctx_lemma' K tp1 tp2 e σ1 σ2 v :
-  rtc erased_step ((fill K e) :: tp1, σ1) (of_val v :: tp2, σ2) →
-  ∃ tp2' σ' w,
-    rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ').
-Proof.
-  pose (ρ1:=((fill K e) :: tp1, σ1)).
-  pose (ρ2:=(of_val v :: tp2, σ2)).
-  fold ρ1 ρ2. intros Hρ.
-  change σ1 with ρ1.2. eapply nice_ctx_lemma; eauto.
-Qed.
-(*/Helper lemmas*)
-
 Lemma ctx_refines_impl_alt Γ e1 e2 τ :
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
   ctx_refines_alt Γ e1 e2 τ.
@@ -436,7 +326,8 @@ Proof.
                 (of_val #true :: thp', σ₁')).
   - unfold C'; simpl.
     destruct 1 as (thp' & σ1' & Hstep').
-    eapply (nice_ctx_lemma' [AppRCtx (λ: <>, #true)] []).
+    eapply (nice_ctx_lemma' (fill [AppRCtx (λ: <>, #true)]) []).
+    { apply _. }
     eapply Hstep'.
   - eapply (H C' thp _ σ1 #true TBool).
     + repeat econstructor; eauto.
@@ -456,7 +347,7 @@ Proof.
       pose (K := [AppRCtx (λ: <>, #true)%E]).
       change (fill_ctx C e1;; #true)%E with (fill K (fill_ctx C e1)).
       change (v1;; #true)%E with (fill K (of_val v1)).
-      by eapply rtc_erased_step_ectx.
+      by eapply rtc_erased_step_ectx; first by apply _.
 Qed.
 
 Definition ctx_equiv Γ e1 e2 τ :=