Misc properties about languages.

theories/heap_lang/tactics.v

@@ -185,13 +185,13 @@ Definition atomic (e : expr) :=
   end.
 Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
 Proof.
-  intros He. apply ectxi_language_atomic.
+  intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *.
     apply language.val_irreducible; revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
-  - intros Ki e' Hfill []%eq_None_not_Some; simpl in *.
+  - apply ectxi_language_sub_values=> /= Ki e' Hfill.
     destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
       naive_solver eauto using to_val_is_Some.
 Qed.

theories/program_logic/ectx_language.v

@@ -59,6 +59,11 @@ Section ectx_language.
 
   Definition head_reducible (e : expr) (σ : state) :=
     ∃ e' σ' efs, head_step e σ e' σ' efs.
+  Definition head_irreducible (e : expr) (σ : state) :=
+    ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
+
+  Definition sub_values (e : expr) :=
+    ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
 
   Inductive prim_step (e1 : expr) (σ1 : state)
       (e2 : expr) (σ2 : state) (efs : list expr) : Prop :=
@@ -87,12 +92,32 @@ Section ectx_language.
     head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
   Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
 
+  Lemma not_head_reducible e σ : ¬head_reducible e σ ↔ head_irreducible e σ.
+  Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
+
   Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ.
   Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
+  Lemma head_prim_irreducible e σ : irreducible e σ → head_irreducible e σ.
+  Proof.
+    rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
+  Qed.
+
+  Lemma prim_head_reducible e σ :
+    reducible e σ → sub_values e → head_reducible e σ.
+  Proof.
+    intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
+    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+    rewrite fill_empty /head_reducible; eauto.
+  Qed.
+  Lemma prim_head_irreducible e σ :
+    head_irreducible e σ → sub_values e → irreducible e σ.
+  Proof.
+    rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
+  Qed.
 
   Lemma ectx_language_atomic e :
     (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
-    (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx) →
+    sub_values e →
     atomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
@@ -101,7 +126,8 @@ Section ectx_language.
   Qed.
 
   Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs :
-    head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 efs →
+    head_reducible e1 σ1 →
+    prim_step e1 σ1 e2 σ2 efs →
     head_step e1 σ1 e2 σ2 efs.
   Proof.
     intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].

theories/program_logic/ectxi_language.v

@@ -90,30 +90,14 @@ Section ectxi_language.
     fill_not_val, fill_app, step_by_val, foldl_app.
   Next Obligation. intros K1 K2 ?%app_eq_nil; tauto. Qed.
 
-  Lemma ectxi_language_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
-    (∀ Ki e', e = fill_item Ki e' → to_val e' = None → False) →
-    atomic e.
+  Lemma ectxi_language_sub_values e :
+    (∀ Ki e', e = fill_item Ki e' → is_Some (to_val e')) → sub_values e.
   Proof.
-    intros Hastep Hafill. apply ectx_language_atomic=> //= {Hastep} K e'.
-    destruct K as [|Ki K IH] using @rev_ind=> //=.
-    rewrite fill_app /= => He Hnval.
-    destruct (Hafill Ki (fill K e')); auto using fill_not_val.
+    intros Hsub K e' ->. destruct K as [|Ki K _] using @rev_ind=> //=.
+    intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
   Qed.
 
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).
   Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
-
-  Lemma step_is_head K e σ :
-    to_val e = None →
-    (∀ Ki K e', e = fill (Ki :: K) e' → ¬head_reducible e' σ) →
-    reducible (fill K e) σ → head_reducible e σ.
-  Proof.
-    intros Hnonval Hnondecomp (e'&σ''&ef&Hstep).
-    change fill with ectx_language.fill in Hstep.
-    apply fill_step_inv in Hstep as (e2'&_&Hstep); last done.
-    clear K. destruct Hstep as [[|Ki K] e1' e2'' -> -> Hstep]; [red; eauto|].
-    destruct (Hnondecomp Ki K e1'); unfold head_reducible; eauto.
-  Qed.
 End ectxi_language.

theories/program_logic/language.v

@@ -29,6 +29,17 @@ Canonical Structure exprC Λ := leibnizC (expr Λ).
 
 Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
+Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
+  fill_not_val e :
+    to_val e = None → to_val (K e) = None;
+  fill_step e1 σ1 e2 σ2 efs :
+    prim_step e1 σ1 e2 σ2 efs →
+    prim_step (K e1) σ1 (K e2) σ2 efs;
+  fill_step_inv e1' σ1 e2 σ2 efs :
+    to_val e1' = None → prim_step (K e1') σ1 e2 σ2 efs →
+    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
+}.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.
@@ -36,9 +47,11 @@ Section language.
   Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' efs, prim_step e σ e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
-    ∀e' σ' efs, ¬prim_step e σ e' σ' efs. 
+    ∀ e' σ' efs, ¬prim_step e σ e' σ' efs.
+
   Definition atomic (e : expr Λ) : Prop :=
     ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'.
+
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
@@ -48,21 +61,23 @@ Section language.
 
   Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
   Proof. intros <-. by rewrite to_of_val. Qed.
+
+  Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ.
+  Proof. unfold reducible, irreducible. naive_solver. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
   Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
   Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
-End language.
 
-Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
-  fill_not_val e :
-    to_val e = None → to_val (K e) = None;
-  fill_step e1 σ1 e2 σ2 efs :
-    prim_step e1 σ1 e2 σ2 efs →
-    prim_step (K e1) σ1 (K e2) σ2 efs;
-  fill_step_inv e1' σ1 e2 σ2 efs :
-    to_val e1' = None → prim_step (K e1') σ1 e2 σ2 efs →
-    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
-}.
+  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
+    to_val e = None → reducible (K e) σ → reducible e σ.
+  Proof.
+    intros ? (e'&σ'&efs&Hstep); unfold reducible.
+    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
+  Qed.
+  Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
+    to_val e = None → irreducible e σ → irreducible (K e) σ.
+  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
+End language.