Some tweaks.

In particular, remove ectx_language.atomic, because it seems unused
expect for a smart constructor for language.atomic.

heap_lang/heap.v

@@ -153,7 +153,7 @@ Section heap.
     to_val e = Some v → nclose heapN ⊆ E →
     heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
-    iIntros (?%of_to_val ?) "[#Hinv HΦ]". subst. rewrite /heap_ctx.
+    iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
     iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
@@ -186,7 +186,7 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    iIntros (?%of_to_val ?) "[#Hh [Hl HΦ]]". subst.
+    iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
@@ -202,7 +202,7 @@ Section heap.
     heap_ctx ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (?%of_to_val ?%of_to_val ??) "[#Hh [Hl HΦ]]". subst.
+    iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
@@ -217,7 +217,7 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (?%of_to_val ?%of_to_val ?) "[#Hh [Hl HΦ]]". subst.
+    iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.

heap_lang/tactics.v

@@ -183,14 +183,14 @@ Definition atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → ectx_language.atomic (to_expr e).
+Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
 Proof.
-  intros He. split.
+  intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef.
     destruct e; simpl; try done; repeat (case_match; try done);
     inversion 1; rewrite ?to_of_val; eauto. subst.
     unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
-  - intros K e' Hfill Hnotval. destruct K as [|Ki K]; [done|exfalso].
+  - intros [|Ki K] e' Hfill Hnotval; [done|exfalso].
     apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
     revert He. destruct e; simpl; try done; repeat (case_match; try done);
     rewrite ?bool_decide_spec;
@@ -223,16 +223,12 @@ Ltac solve_to_val :=
   end.
 
 Ltac solve_atomic :=
-  try match goal with
-  | |- language.atomic ?e => apply ectx_language_atomic
-  end;
   match goal with
-  | |- ectx_language.atomic ?e =>
-     let e' := W.of_expr e in change (atomic (W.to_expr e'));
+  | |- language.atomic ?e =>
+     let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
      apply W.atomic_correct; vm_compute; exact I
   end.
 Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
-Hint Extern 0 (ectx_language.atomic _) => solve_atomic : fsaV.
 
 (** Substitution *)
 Ltac simpl_subst :=

program_logic/ectx_language.v

@@ -59,10 +59,6 @@ Section ectx_language.
   Definition head_reducible (e : expr) (σ : state) :=
     ∃ e' σ' ef, head_step e σ e' σ' ef.
 
-  Definition atomic (e : expr) :=
-    (∀ σ e' σ' ef, head_step e σ e' σ' ef → is_Some (to_val e')) ∧
-    (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx).
-
   Inductive prim_step (e1 : expr) (σ1 : state)
       (e2 : expr) (σ2 : state) (ef : option expr) : Prop :=
     Ectx_step K e1' e2' :
@@ -73,22 +69,6 @@ Section ectx_language.
     prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
   Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
 
-  Lemma atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
-  Proof. destruct 1 as [? _]; eauto. Qed.
-
-  Lemma atomic_fill e K :
-    atomic (fill K e) → to_val e = None → K = empty_ectx.
-  Proof. destruct 1 as [_ ?]; eauto. Qed.
-
-  Lemma atomic_prim_step e1 σ1 e2 σ2 ef :
-    atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
-  Proof.
-    intros Hatomic [K e1' e2' -> -> Hstep].
-    assert (K = empty_ectx) as -> by eauto 10 using atomic_fill, val_stuck.
-    revert Hatomic; rewrite !fill_empty. eauto using atomic_step.
-  Qed.
-
   Canonical Structure ectx_lang : language := {|
     language.expr := expr; language.val := val; language.state := state;
     language.of_val := of_val; language.to_val := to_val;
@@ -105,11 +85,14 @@ Section ectx_language.
   Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ.
   Proof. intros (e'&σ'&ef&?). eexists e', σ', ef. by apply head_prim_step. Qed.
 
-  Lemma ectx_language_atomic e : atomic e → language.atomic e.
+  Lemma ectx_language_atomic e :
+    (∀ σ e' σ' ef, head_step e σ e' σ' ef → is_Some (to_val e')) →
+    (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx) →
+    atomic e.
   Proof.
-    intros Hatomic σ e' σ' ef [K e1' e2' -> -> Hstep].
-    assert (K = empty_ectx) as -> by eauto 10 using atomic_fill, val_stuck.
-    revert Hatomic; rewrite !fill_empty. intros. by eapply atomic_step.
+    intros Hatomic_step Hatomic_fill σ e' σ' ef [K e1' e2' -> -> Hstep].
+    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
   Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef :

program_logic/weakestpre.v

@@ -161,8 +161,8 @@ Lemma wp_atomic E1 E2 e Φ :
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
   rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs.
-  destruct (to_val e) as [v|] eqn:Hvale.
-  - apply of_to_val in Hvale. subst e. eapply wp_pre_value. rewrite pvs_eq.
+  destruct (Some_dec (to_val e)) as [[v <-%of_to_val]|].
+  - eapply wp_pre_value. rewrite pvs_eq.
     intros k Ef σ rf ???. destruct (Hvs k Ef σ rf) as (r'&Hwp&?); auto.
     apply wp_value_inv in Hwp. rewrite pvs_eq in Hwp.
     destruct (Hwp k Ef σ rf) as (r2'&HΦ&?); auto.