phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/updates.v *)
Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P.
Proof.
    intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
  Qed.
(* iris/bi/updates.v *)
(* How to apply an arbitrary mask-changing view shift when having
      an arbitrary mask. *)
Lemma fupd_mask_frame E E' E1 E2 P :
    E1 ⊆ E →
    (|={E1,E2}=> |={E2 ∪ (E ∖ E1),E'}=> P) ⊢ (|={E,E'}=> P).
Proof.
    intros ?. rewrite (fupd_mask_frame_r _ _ (E ∖ E1)); last set_solver.
    rewrite fupd_trans.
    by replace (E1 ∪ E ∖ E1) with E by (by apply union_difference_L).
  Qed.
(* iris/bi/updates.v *)
(* A variant of [fupd_mask_frame] that works well for accessors: Tailored to
     eliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to
     transform the closing view shift instead of letting you prove the same
     side-conditions twice. *)
Lemma fupd_mask_frame_acc E E' E1(*Eo*) E2(*Em*) P Q :
    E1 ⊆ E →
    (|={E1,E1∖E2}=> Q) -∗
    (Q -∗ |={E∖E2,E'}=> (∀ R, (|={E1∖E2,E1}=> R) -∗ |={E∖E2,E}=> R) -∗  P) -∗
    (|={E,E'}=> P).
Proof.
    intros HE. apply entails_wand, wand_intro_r. rewrite fupd_frame_r.
    rewrite wand_elim_r. clear Q.
    rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.
    (* The most horrible way to apply fupd_intro_mask *)
    rewrite -[X in (X ⊢ _)](right_id emp%I).
    rewrite (fupd_mask_intro_subseteq (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp); last first.
    { rewrite {1}(union_difference_L _ _ HE). set_solver. }
    rewrite fupd_frame_l fupd_frame_r. apply fupd_elim.
    apply fupd_mono.
    eapply wand_apply;
      last (apply sep_mono; first reflexivity); first reflexivity.
    apply forall_intro=>R. apply wand_intro_r.
    rewrite fupd_frame_r. apply fupd_elim. rewrite left_id.
    rewrite (fupd_mask_frame_r _ _ (E ∖ E1)); last set_solver+.
    rewrite {4}(union_difference_L _ _ HE). done.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_mask_subseteq_emptyset_difference E1 E2 :
    E2 ⊆ E1 →
    ⊢@{PROP} |={E1, E2}=> |={∅, E1∖E2}=> emp.
Proof.
    intros ?. rewrite [in fupd E1](union_difference_L E2 E1); [|done].
    rewrite (comm_L (∪))
      -[X in fupd _ X](left_id_L ∅ (∪) E2) -fupd_mask_frame_r; [|set_solver+].
    apply fupd_mask_intro_subseteq; set_solver.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_or E1 E2 P Q :
    (|={E1,E2}=> P) ∨ (|={E1,E2}=> Q) ⊢@{PROP}
    (|={E1,E2}=> (P ∨ Q)).
Proof. apply or_elim; apply fupd_mono; [ apply or_intro_l | apply or_intro_r ]. Qed.
(* iris/bi/updates.v *)
Instance fupd_or_homomorphism E :
    MonoidHomomorphism bi_or bi_or (flip (⊢)) (fupd (PROP:=PROP) E E).
Proof. split; [split|]; try apply _; [apply fupd_or | apply fupd_intro]. Qed.
(* iris/bi/updates.v *)
Lemma fupd_and E1 E2 P Q :
    (|={E1,E2}=> (P ∧ Q)) ⊢@{PROP} (|={E1,E2}=> P) ∧ (|={E1,E2}=> Q).
Proof. apply and_intro; apply fupd_mono; [apply and_elim_l | apply and_elim_r]. Qed.
(* iris/bi/updates.v *)
Lemma fupd_exist E1 E2 A (Φ : A → PROP) :
    (∃ x : A, |={E1, E2}=> Φ x) ⊢ |={E1, E2}=> ∃ x : A, Φ x.
Proof. apply exist_elim=> a. by rewrite -(exist_intro a). Qed.
(* iris/bi/updates.v *)
Lemma fupd_forall E1 E2 A (Φ : A → PROP) :
    (|={E1, E2}=> ∀ x : A, Φ x) ⊢ ∀ x : A, |={E1, E2}=> Φ x.
Proof. apply forall_intro=> a. by rewrite -(forall_elim a). Qed.
(* iris/bi/updates.v *)
Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ⊢ |={E}=> P ∗ Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
(* iris/bi/updates.v *)
Instance fupd_sep_homomorphism E :
    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (fupd (PROP:=PROP) E E).
Proof. split; [split|]; try apply _; [apply fupd_sep | apply fupd_intro]. Qed.
(* iris/bi/updates.v *)
Lemma big_sepL_fupd {A} E (Φ : nat → A → PROP) l :
    ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ⊢ |={E}=> [∗ list] k↦x ∈ l, Φ k x.
Proof. by rewrite (big_opL_commute _). Qed.
(* iris/bi/updates.v *)
Lemma big_sepL2_fupd {A B} E (Φ : nat → A → B → PROP) l1 l2 :
    ([∗ list] k↦x;y ∈ l1;l2, |={E}=> Φ k x y) ⊢ |={E}=> [∗ list] k↦x;y ∈ l1;l2, Φ k x y.
Proof.
    rewrite !big_sepL2_alt !persistent_and_affinely_sep_l.
    etrans; [| by apply fupd_frame_l]. apply sep_mono_r. apply big_sepL_fupd.
  Qed.
(* iris/bi/updates.v *)
Lemma big_sepM_fupd `{Countable K} {A} E (Φ : K → A → PROP) m :
    ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ⊢ |={E}=> [∗ map] k↦x ∈ m, Φ k x.
Proof. by rewrite (big_opM_commute _). Qed.
(* iris/bi/updates.v *)
Lemma big_sepM2_fupd `{Countable K} {A B} E (Φ : K → A → B → PROP) m m' :
    ([∗ map] k↦x;y ∈ m;m', |={E}=> Φ k x y) ⊢ |={E}=> [∗ map] k↦x;y ∈ m;m', Φ k x y.
Proof.
    rewrite !big_sepM2_alt big_sepM_fupd.
    rewrite !persistent_and_affinely_sep_l fupd_frame_l //.
  Qed.
(* iris/bi/updates.v *)
Lemma big_sepS_fupd `{Countable A} E (Φ : A → PROP) X :
    ([∗ set] x ∈ X, |={E}=> Φ x) ⊢ |={E}=> [∗ set] x ∈ X, Φ x.
Proof. by rewrite (big_opS_commute _). Qed.
(* iris/bi/updates.v *)
Lemma big_sepMS_fupd `{Countable A} E (Φ : A → PROP) l :
    ([∗ mset] x ∈ l, |={E}=> Φ x) ⊢ |={E}=> [∗ mset] x ∈ l, Φ x.
Proof. by rewrite (big_opMS_commute _). Qed.
(* iris/bi/updates.v *)
(* Fancy updates that take a step derived rules. *)
Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]▷=> P) -∗ (P -∗ Q) -∗ |={Eo}[Ei]▷=> Q.
Proof.
    apply entails_wand, wand_intro_l.
    by rewrite (later_intro (P -∗ Q)) fupd_frame_l -later_sep fupd_frame_l
               wand_elim_l.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_mask_frame_r Eo Ei Ef P :
    Eo ## Ef → Ei ## Ef → (|={Eo}[Ei]▷=> P) ⊢ |={Eo ∪ Ef}[Ei ∪ Ef]▷=> P.
Proof.
    intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_mask_mono Eo1 Eo2 Ei1 Ei2 P :
    Ei2 ⊆ Ei1 → Eo1 ⊆ Eo2 → (|={Eo1}[Ei1]▷=> P) ⊢ |={Eo2}[Ei2]▷=> P.
Proof.
    intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]▷=> P)%I).
    rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp) //.
    rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
    rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)) //.
    rewrite fupd_frame_r. f_equiv.
    rewrite [X in (X ∗ _)%I]later_intro -later_sep. f_equiv.
    rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans Ei1 Eo1 Eo2). f_equiv.
    by rewrite fupd_frame_r left_id.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_intro Ei Eo P : Ei ⊆ Eo → ▷ P ⊢ |={Eo}[Ei]▷=> P.
Proof. intros. by rewrite -(step_fupd_mask_mono Ei _ Ei _) // -!fupd_intro. Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_frame_l Eo Ei R Q :
    (R ∗ |={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> (R ∗ Q).
Proof.
    rewrite fupd_frame_l.
    apply fupd_mono.
    rewrite [P in P ∗ _ ⊢ _](later_intro R) -later_sep fupd_frame_l.
    by apply later_mono, fupd_mono.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_fupd Eo Ei P : (|={Eo}[Ei]▷=> P) ⊣⊢ (|={Eo}[Ei]▷=> |={Eo}=> P).
Proof.
    apply (anti_symm (⊢)).
    - by rewrite -fupd_intro.
    - by rewrite fupd_trans.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_mono Eo Ei n P Q :
    (P ⊢ Q) → (|={Eo}[Ei]▷=>^n P) ⊢ (|={Eo}[Ei]▷=>^n Q).
Proof.
    intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_wand Eo Ei n P Q :
    (|={Eo}[Ei]▷=>^n P) -∗ (P -∗ Q) -∗ (|={Eo}[Ei]▷=>^n Q).
Proof.
    apply entails_wand, wand_intro_l. induction n as [|n IH]=> /=.
    { by rewrite wand_elim_l. }
    rewrite -IH -fupd_frame_l later_sep -fupd_frame_l.
    by apply sep_mono; first apply later_intro.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_intro Ei Eo n P : Ei ⊆ Eo → ▷^n P ⊢ |={Eo}[Ei]▷=>^n P.
Proof.
    induction n as [|n IH]=> ?; [done|].
    rewrite /= -step_fupd_intro; [|done]. by rewrite IH.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_S_fupd n E P :
    (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
Proof.
    apply (anti_symm (⊢)); rewrite !Nat.iter_succ_r; apply step_fupdN_mono;
      rewrite -step_fupd_fupd //.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_frame_l Eo Ei n R Q :
    (R ∗ |={Eo}[Ei]▷=>^n Q) ⊢ |={Eo}[Ei]▷=>^n (R ∗ Q).
Proof.
    induction n as [|n IH]; simpl; [done|].
    rewrite step_fupd_frame_l IH //=.
  Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_add n m Eo Ei P :
    (|={Eo}[Ei]▷=>^(n+m) P) ⊣⊢ (|={Eo}[Ei]▷=>^n |={Eo}[Ei]▷=>^m P).
Proof.
    induction n as [ | n IH]; simpl; [done | by rewrite IH].
  Qed.
(* iris/bi/updates.v *)
(* The sidecondition [Ei ⊆ Eo] is needed because for [n = 0],
    this lemma introduces updates in the same way as [step_fupdN_intro]
    (in fact, for [n = 0] it is essentially [step_fupdN_intro], modulo laters). *)
Lemma step_fupdN_le n m Eo Ei P :
    n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^n P) ⊢ (|={Eo}[Ei]▷=>^m P).
Proof.
    intros ??. replace m with ((m - n) + n) by lia.
    rewrite step_fupdN_add.
    rewrite -(step_fupdN_intro _ _ (m - n)); last done.
    by rewrite -laterN_intro.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_keep_si_pure {E1 E2} E2' Pi R :
      (|={E1,E2'}=> <si_pure> Pi) ∧ (<si_pure> Pi ={E1,E2}=∗ R) ⊢ |={E1,E2}=> R.
Proof.
      rewrite -{2}(fupd_trans E1 E1 E2) -(fupd_keep_si_pure' E2' Pi).
      by rewrite -fupd_intro.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_keep_plainly {E1 E2} E2' P R :
      (|={E1,E2'}=> ■ P) ∧ (P ={E1,E2}=∗ R) ⊢ |={E1,E2}=> R.
Proof.
      rewrite -{2}(fupd_keep_si_pure E2' (<si_emp_valid> P) R).
      by rewrite {2}si_pure_si_emp_valid_elim.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plainly_later E P : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P.
Proof.
      by rewrite /plainly fupd_si_pure_later si_pure_si_emp_valid_elim.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
      (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x.
Proof.
      rewrite /plainly fupd_si_pure_forall_2.
      by setoid_rewrite si_pure_si_emp_valid_elim; last apply _.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plainly_mask E E' P : (|={E,E'}=> ■ P) ⊢ |={E}=> P.
Proof.
      etrans; [|apply (fupd_keep_plainly E' P)]. apply and_intro; [done|].
      apply wand_intro_l. by rewrite sep_elim_l -fupd_intro.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plainly_laterN E n P : (▷^n |={E}=> ■ P) ⊢ |={E}=> ▷^n ◇ P.
Proof.
      revert P. induction n as [|n IH]=> P /=.
      { by rewrite -except_0_intro plainly_elim. }
      rewrite -!later_laterN !laterN_later.
      rewrite -plainly_idemp fupd_plainly_later.
      by rewrite except_0_plainly_1 later_plainly_1 IH except_0_later.
    Qed.
(* iris/bi/updates.v *)
(* Laws for general plain propositions. *)
Lemma fupd_keep_plain {E1 E2} E2' P `{!Plain P} R :
      (|={E1,E2'}=> P) ∧ (P ={E1,E2}=∗ R) ⊢ |={E1,E2}=> R.
Proof. by rewrite -{1}(plain_plainly P) fupd_keep_plainly. Qed.
(* iris/bi/updates.v *)
Lemma fupd_plain_mask E E' P `{!Plain P} : (|={E,E'}=> P) ⊢ |={E}=> P.
Proof. by rewrite {1}(plain P) fupd_plainly_mask. Qed.
(* iris/bi/updates.v *)
(* This is an alternative version of [fupd_keep_plain] that might look more
    intuitive, but is more annoying to use: we can eliminate a [fupd] that
    "consumes" [R] to produce some plain [P] without actually using up [R]. *)
Lemma fupd_keep_plain_sep {E} E' P `{!Plain P} R :
      (R ={E,E'}=∗ P) -∗ R -∗ |={E}=> P ∗ R.
Proof.
      apply entails_wand, wand_intro_r.
      etrans; [|apply (fupd_keep_plain E' P)]. apply and_intro.
      - by rewrite wand_elim_l.
      - rewrite sep_elim_r -fupd_intro. by apply wand_intro_l.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plain_later E P `{!Plain P} : (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
Proof. by rewrite {1}(plain P) fupd_plainly_later. Qed.
(* iris/bi/updates.v *)
Lemma fupd_plain_laterN E n P `{!Plain P} : (▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
Proof. by rewrite {1}(plain P) fupd_plainly_laterN. Qed.
(* iris/bi/updates.v *)
Lemma fupd_plain_forall_2 E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      (∀ x, |={E}=> Φ x) ⊢ |={E}=> ∀ x, Φ x.
Proof.
      rewrite -fupd_plainly_forall_2. apply forall_mono=> x.
      by rewrite {1}(plain (Φ _)).
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      E2 ⊆ E1 →
      (|={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}=> Φ x).
Proof.
      intros. apply (anti_symm _); first apply fupd_forall.
      trans (∀ x, |={E1}=> Φ x)%I.
      { apply forall_mono=> x. by rewrite fupd_plain_mask. }
      rewrite fupd_plain_forall_2. apply fupd_elim.
      rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_intro_discard E1 E2 (■ _)) //.
      by rewrite plainly_elim.
    Qed.
(* iris/bi/updates.v *)
Lemma fupd_plain_forall' E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      (|={E}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E}=> Φ x).
Proof. by apply fupd_plain_forall. Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]▷=> P) ⊢ |={Eo}=> ▷ ◇ P.
Proof.
      rewrite -(fupd_plain_mask _ Ei (▷ ◇ P)).
      apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
    Qed.
(* iris/bi/updates.v *)
Lemma step_fupdN_plain Eo Ei n P `{!Plain P} : (|={Eo}[Ei]▷=>^n P) ⊢ |={Eo}=> ▷^n ◇ P.
Proof.
      induction n as [|n IH].
      - by rewrite -fupd_intro -except_0_intro.
      - rewrite Nat.iter_succ step_fupd_fupd IH !fupd_trans step_fupd_plain.
        apply fupd_mono. destruct n as [|n]; simpl.
        * by rewrite except_0_idemp.
        * by rewrite except_0_later.
    Qed.
(* iris/bi/updates.v *)
Lemma step_fupd_plain_forall Eo Ei {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      Ei ⊆ Eo →
      (|={Eo}[Ei]▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={Eo}[Ei]▷=> Φ x).
Proof.
      intros. apply (anti_symm _).
      { apply forall_intro=> x. by rewrite (forall_elim x). }
      trans (∀ x, |={Eo}=> ▷ ◇ Φ x)%I.
      { apply forall_mono=> x. by rewrite step_fupd_plain. }
      rewrite -fupd_plain_forall'. apply fupd_elim.
      rewrite -(fupd_except_0 Ei Eo) -step_fupd_intro //.
      by rewrite -later_forall -except_0_forall.
    Qed.
(* iris/bi/weakestpre.v *)
Inductive stuckness
:= NotStuck | MaybeStuck.
(* iris/bi/weakestpre.v *)
Instance stuckness_le : SqSubsetEq stuckness
:= λ s1 s2,
  match s1, s2 with
  | MaybeStuck, NotStuck => False
  | _, _ => True
  end.
(* iris/bi/weakestpre.v *)
Instance stuckness_le_po : PreOrder (⊑@{stuckness}).
Proof. split; by repeat intros []. Qed.
(* iris/bi/weakestpre.v *)
(* Weakest preconditions [WP e @ s ; E {{ Φ }}] have an additional argument [s]
of arbitrary type [A], that can be chosen by the one instantiating the [Wp] type
class. This argument can be used for e.g. the stuckness bit (as in Iris) or
thread IDs (as in iGPS).

For the case of stuckness bits, there are two specific notations
[WP e @ E {{ Φ }}] and [WP e @ E ?{{ Φ }}], which forces [A] to be [stuckness],
and [s] to be [NotStuck] or [MaybeStuck].  This will fail to typecheck if [A] is
not [stuckness].  If we ever want to use the notation [WP e @ E {{ Φ }}] with a
different [A], the plan is to generalize the notation to use [Inhabited] instead
to pick a default value depending on [A]. *)
Class Wp (PROP EXPR VAL A : Type)
:=
  wp : A → coPset → EXPR → (VAL → PROP) → PROP.
(* iris/bi/weakestpre.v *)
Instance : Params (@wp) 8
:= {}.
(* iris/bi/weakestpre.v *)
Class Twp (PROP EXPR VAL A : Type)
:=
  twp : A → coPset → EXPR → (VAL → PROP) → PROP.
(* iris/bi/weakestpre.v *)
Instance : Params (@twp) 8
:= {}.
(* iris/bi/weakestpre.v *)
(* Notations without binder -- only parsing because they overlap with the
notations with binder. *)
Notation "'WP' e @ s ; E {{ Φ } }"
:= (wp s E e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E {{ Φ } }"
:= (wp NotStuck E e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E ? {{ Φ } }"
:= (wp MaybeStuck E e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e {{ Φ } }"
:= (wp NotStuck ⊤ e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e ? {{ Φ } }"
:= (wp MaybeStuck ⊤ e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
(* The general approach we use for all these complex notations: an outer '[hv'
to switch bwteen "horizontal mode" where it all fits on one line, and "vertical
mode" where each '/' becomes a line break. Then, as appropriate, nested boxes
('['...']') for things like preconditions and postconditions such that they are
maximally horizontal and suitably indented inside the parentheses that surround
them. *)
Notation "'WP' e @ s ; E {{ v , Q } }"
:= (wp s E e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E  ']' '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E {{ v , Q } }"
:= (wp NotStuck E e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' @  E  '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E ? {{ v , Q } }"
:= (wp MaybeStuck E e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' @  E  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e {{ v , Q } }"
:= (wp NotStuck ⊤ e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e ? {{ v , Q } }"
:= (wp MaybeStuck ⊤ e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ,
      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ,
      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ,
      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' ? {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ,
      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' {{{  '[' x  ..  y ,  RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ,
      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' ? {{{  '[' x  ..  y ,   RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
    (at level 20,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  '[' s ;  '/' E  ']' '/' {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
    (at level 20,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
    (at level 20,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' @  E  '/' ? {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
    (at level 20,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }"
:=
  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
    (at level 20,
     format "'[hv' {{{  '[' P  ']' } } }  '/  ' e  '/' ? {{{  '[' RET  pat ;  '/' Q  ']' } } } ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
(* Aliases for stdpp scope -- they inherit the levels and format from above. *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }"
:=
  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
(* iris/bi/weakestpre.v *)
(* Notations without binder -- only parsing because they overlap with the
notations with binder. *)
Notation "'WP' e @ s ; E [{ Φ } ]"
:= (twp s E e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E [{ Φ } ]"
:= (twp NotStuck E e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E ? [{ Φ } ]"
:= (twp MaybeStuck E e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e [{ Φ } ]"
:= (twp NotStuck ⊤ e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e ? [{ Φ } ]"
:= (twp MaybeStuck ⊤ e%E Φ)
  (at level 0, e, Φ at level 200, only parsing) : bi_scope.
(* iris/bi/weakestpre.v *)
(* Notations with binder. *)
Notation "'WP' e @ s ; E [{ v , Q } ]"
:= (twp s E e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E  ']' '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E [{ v , Q } ]"
:= (twp NotStuck E e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' @  E  '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e @ E ? [{ v , Q } ]"
:= (twp MaybeStuck E e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' @  E  '/' ? [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.
(* iris/bi/weakestpre.v *)
Notation "'WP' e [{ v , Q } ]"
:= (twp NotStuck ⊤ e%E (λ v, Q))
  (at level 0, e, Q at level 200, v at level 200 as pattern,
   format "'[hv' 'WP'  e  '/' [{  '[' v ,  '/' Q  ']' } ] ']'") : bi_scope.