Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/agree.v

@@ -3,7 +3,7 @@ From iris.algebra Require Import upred.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
-  agree_car :> nat → A;
+  agree_car : nat → A;
   agree_is_valid : nat → Prop;
   agree_valid_S n : agree_is_valid (S n) → agree_is_valid n
 }.
@@ -15,7 +15,7 @@ Section agree.
 Context {A : cofeT}.
 
 Instance agree_validN : ValidN (agree A) := λ n x,
-  agree_is_valid x n ∧ ∀ n', n' ≤ n → x n ≡{n'}≡ x n'.
+  agree_is_valid x n ∧ ∀ n', n' ≤ n → agree_car x n ≡{n'}≡ agree_car x n'.
 Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
 
 Lemma agree_valid_le n n' (x : agree A) :
@@ -24,12 +24,13 @@ Proof. induction 2; eauto using agree_valid_S. Qed.
 
 Instance agree_equiv : Equiv (agree A) := λ x y,
   (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
-  (∀ n, agree_is_valid x n → x n ≡{n}≡ y n).
+  (∀ n, agree_is_valid x n → agree_car x n ≡{n}≡ agree_car y n).
 Instance agree_dist : Dist (agree A) := λ n x y,
   (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
-  (∀ n', n' ≤ n → agree_is_valid x n' → x n' ≡{n'}≡ y n').
+  (∀ n', n' ≤ n → agree_is_valid x n' → agree_car x n' ≡{n'}≡ agree_car y n').
 Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
+  {| agree_car n := agree_car (c n) n;
+     agree_is_valid n := agree_is_valid (c n) n |}.
 Next Obligation.
   intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
 Qed.
@@ -44,20 +45,15 @@ Proof.
     + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
     + intros x y z Hxy Hyz; split; intros n'; intros.
       * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
-      * trans (y n'). by apply Hxy. by apply Hyz, Hxy.
+      * trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
   - intros n x y Hxy; split; intros; apply Hxy; auto.
   - intros n c; apply and_wlog_r; intros;
       symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
 Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
 
-Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
-Proof. by intros [??] Hxy; apply Hxy. Qed.
-Lemma agree_cauchy n (x : agree A) i : ✓{n} x → i ≤ n → x n ≡{i}≡ x i.
-Proof. by intros [? Hx]; apply Hx. Qed.
-
 Program Instance agree_op : Op (agree A) := λ x y,
-  {| agree_car := x;
+  {| agree_car := agree_car x;
      agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_pcore : PCore (agree A) := Some.
@@ -127,13 +123,19 @@ Proof. by constructor. Qed.
 Program Definition to_agree (x : A) : agree A :=
   {| agree_car n := x; agree_is_valid n := True |}.
 Solve Obligations with done.
+
 Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
 Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
+
 Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
-Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
-Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
+
+Lemma to_agree_uninj n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x.
+Proof.
+  intros [??]. exists (agree_car x n).
+  split; naive_solver eauto using agree_valid_le.
+Qed.
 
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
@@ -148,7 +150,7 @@ Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x;
+  {| agree_car n := f (agree_car x n); agree_is_valid := agree_is_valid x;
      agree_valid_S := agree_valid_S _ x |}.
 Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
 Proof. by destruct x. Qed.

heap_lang/heap.v

@@ -153,12 +153,12 @@ 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 (??) "[#Hinv HΦ]". 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 _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
-    iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
+    iApply wp_alloc_pst. iFrame "Hheap". iNext.
     iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
     iFrame "Hheap". iSplitR; first iPureIntro.
@@ -173,7 +173,7 @@ Section heap.
   Proof.
     iIntros (?) "[#Hh [Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
     rewrite of_heap_singleton_op //. iFrame "Hl".
@@ -186,9 +186,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    iIntros (??) "[#Hh [Hl HΦ]]".
+    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 _)); simpl; eauto.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
@@ -202,9 +202,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (????) "[#Hh [Hl HΦ]]".
+    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 _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
     rewrite of_heap_singleton_op //. iFrame "Hl".
@@ -217,9 +217,9 @@ Section heap.
     heap_ctx ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros (???) "[#Hh [Hl HΦ]]".
+    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 _)); simpl; eauto 10.
+    iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); eauto with fsaV.
     iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".

heap_lang/lang.v

@@ -273,19 +273,6 @@ Inductive head_step : expr → state → expr → state → option (expr) → Pr
      σ !! l = Some v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
-(** Atomic expressions *)
-Definition atomic (e: expr) :=
-  match e with
-  | Alloc e => is_Some (to_val e)
-  | Load e => is_Some (to_val e)
-  | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
-  | CAS e0 e1 e2 =>
-     is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
-  (* Make "skip" atomic *)
-  | App (Rec _ _ (Lit _)) (Lit _) => True
-  | _ => False
-  end.
-
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
 Proof.
@@ -310,22 +297,6 @@ Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma atomic_not_val e : atomic e → to_val e = None.
-Proof. by destruct e. Qed.
-
-Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
-Proof.
-  intros. destruct Ki; simplify_eq/=; destruct_and?;
-    repeat (simpl || case_match || contradiction); eauto.
-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 2; simpl; rewrite ?to_of_val; try by eauto. subst.
-  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
-Qed.
-
 Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
   head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
@@ -391,13 +362,11 @@ Program Instance heap_ectxi_lang :
   EctxiLanguage
     (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  fill_item := heap_lang.fill_item;
-  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
+  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
 |}.
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
-  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
-  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
-  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
+  heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
+  heap_lang.head_ctx_step_val.
 
 Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
 

heap_lang/lifting.v

@@ -23,13 +23,12 @@ Lemma wp_bindi {E e} Ki Φ :
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ e v Φ :
-  to_val e = Some v →
+Lemma wp_alloc_pst E σ v Φ :
   ▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
-  ⊢ WP Alloc e @ E {{ Φ }}.
+  ⊢ WP Alloc (of_val v) @ E {{ Φ }}.
 Proof.
-  iIntros (?)  "[HP HΦ]".
-  iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
+  iIntros "[HP HΦ]".
+  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto with fsaV.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
   subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
@@ -40,36 +39,37 @@ Lemma wp_load_pst E σ l v Φ :
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
-    last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
+    last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
 Qed.
 
-Lemma wp_store_pst E σ l e v v' Φ :
-  to_val e = Some v → σ !! l = Some v' →
+Lemma wp_store_pst E σ l v v' Φ :
+  σ !! l = Some v' →
   ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
-  ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
 Proof.
-  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
-    ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
+  intros ?.
+  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
+    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
-Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
+Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
+  σ !! l = Some v' → v' ≠ v1 →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
-  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
-    ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; by eauto 10.
+  intros ??.
+  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
+    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
-Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
+Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
+  σ !! l = Some v1 →
   ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
-  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
-    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; by eauto 10.
+  intros ?. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
+    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto).
+  solve_atomic.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)

heap_lang/tactics.v

@@ -183,10 +183,20 @@ Definition atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → heap_lang.atomic (to_expr e).
+Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
 Proof.
-  destruct e; simpl; repeat (case_match; try done);
-    naive_solver eauto using to_val_is_Some.
+  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 [|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;
+    destruct Ki; inversion Hfill; subst; clear Hfill;
+    try naive_solver eauto using to_val_is_Some.
+    move=> _ /=; destruct decide as [|Nclosed]; [by eauto | by destruct Nclosed].
 Qed.
 End W.
 
@@ -213,16 +223,11 @@ Ltac solve_to_val :=
   end.
 
 Ltac solve_atomic :=
-  try match goal with
-  | |- context E [language.atomic ?e] =>
-     let X := context E [atomic e] in change X
-  end;
   match goal with
-  | |- 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 (atomic _) => solve_atomic : fsaV.
 Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
 
 (** Substitution *)

prelude/base.v

@@ -590,7 +590,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.
 
 Class Difference A := difference: A → A → A.
 Instance: Params (@difference) 2.
-Infix "∖" := difference (at level 40) : C_scope.
+Infix "∖" := difference (at level 40, left associativity) : C_scope.
 Notation "(∖)" := difference (only parsing) : C_scope.
 Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
 Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.

program_logic/ectx_language.v

@@ -11,7 +11,6 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
@@ -34,16 +33,6 @@ Class EctxLanguage (expr val ectx state : Type) := {
     to_val e1 = None →
     head_step e1' σ1 e2 σ2 ef →
     exists K'', K' = comp_ectx K K'';
-
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    head_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2);
-  atomic_fill e K :
-    atomic (fill K e) →
-    to_val e = None →
-    K = empty_ectx;
 }.
 
 Arguments of_val {_ _ _ _ _} _.
@@ -51,7 +40,6 @@ Arguments to_val {_ _ _ _ _} _.
 Arguments empty_ectx {_ _ _ _ _}.
 Arguments comp_ectx {_ _ _ _ _} _ _.
 Arguments fill {_ _ _ _ _} _ _.
-Arguments atomic {_ _ _ _ _} _.
 Arguments head_step {_ _ _ _ _} _ _ _ _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
@@ -62,9 +50,6 @@ Arguments fill_comp {_ _ _ _ _} _ _ _.
 Arguments fill_not_val {_ _ _ _ _} _ _ _.
 Arguments ectx_positive {_ _ _ _ _} _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
-Arguments atomic_not_val {_ _ _ _ _} _ _.
-Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments atomic_fill {_ _ _ _ _} _ _ _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
@@ -84,23 +69,12 @@ 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_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;
-    language.atomic := atomic;
     language.prim_step := prim_step;
     language.to_of_val := to_of_val; language.of_to_val := of_to_val;
     language.val_stuck := val_prim_stuck;
-    language.atomic_not_val := atomic_not_val;
-    language.atomic_step := atomic_prim_step
   |}.
 
   (* Some lemmas about this language *)
@@ -111,6 +85,16 @@ 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 :
+    (∀ σ 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_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 :
     head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 ef →
     head_step e1 σ1 e2 σ2 ef.

program_logic/ectxi_language.v

@@ -9,7 +9,6 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  atomic : expr → Prop;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
@@ -24,20 +23,11 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
 
   head_ctx_step_val Ki e σ1 e2 σ2 ef :
     head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e);
-
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    head_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2);
-  atomic_fill_item e Ki :
-    atomic (fill_item Ki e) → is_Some (to_val e)
 }.
 
 Arguments of_val {_ _ _ _ _} _.
 Arguments to_val {_ _ _ _ _} _.
 Arguments fill_item {_ _ _ _ _} _ _.
-Arguments atomic {_ _ _ _ _} _.
 Arguments head_step {_ _ _ _ _} _ _ _ _ _.
 
 Arguments to_of_val {_ _ _ _ _} _.
@@ -47,9 +37,6 @@ Arguments fill_item_val {_ _ _ _ _} _ _ _.
 Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
 Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
-Arguments atomic_not_val {_ _ _ _ _} _ _.
-Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments atomic_fill_item {_ _ _ _ _} _ _ _.
 
 Section ectxi_language.
   Context {expr val ectx_item state}
@@ -70,12 +57,6 @@ Section ectxi_language.
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
 
-  Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
-  Proof.
-    destruct K as [|Ki K]; [done|].
-    rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
-  Qed.
-
   (* When something does a step, and another decomposition of the same expression
   has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
   other words, [e] also contains the reducible expression *)
@@ -95,10 +76,9 @@ Section ectxi_language.
   Global Program Instance : EctxLanguage expr val ectx state :=
     (* For some reason, Coq always rejects the record syntax claiming I
        fixed fields of different records, even when I did not. *)
-    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill atomic head_step _ _ _ _ _ _ _ _ _ _ _ _.
+    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill head_step _ _ _ _ _ _ _ _ _.
   Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
-    atomic_not_val, atomic_step, fill_not_val, atomic_fill,
-    step_by_val, fold_right_app, app_eq_nil.
+    fill_not_val, step_by_val, fold_right_app, app_eq_nil.
 
   Global Instance ectxi_lang_ctx_item Ki :
     LanguageCtx (ectx_lang expr) (fill_item Ki).

program_logic/hoare_lifting.v

@@ -49,12 +49,12 @@ Proof.
   iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I
            (λ e2 σ2 ef, ownP σ2 ★ ■ (is_Some (to_val e2) ∧ prim_step e1 σ1 e2 σ2 ef))%I
            (λ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ P)%I);
-    try by (eauto using atomic_not_val).
+    try by (eauto using reducible_not_val).
   repeat iSplit.
   - iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro.
-    iSplit. by eauto using atomic_step. iFrame. by auto.
+    iSplit. by eauto. iFrame. by auto.
   - iIntros (? e2 σ2 ef) "! (%&Hown&HP&%)". iPvsIntro. subst.
-    iFrame. iSplit; iPureIntro; auto. split; eauto using atomic_step.
+    iFrame. iSplit; iPureIntro; auto. split; eauto.
   - iIntros (e2 σ2 ef) "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
     iApply wp_value'. iExists σ2, ef. by iSplit.
   - done.

program_logic/language.v

@@ -6,26 +6,17 @@ Structure language := Language {
   state : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  atomic : expr → Prop;
   prim_step : expr → state → expr → state → option expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
-  atomic_not_val e : atomic e → to_val e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    prim_step e1 σ1 e2 σ2 ef →
-    is_Some (to_val e2)
+  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None
 }.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
-Arguments atomic {_} _.
 Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
 Arguments val_stuck {_} _ _ _ _ _ _.
-Arguments atomic_not_val {_} _ _.
-Arguments atomic_step {_} _