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

CHANGELOG.md

 In this changelog, we document "large-ish" changes to Iris that affect even the
 way the logic is used on paper.  We also mention some significant changes in the
 Coq development, but not every API-breaking change is listed.  Changes marked
-[#] still need to be ported to the Iris Documentation LaTeX file.
+[#] still need to be ported to the Iris Documentation LaTeX file(s).
+
+## Iris 3.0
+
+* [#] View shifts are radically simplified to just internalize frame-preserving
+  updates.  Weakestpre is defined inside the logic, and invariants and view
+  shifts with masks are also coded up inside Iris.
+* [#] The language can now fork off multiple threads at once.
 
 ## Iris 2.0
 

_CoqProject

@@ -76,7 +76,6 @@ program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
-program_logic/global_functor.v
 program_logic/saved_prop.v
 program_logic/auth.v
 program_logic/sts.v
@@ -110,6 +109,7 @@ tests/proofmode.v
 tests/barrier_client.v
 tests/list_reverse.v
 tests/tree_sum.v
+tests/counter.v
 proofmode/coq_tactics.v
 proofmode/pviewshifts.v
 proofmode/environments.v

algebra/cofe_solver.v

@@ -106,17 +106,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
 Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
   coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
 Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
-Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
+Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
 Proof.
-  assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1.
+  intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
   induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
     [by rewrite coerce_id|by rewrite g_coerce IH].
 Qed.
-Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
+Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
   coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
 Proof.
-  assert (i = i1 + i2) by lia; simplify_eq/=.
+  intros ? <- x. assert (i = i1 + i2) as -> by lia.
   induction i1 as [|i1 IH]; simplify_eq/=;
     [by rewrite coerce_id|by rewrite coerce_f IH].
 Qed.

algebra/list.v

@@ -81,13 +81,16 @@ End cofe.
 Arguments listC : clear implicits.
 
 (** Functor *)
+Lemma list_fmap_ext_ne {A} {B : cofeT} (f g : A → B) (l : list A) n :
+  (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
+Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
 Instance list_fmap_ne {A B : cofeT} (f : A → B) n:
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
-Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. 
+Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
   CofeMor (fmap f : listC A → listC B).
 Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
-Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
+Proof. intros f g ? l. by apply list_fmap_ext_ne. Qed.
 
 Program Definition listCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := listC (cFunctor_car F A B);

algebra/upred.v

@@ -328,13 +328,6 @@ Arguments uPred_always_if _ !_ _/.
 Notation "□? p P" := (uPred_always_if p P)
   (at level 20, p at level 0, P at level 20, format "□? p  P").
 
-Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
-  Nat.iter n uPred_later P.
-Instance: Params (@uPred_laterN) 2.
-Notation "▷^ n P" := (uPred_laterN n P)
-  (at level 20, n at level 9, right associativity,
-   format "▷^ n  P") : uPred_scope.
-
 Definition uPred_now_True {M} (P : uPred M) : uPred M := ▷ False ∨ P.
 Notation "◇ P" := (uPred_now_True P)
   (at level 20, right associativity) : uPred_scope.
@@ -987,8 +980,6 @@ Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ★ P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ★ □ Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
-Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
 
 (* Conditional always *)
 Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
@@ -1071,60 +1062,6 @@ Proof. apply wand_intro_r;rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
-(* n-times later *)
-Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
-Proof. induction m; simpl. by intros ???. solve_proper. Qed.
-Global Instance laterN_proper m :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _.
-
-Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
-Proof. done. Qed.
-Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
-Proof. induction n; simpl; auto. Qed.
-Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
-Proof. induction n1; simpl; auto. Qed.
-Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
-Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
-
-Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
-Proof. induction n; simpl; auto. Qed.
-Lemma laterN_intro n P : P ⊢ ▷^n P.
-Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
-Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
-Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
-Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
-Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
-Lemma laterN_exist_1 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ (▷^n ∃ a, Φ a).
-Proof. induction n as [|n IH]; simpl; rewrite ?later_exist_1; auto. Qed.
-Lemma laterN_exist_2 `{Inhabited A} n (Φ : A → uPred M) :
-  (▷^n ∃ a, Φ a) ⊢ ∃ a, ▷^n Φ a.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_exist_2; auto. Qed.
-Lemma laterN_sep n P Q : ▷^n (P ★ Q) ⊣⊢ ▷^n P ★ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.
-
-Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@uPred_laterN M n).
-Proof. intros P Q; apply laterN_mono. Qed.
-Global Instance laterN_flip_mono' n :
-  Proper (flip (⊢) ==> flip (⊢)) (@uPred_laterN M n).
-Proof. intros P Q; apply laterN_mono. Qed.
-Lemma laterN_True n : ▷^n True ⊣⊢ True.
-Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed.
-Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
-Proof.
-  apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
-Qed.
-Lemma laterN_exist n `{Inhabited A} (Φ : A → uPred M) :
-  ▷^n (∃ a, Φ a) ⊣⊢ (∃ a, ▷^n Φ a).
-Proof. apply: anti_symm; eauto using laterN_exist_2, laterN_exist_1. Qed.
-Lemma laterN_wand n P Q : ▷^n (P -★ Q) ⊢ ▷^n P -★ ▷^n Q.
-Proof.
-  apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
-Qed.
-Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
-Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
-
 (* True now *)
 Global Instance now_True_ne n : Proper (dist n ==> dist n) (@uPred_now_True M).
 Proof. solve_proper. Qed.
@@ -1244,7 +1181,7 @@ Proof.
   exists (y ⋅ x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma now_True_rvs P : ◇ (|=r=> ◇ P) ⊢ (|=r=> ◇ P).
+Lemma now_True_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
 Proof.
   rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
   by rewrite -rvs_intro -or_intro_l.
@@ -1390,8 +1327,6 @@ Global Instance valid_persistent {A : cmraT} (a : A) :
 Proof. by intros; rewrite /PersistentP always_valid. Qed.
 Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
-Proof. induction n; apply _. Qed.
 Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
@@ -1427,14 +1362,8 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
-Lemma soundness_laterN n : ¬(True ⊢ ▷^n False).
-Proof.
-  intros H. apply (adequacy False n). rewrite H {H}.
-  induction n as [|n IH]; rewrite /= ?IH; auto using rvs_intro.
-Qed.
-
 Theorem soundness : ¬ (True ⊢ False).
-Proof. exact (soundness_laterN 0). Qed.
+Proof. exact (adequacy False 0). Qed.
 End uPred_logic.
 
 (* Hint DB for the logic *)

heap_lang/adequacy.v

@@ -4,7 +4,7 @@ From iris.program_logic Require Import auth ownership.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics weakestpre.
 
-Definition heapGF : gFunctorList := [authGF heapUR; irisGF heap_lang].
+Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
 
 Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ :
   (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■ φ v }}) →

heap_lang/lang.v

@@ -225,53 +225,53 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Inductive head_step : expr → state → expr → state → option (expr) → Prop :=
+Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
   | BetaS f x e1 e2 v2 e' σ :
      to_val e2 = Some v2 →
      Closed (f :b: x :b: []) e1 →
      e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
-     head_step (App (Rec f x e1) e2) σ e' σ None
+     head_step (App (Rec f x e1) e2) σ e' σ []
   | UnOpS op l l' σ :
      un_op_eval op l = Some l' → 
-     head_step (UnOp op (Lit l)) σ (Lit l') σ None
+     head_step (UnOp op (Lit l)) σ (Lit l') σ []
   | BinOpS op l1 l2 l' σ :
      bin_op_eval op l1 l2 = Some l' → 
-     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
+     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ []
   | IfTrueS e1 e2 σ :
-     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
+     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
   | IfFalseS e1 e2 σ :
-     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
+     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
   | FstS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Fst (Pair e1 e2)) σ e1 σ None
+     head_step (Fst (Pair e1 e2)) σ e1 σ []
   | SndS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Snd (Pair e1 e2)) σ e2 σ None
+     head_step (Snd (Pair e1 e2)) σ e2 σ []
   | CaseLS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
+     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
   | CaseRS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
+     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
   | ForkS e σ:
-     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
+     head_step (Fork e) σ (Lit LitUnit) σ [e]
   | AllocS e v σ l :
      to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
+     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
   | LoadS l v σ :
      σ !! l = Some v →
-     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
+     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
+     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) [].
 
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -294,11 +294,11 @@ Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
 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.
+Lemma val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
 Proof. destruct 1; naive_solver. 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).
+Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
+  head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -313,7 +313,7 @@ Qed.
 
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
-  to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
+  to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
 (** Closed expressions *)

heap_lang/lib/barrier/proof.v

@@ -14,10 +14,10 @@ Class barrierG Σ := BarrierG {
   barrier_savedPropG :> savedPropG Σ idCF;
 }.
 (** The Functors we need. *)
-Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF idCF].
+Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
 (* Show and register that they match. *)
-Instance inGF_barrierG `{H : inGFs Σ barrierGF} : barrierG Σ.
-Proof. destruct H as (?&?&?). split; apply _. Qed.
+Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
+Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.

heap_lang/lib/counter.v

@@ -14,9 +14,10 @@ Global Opaque newcounter inc get.
 
 (** The CMRA we need. *)
 Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
-Definition counterGF : gFunctorList := [authGF mnatUR].
-Instance inGF_counterG `{H : inGFs Σ counterGF} : counterG Σ.
-Proof. destruct H; split; apply _. Qed.
+
+Definition counterΣ : gFunctors := #[authΣ mnatUR].
+Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
+Proof. intros [? _]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Σ, !counterG Σ} (N : namespace).

heap_lang/lib/lock.v

@@ -14,9 +14,10 @@ Global Opaque newlock acquire release.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
-Instance inGF_lockG `{H : inGFs Σ lockGF} : lockG Σ.
-Proof. destruct H. split. apply: inGF_inG. Qed.
+
+Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Σ, !lockG Σ} (N : namespace).

heap_lang/lib/spawn.v

@@ -19,11 +19,11 @@ Global Opaque spawn join.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
-(** The functor we need. *)
-Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
-(* Show and register that they match. *)
-Instance inGF_spawnG `{H : inGFs Σ spawnGF} : spawnG Σ.
-Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
+
+(** The functor we need and register that they match. *)
+Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.

heap_lang/lib/ticket_lock.v

@@ -36,10 +36,10 @@ Class tlockG Σ := TlockG {
    tlock_exclG  :> inG Σ (exclR unitC)
 }.
 
-Definition tlockGF : gFunctorList :=
-  [authGF (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
-Instance inGF_tlockG `{H : inGFs Σ tlockGF} : tlockG Σ.
-Proof. destruct H as (? & ? & ?). split. apply _. apply: inGF_inG. Qed.
+Definition tlockΣ : gFunctors :=
+  #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
+Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
+Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Σ, !tlockG Σ} (N : namespace).

heap_lang/lifting.v

@@ -10,7 +10,7 @@ Section lifting.
 Context `{irisG heap_lang Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
-Implicit Types ef : option expr.
+Implicit Types efs : list expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
@@ -38,7 +38,7 @@ Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
+  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ []) ?right_id //;
     last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
 Qed.
 
@@ -48,7 +48,7 @@ Lemma wp_store_pst E σ l v v' Φ :
   ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
 Proof.
   intros ?.
-  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
+  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) [])
     ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
@@ -58,7 +58,7 @@ Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
   ⊢ 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)
+  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ [])
     ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
@@ -68,7 +68,7 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
   ⊢ 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).
+    (<[l:=v2]>σ) []) ?right_id //; last (by intros; inv_head_step; eauto).
   solve_atomic.
 Qed.
 
@@ -76,9 +76,9 @@ Qed.
 Lemma wp_fork E e Φ :
   ▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
+  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=;
     last by intros; inv_head_step; eauto.
-  rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
+  by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
 Qed.
 
 Lemma wp_rec E f x erec e1 e2 Φ :
@@ -88,7 +88,7 @@ Lemma wp_rec E f x erec e1 e2 Φ :
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
   intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
-    (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
+    (subst' x e2 (subst' f (Rec f x erec) erec)) []) //= ?right_id;
     intros; inv_head_step; eauto.
 Qed.
 
@@ -96,7 +96,7 @@ Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
   ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
+  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -104,21 +104,21 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
   ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
-  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
+  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Φ :
   ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 [])
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Φ :
   ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 [])
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
@@ -126,7 +126,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
   to_val e1 = Some v1 → is_Some (to_val e2) →
   ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
+  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -134,7 +134,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
   is_Some (to_val e1) → to_val e2 = Some v2 →
   ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
+  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -143,7 +143,7 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
   intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
-    (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
+    (App e1 e0) []) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_case_inr E e0 e1 e2 Φ :
@@ -151,6 +151,6 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
   intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
-    (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
+    (App e2 e0) []) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 End lifting.

heap_lang/tactics.v

@@ -312,7 +312,7 @@ Tactic Notation "do_head_step" tactic3(tac) :=
   try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;
   match goal with
-  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?efs =>
      first [apply alloc_fresh|econstructor];
        (* solve [to_val] side-conditions *)
        first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]

heap_lang/wp_tactics.v

-From iris.algebra Require Export upred_tactics.
 From iris.heap_lang Require Export tactics derived.