phanerozoic/Coq-Iris huggingface dataset:
(* tests/heap_lang_proph.v *)
Lemma test_resolve1' E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
    l ↦ #n -∗
    proph p vs -∗
    WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
      {{ v, ⌜v = (#n, #true)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}.
Proof.
    iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
    iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
  Qed.
(* tests/heap_lang_proph.v *)
Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
    proph p vs -∗
    WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, ⌜v = #0⌝ ∗ ∃vs, proph p vs }}.
Proof.
    iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
    wp_pures. iIntros "!>" (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
  Qed.
(* tests/heap_lang_proph.v *)
Lemma test_resolve3 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
    {{{ proph p1 vs1 ∗ proph p2 vs2 }}}
      Resolve (Resolve (#n - #n) #p2 #2) #p1 #1 @ s; E
    {{{ RET #0 ; ∃ vs1' vs2', ⌜vs1 = (#0, #1)::vs1' ∧ vs2 = (#0, #2)::vs2'⌝ ∗ proph p1 vs1' ∗ proph p2 vs2' }}}.
Proof.
    iIntros (Φ) "[Hp1 Hp2] HΦ".
    wp_apply (wp_resolve with "Hp1"); first done.
    wp_apply (wp_resolve with "Hp2"); first done.
    wp_op.
    iIntros "!>" (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
    iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
  Qed.
(* tests/heap_lang_proph.v *)
Lemma test_resolve4 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
    {{{ proph p1 vs1 ∗ proph p2 vs2 }}}
      Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E
    {{{ RET #0 ; ∃ vs1' vs2', ⌜vs1 = (#0, #1)::vs1' ∧ vs2 = (#0, #2)::vs2'⌝ ∗ proph p1 vs1' ∗ proph p2 vs2' }}}.
Proof.
    iIntros (Φ) "[Hp1 Hp2] HΦ". wp_pures.
    wp_apply (wp_resolve with "Hp1"); first done.
    wp_apply (wp_resolve with "Hp2"); first done.
    wp_op.
    iIntros "!>" (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
    iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
  Qed.
(* tests/heap_lang_proph.v *)
Lemma test_resolve1_twice s E (p : proph_id) (vs : list (val * val)) :
    {{{ proph p vs }}}
      Resolve (Resolve (#1 + #2) #p #1) #p #2 @ s; E
    {{{ RET #3 ; ∃ vs', ⌜vs = (#3, #1)::(#3, #2)::vs'⌝ ∗ proph p vs' }}}.
Proof.
    iIntros (Φ) "Hp HΦ". wp_pures.
    wp_apply (wp_resolve_strong with "Hp") as "Hp"; first done.
    wp_apply (wp_resolve_strong with "Hp") as "Hp"; first done.
    wp_op.
    iIntros "!> {$Hp} %pvs'' -> $ %pvs' -> Hp".
    iApply "HΦ". by iFrame.
  Qed.
(* tests/ipm_paper.v *)
Notation iProp
:= (uPred M).
(* tests/ipm_paper.v *)
(* The version in Coq *)
Lemma and_exist A (P R: Prop) (Ψ: A → Prop) :
    P ∧ (∃ a, Ψ a) ∧ R → ∃ a, P ∧ Ψ a.
Proof.
    intros [HP [HΨ HR]].
    destruct HΨ as [x HΨ].
    exists x.
    split.
    -  assumption.
    -  assumption.
  Qed.
(* tests/ipm_paper.v *)
Lemma sep_exist A (P R: iProp) (Ψ: A → iProp) :
    P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
Proof.
    iIntros "[HP [HΨ HR]]".
    iDestruct "HΨ" as (x) "HΨ".
    iExists x. Show.
    iSplitL "HΨ".
    - Show. iAssumption.
    - Show. iAssumption.
  Qed.
(* tests/ipm_paper.v *)
Lemma sep_exist_short A (P R: iProp) (Ψ: A → iProp) :
    P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
(* tests/ipm_paper.v *)
(* An even shorter version in IPM, using the frame introduction pattern `$` *)
Lemma sep_exist_shorter A (P R: iProp) (Ψ: A → iProp) :
    P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
Proof. by iIntros "[$ [??]]". Qed.
(* tests/ipm_paper.v *)
Fixpoint is_list (hd : val) (xs : list val) : iProp
:=
    match xs with
    | [] => ⌜hd = NONEV⌝
    | x :: xs => ∃ l hd', ⌜hd = SOMEV #l⌝ ∗ l ↦ (x,hd') ∗ is_list hd' xs
    end%I.
(* tests/ipm_paper.v *)
Definition rev : val
:=
    rec: "rev" "hd" "acc" :=
      match: "hd" with
        NONE => "acc"
      | SOME "l" =>
         let: "tmp1" := Fst !"l" in
         let: "tmp2" := Snd !"l" in
         "l" <- ("tmp1", "acc");;
         "rev" "tmp2" "hd"
      end.
(* tests/ipm_paper.v *)
Lemma rev_acc_ht hd acc xs ys :
    ⊢ {{ is_list hd xs ∗ is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
Proof.
    iIntros "!> [Hxs Hys]".
    iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
    destruct xs as [|x xs]; iSimplifyEq.
    - (* nil *) by wp_match.
    - (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
      wp_match. wp_load. wp_load. wp_store.
      rewrite reverse_cons -assoc.
      iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
      iExists l, acc; by iFrame.
  Qed.
(* tests/ipm_paper.v *)
Lemma rev_ht hd xs :
    ⊢ {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
Proof.
    iIntros "!> Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
    iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
  Qed.
(* tests/ipm_paper.v *)
Definition incr : val
:=
  rec: "incr" "l" :=
    let: "n" := !"l" in
    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
(* tests/ipm_paper.v *)
(* The CMRA we need. *)
Inductive M
:= Auth : nat → M | Frag : nat → M | Bot.
(* tests/ipm_paper.v *)
Canonical M_O : ofe
:= leibnizO M.
(* tests/ipm_paper.v *)
Instance M_valid : Valid M
:= λ x, x ≠ Bot.
(* tests/ipm_paper.v *)
Instance M_op : Op M
:= λ x y,
    match x, y with
    | Auth n, Frag j | Frag j, Auth n => if decide (j ≤ n) then Auth n else Bot
    | Frag i, Frag j => Frag (max i j)
    | _, _ => Bot
    end.
(* tests/ipm_paper.v *)
Instance M_pcore : PCore M
:= λ x,
    Some match x with Auth j | Frag j => Frag j | _ => Bot end.
(* tests/ipm_paper.v *)
Instance M_unit : Unit M
:= Frag 0.
(* tests/ipm_paper.v *)
Definition M_ra_mixin : RAMixin M.
Proof.
    apply ra_total_mixin; try solve_proper || eauto.
    - intros [n1|i1|] [n2|i2|] [n3|i3|];
        repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n1|i1|] [n2|i2|]; repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n|i|]; repeat (simpl; case_decide); f_equal/=; lia.
    - by intros [n|i|].
    - intros [n1|i1|] y [[n2|i2|] ?]; exists (core y); simplify_eq/=;
        repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
  Qed.
(* tests/ipm_paper.v *)
Canonical M_R : cmra
:= discreteR M M_ra_mixin.
(* tests/ipm_paper.v *)
Instance M_discrete : CmraDiscrete M_R.
Proof. apply discrete_cmra_discrete. Qed.
(* tests/ipm_paper.v *)
Definition M_ucmra_mixin : UcmraMixin M.
Proof.
    split; try (done || apply _).
    intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
  Qed.
(* tests/ipm_paper.v *)
Canonical M_UR : ucmra
:= Ucmra M M_ucmra_mixin.
(* tests/ipm_paper.v *)
Instance frag_core_id n : CoreId (Frag n).
Proof. by constructor. Qed.
(* tests/ipm_paper.v *)
Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → j ≤ n.
Proof. simpl. case_decide; first done. by intros []. Qed.
(* tests/ipm_paper.v *)
Lemma auth_frag_op (j n : nat) : j ≤ n → Auth n = Auth n ⋅ Frag j.
Proof. intros. by rewrite /= decide_True. Qed.
(* tests/ipm_paper.v *)
Lemma M_update n : Auth n ~~> Auth (S n).
Proof.
    apply cmra_discrete_total_update=>-[m|j|] /= ?; repeat case_decide; done || lia.
  Qed.
(* tests/ipm_paper.v *)
Class counterG Σ
:= CounterG { #[local] counter_tokG :: inG Σ M_UR }.
(* tests/ipm_paper.v *)
Definition counterΣ : gFunctors
:= #[GFunctor (constRF M_UR)].
(* tests/ipm_paper.v *)
Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
(* tests/ipm_paper.v *)
Definition I (γ : gname) (l : loc) : iProp Σ
:=
    (∃ c : nat, l ↦ #c ∗ own γ (Auth c))%I.
(* tests/ipm_paper.v *)
Definition C (l : loc) (n : nat) : iProp Σ
:=
    (∃ N γ, inv N (I γ l) ∧ own γ (Frag n))%I.
(* tests/ipm_paper.v *)
(* The main proofs. *)
Instance C_persistent l n : Persistent (C l n).
Proof. apply _. Qed.
(* tests/ipm_paper.v *)
Lemma newcounter_spec :
    ⊢ {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
Proof.
    iIntros "!> _ /=". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
    iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
    rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
    set (N:= nroot .@ "counter").
    iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
    { iIntros "!>". iExists 0. by iFrame. }
    iModIntro. rewrite /C; eauto 10.
  Qed.
(* tests/ipm_paper.v *)
Lemma incr_spec l n :
    ⊢ {{ C l n }} incr #l {{ v, ⌜v = #()⌝ ∧ C l (S n) }}.
Proof.
    iIntros "!> Hl /=". iLöb as "IH". wp_rec.
    iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
    wp_bind (! _)%E. iInv "Hinv" as (c) "[Hl Hγ]".
    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    wp_let. wp_op.
    wp_bind (CmpXchg _ _ _). iInv "Hinv" as (c') ">[Hl Hγ]".
    destruct (decide (c' = c)) as [->|].
    - iCombine "Hγ" "Hγf" as "Hγ".
      iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
      iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
      rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
      wp_pures. by iFrame "#∗".
    - wp_cmpxchg_fail; first (intros [=]; abstract lia).
      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
      wp_pures. iApply "IH". iFrame "#∗".
  Qed.
(* tests/ipm_paper.v *)
Lemma read_spec l n :
    ⊢ {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
Proof.
    iIntros "!> Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
    rewrite /read /=. wp_lam. Show. iInv "Hinv" as (c) "[Hl Hγ]". wp_load. Show.
    iDestruct (own_valid γ (Auth c ⋅ Frag n) with "[-]") as %H%auth_frag_valid.
    { iApply own_op. by iFrame. }
    rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    rewrite /C; eauto 10 with lia.
  Qed.
(* tests/iprop.v *)
(* A [sigT] that is partially applied and template-polymorphic causes universe
inconsistency errors, which is why [sigT] should be avoided for the definition
of [gFunctors].

The following constructs a partially applied [sigT] that generates bad universe
constraints. This causes a universe inconsistency when [gFunctors] are
to be defined with [sigT]. *)
Definition foo
:=
  eq_dep
    ((Type -> Type) -> Type)
    (sigT (A:=Type -> Type)).
(* tests/iprop.v *)
Lemma bi_ofeO_iProp Σ : bi_ofeO (iPropI Σ) = iPropO Σ.
Proof. reflexivity. Qed.
(* tests/iprop.v *)
Lemma bi_cofe_iProp Σ : bi_cofe (iPropI Σ) = @uPred_cofe (iResUR Σ).
Proof. reflexivity. Qed.
(* tests/iris_notation.v *)
(* Test scopes for bupd *)
Definition use_bupd_uPred (n : nat) : uPred M
:=
    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
(* tests/iris_notation.v *)
Definition use_plainly_uPred (n : nat) : uPred M
:=
    ■ |==> ∃ m : nat , ⌜ n = 2 ⌝.
(* tests/iris_notation.v *)
(* Test scopes inside big-ops *)
Definition big_op_scope_uPred_1 (xs : list nat) : uPred M
:=
    [∗ list] _ ↦ x ∈ xs, True.
(* tests/iris_notation.v *)
Definition big_op_scope_uPred_2 (xs : list nat) : uPred M
:=
    [∗ list] x; y ∈ xs; xs, True.
(* tests/iris_notation.v *)
Definition big_op_scope_uPred_3 (m : gmap nat nat) : uPred M
:=
    [∗ map] _ ↦ x ∈ m, True.
(* tests/iris_notation.v *)
Definition big_op_scope_uPred_4 (m : gmap nat nat) : uPred M
:=
    [∗ map] x; y ∈ m; m, True.
(* tests/iris_notation.v *)
(* Test scopes for bupd and fupd *)
Definition use_bupd_iProp (n : nat) : iProp Σ
:=
    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
(* tests/iris_notation.v *)
Definition use_fupd_iProp (n : nat) : iProp Σ
:=
    □ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.
(* tests/iris_notation.v *)
(* Test scopes inside big-ops *)
Definition big_op_scope_iProp_1 (xs : list nat) : iProp Σ
:=
    [∗ list] _ ↦ x ∈ xs, True.
(* tests/iris_notation.v *)
Definition big_op_scope_iProp_2 (xs : list nat) : iProp Σ
:=
    [∗ list] x; y ∈ xs; xs, True.
(* tests/iris_notation.v *)
Definition big_op_scope_iProp_3 (m : gmap nat nat) : iProp Σ
:=
    [∗ map] _ ↦ x ∈ m, True.
(* tests/iris_notation.v *)
Definition big_op_scope_iProp_4 (m : gmap nat nat) : iProp Σ
:=
    [∗ map] x; y ∈ m; m, True.
(* tests/later_credits_paper.v *)
(* This is the small example from the end of Section 2 (page 9) of the paper.
  Using later credits in this example is not strictly necessary, but it
  demonstrates how they can be used. *)
Lemma mini_later_credits_example `{!heapGS Σ} N (f : val) l :
  (** Assume we have some specification for f... *)
  (∀ v, ⊢ {{{ ∃ n: nat, ⌜v = LitV n⌝}}} f v {{{ (n' : nat), RET #n'; True }}}) →
  (** ... and an invariant managing [l] *)
  inv N (∃ n : nat, l ↦ LitV n) -∗
  (** Our program stores the result of calling [f] to [l]. *)
  {{{ True }}} #l <- f (#41 + #1) {{{ v, RET v; True }}}.
Proof.
  (** We will use a later credit to strip the later we get over the
     contents of the invariant when opening it. This is not strictly
     necessary (timelessness would also work here), but it is
     nevertheless instructive. *)

  iIntros (Hs) "#Hpre". iIntros (Φ) "!> _ Hpost".
  wp_bind (_ + _)%E.
  (** We generate a later credit ["Hcred" : £ 1] from executing a pure step.
     [wp_pure credit:"Hcred"] behaves like [wp_pure] in executing a pure step,
     but additionally provides a new hypothesis ["Hcred" : £ 1].
     [£ 1] denotes ownership of the right to eliminate one later. *)
  wp_pure credit:"Hcred".

  (** We now use the specification for [f]. *)
  wp_bind (f _). iApply Hs.
  { iExists 42. done. }
  iNext. iIntros (n') "_".
  (** Now we open the invariant... *)
  iInv "Hpre" as "Hl".
  (** and get [Hl : ▷ (∃ n : nat, l ↦ #n)]. *)

  (** We can use the later credit we just obtained to eliminate the later.
     Later credits can be used to eliminate laters at fancy updates, in general
     away from a weakest precondition.
     [lc_fupd_elim_later] can be used to transform a hypothesis [▷ P] to [P]
     using one credit [£1]. *)
  iMod (lc_fupd_elim_later with "Hcred Hl") as "Hl".
  iDestruct "Hl" as "(%n & Hl)".
  (** now we can execute the store using the [l ↦ _]. *)
  wp_store. iModIntro.
  iSplitL "Hl". { eauto with iFrame. }
  by iApply "Hpost".
Qed.
(* tests/later_credits_paper.v *)
(* Now for a slightly more complicated example involving nested invariants.
  This is an instance of the example outlined in the introduction (page 4) of the paper.

  Of course, we again consider a very simple proof that might appear toyish, but with
  challenges that might well appear as part of much more complicated proof setups. *)
Lemma nested_invariants_example `{!heapGS Σ} `{!ghost_varG Σ loc} γ (l : loc) :
  (** Assume that the location [l] is managed through another indirection with a ghost variable [γ],
     a situation you might well encounter as part of more complicated proof setups.
     The ownership of the location [l] itself is kept inside a nested invariant. *)
  inv (nroot .@ "1") (∃ l : loc, inv (nroot .@ "2") (∃ n : nat, l ↦ #n) ∗ γ ↪VAR{#1/2} l) -∗
  (** One half of [γ] is kept outside the invariant to keep knowledge about the location [l].
     We also assume to get one later credit, perhaps from a preceding pure step or from a
     totally different part of the program. *)
  {{{ γ ↪VAR{#1/2} l ∗ £ 1 }}} #l <- #42 {{{ v, RET v; True }}}.
Proof.
  iIntros "#Hinv". iIntros (Φ) "!> (Hv & Hcred) Hpost".
  (** We open the outer invariant... *)
  iInv "Hinv" as "(%l' & #Hinv' & >Hv')".
  (** and use timelessness to strip the later over ["Hv'"].
     But we cannot do the same for ["Hinv'"], the knowledge about the nested invariant, because
     it is not timeless. And we also cannot take any program step to strip the later here! *)
  iCombine "Hv Hv'" gives %[_ <-].
  (** Instead, we use the later credit to strip the later in front of the invariant.
    Here we make use of [lc_fupd_add_later], which adds a later to the goal using one credit,
    if the current goal is a fancy update. *)
  iApply fupd_wp. iApply (lc_fupd_add_later with "Hcred").
  (** We can use this to strip laters off multiple hypotheses now. *)
  iIntros "!>!>".
  (** Now we are ready to open the nested invariant! *)
  iInv "Hinv'" as "(%n & >Hl)".
  (** And finally we can take a program step. *)
  wp_store. iModIntro.
  iSplitL "Hl". { iNext. iExists 42. done. }
  iModIntro. iSplitL "Hv'". { iNext. eauto with iFrame. }
  by iApply "Hpost".
Qed.
(* tests/list_reverse.v *)
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ
:=
  match xs with
  | [] => ⌜hd = NONEV⌝
  | x :: xs => ∃ l hd', ⌜hd = SOMEV #l⌝ ∗ l ↦ (x,hd') ∗ is_list hd' xs
  end%I.
(* tests/list_reverse.v *)
Definition rev : val
:=
  rec: "rev" "hd" "acc" :=
    match: "hd" with
      NONE => "acc"
    | SOME "l" =>
       let: "tmp1" := Fst !"l" in
       let: "tmp2" := Snd !"l" in
       "l" <- ("tmp1", "acc");;
       "rev" "tmp2" "hd"
    end.
(* tests/list_reverse.v *)
Lemma rev_acc_wp hd acc xs ys :
  [[{ is_list hd xs ∗ is_list acc ys }]]
    rev hd acc
  [[{ w, RET w; is_list w (reverse xs ++ ys) }]].
Proof.
  iIntros (Φ) "[Hxs Hys] HΦ". Show.
  iInduction xs as [|x xs IH] forall (hd acc ys Φ);
    iSimplifyEq; wp_rec; wp_let.
  - Show. wp_match. by iApply "HΦ".
  - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
    wp_load. wp_load. wp_store.
    iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
    { iExists l, acc; by iFrame. }
    iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Qed.
(* tests/list_reverse.v *)
Lemma rev_wp hd xs :
  [[{ is_list hd xs }]] rev hd NONEV [[{ w, RET w; is_list w (reverse xs) }]].
Proof.
  iIntros (Φ) "Hxs HΦ".
  iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
  iIntros (w). rewrite right_id_L. iApply "HΦ".
Qed.
(* tests/lock.v *)
Definition lock_client_gen : expr
:=
    let: "l" := ref #10 in
    let: "lock" := newlock #() in
    acquire "lock";;
    "l" <- #42;;
    release "lock".
(* tests/lock.v *)
Lemma wp_lock_client_gen `{!heapGS Σ, !lockG Σ} :
    ⊢ WP lock_client_gen {{ _, True }}.
Proof.
    unfold lock_client_gen. wp_alloc l as "Hl".
    wp_smart_apply (newlock_spec (∃ n : Z, l ↦ #n)%I with "[$Hl]")
      as (lk γ) "#Hlock".
    wp_smart_apply (acquire_spec with "Hlock") as "(Hlocked & %v & Hloc)".
    wp_store.
    wp_smart_apply (release_spec with "[$Hlock $Hlocked Hloc]"); by eauto.
  Qed.
(* tests/lock.v *)
Definition lock_client_spin : expr
:=
    let: "l" := ref #10 in
    let: "lock" := newlock #() in
    acquire "lock";;
    "l" <- #42;;
    release "lock".
(* tests/lock.v *)
Lemma wp_lock_client_spin `{!heapGS Σ, !spin_lockG Σ} :
    ⊢ WP lock_client_spin {{ _, True }}.
Proof.
    unfold lock_client_spin.
    (* This should not unfold the [newlock], [acquire], and [release]
    projections. That is, it should not show [spin_lock.<something>]. *)
    simpl. Show.
    wp_alloc l as "Hl".
    wp_smart_apply (newlock_spec (∃ n : Z, l ↦ #n) with "[$Hl]")
      as (lk γ) "#Hlock".
    wp_smart_apply (acquire_spec with "Hlock") as "(Hlocked & %v & Hloc)".
    wp_store.
    wp_smart_apply (release_spec with "[$Hlock $Hlocked Hloc]"); by eauto.
  Qed.
(* tests/lock.v *)
Lemma lock_client_gen_adequate σ :
    adequate NotStuck lock_client_gen σ (λ _ _, True).
Proof.
    set (Σ := #[heapΣ; spin_lockΣ]).
    apply (heap_adequacy Σ); iIntros (?) "_".
    iApply wp_lock_client_gen.
  Qed.
(* tests/lock.v *)
Lemma lock_client_spin_adequate σ :
    adequate NotStuck lock_client_spin σ (λ _ _, True).
Proof.
    set (Σ := #[heapΣ; spin_lockΣ]).
    apply (heap_adequacy Σ); iIntros (?) "_".
    iApply wp_lock_client_gen.
  Qed.
(* tests/monpred.v *)
Notation monPred
:= (monPred I (uPredI M)).
(* tests/monpred.v *)
Lemma monPred_unseal_test_1 P Q (R : monPred) :
    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
Proof.
    intros. split=> i. monPred.unseal.
    (** Make sure [∗] on uPred is not unfolded *)
    Show.
  Abort.
(* tests/monpred.v *)
Lemma monPred_unseal_test_2 P Q (R : monPred) :
    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
Proof.
    uPred.unseal.
    (** Make sure [∗] on monPred is not unfolded *)
    Show.
  Abort.
(* tests/mosel_paper.v *)
Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
  P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
Proof.
  iIntros "[HP H]". Show.
  iDestruct "H" as (x) "[H1|H2]".
  - Show. iExists x. iLeft. iSplitL "HP"; iAssumption.
  - Show. iExists x. iRight. iSplitL "HP"; iAssumption.
Qed.
(* tests/mosel_paper.v *)
Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
  P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
Proof.
  iIntros "[HP H]". Show.
  iFrame "HP". Show.
  iAssumption.
Qed.
(* tests/mosel_paper.v *)
Lemma example_2 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
  <affine> P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, Φ a ∨ (P ∗ Ψ a).
Proof.
  iIntros "[HP H]". iDestruct "H" as (x) "[H1|H2]".
  - iExists x. iLeft. Show. iAssumption.
  - iExists x. iRight. Show. iSplitL "HP"; iAssumption.
Qed.
(* tests/mosel_paper.v *)
Lemma example_3 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
  □ P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, Φ a ∨ (P ∗ P ∗ Ψ a).
Proof.
  iIntros "[#HP H]". Show. iDestruct "H" as (x) "[H1|H2]".
  - iExists x. iLeft. iAssumption.
  - iExists x. iRight. Show. iSplitR; [|iSplitR]; iAssumption.
Qed.
(* tests/mosel_paper.v *)
Lemma example_4 {PROP : bi} {A : Type} (P Q : PROP) : □ P ∧ □ Q -∗ □ (P ∗ Q).
Proof. iIntros "[#HP #HQ]". Show. iModIntro. iSplitL; iAssumption. Qed.
(* tests/mosel_paper.v *)
Lemma example_monpred {I PROP} (Φ Ψ : monPred I PROP) : Φ ∗ (Φ -∗ Ψ) ⊢ Ψ.
Proof. iIntros "[H1 H2]". Show. iApply "H2". iAssumption. Qed.
(* tests/mosel_paper.v *)
Lemma example_monpred_model {I PROP} (Φ Ψ : monPred I PROP) : Φ ∗ (Φ -∗ Ψ) ⊢ Ψ.
Proof. iStartProof PROP. Show. iIntros (i) "[H1 H2]". iApply "H2". iAssumption. Qed.
(* tests/mosel_paper.v *)
Lemma example_monpred_2 {I PROP} (Φ : monPred I PROP) (P Q : PROP) :
  ⎡ P -∗ Q ⎤ -∗ ⎡ □ P ⎤ -∗ <affine> Φ -∗ ⎡ P ∗ Q ⎤.
Proof. iIntros "H1 #H2 H3". Show. iFrame "H2". Show. iApply "H1". iAssumption. Qed.
(* tests/mra.v *)
Notation gset_mra K
:= (mra (⊆@{gset K})).
(* tests/mra.v *)
Lemma mra_test_eq {SI : sidx} X Y :
  to_mra X ≡@{gset_mra nat} to_mra Y → X = Y.
Proof. intros ?%(inj _). Show. done. Qed.
(* tests/mra.v *)
Notation propset_mra K
:= (mra (⊆@{propset K})).
(* tests/mra.v *)
Lemma mra_test_equiv {SI : sidx} X Y :
  to_mra X ≡@{propset_mra nat} to_mra Y → X ≡ Y.
Proof. intros ?%(inj _). done. Qed.
(* tests/one_shot.v *)
Definition one_shot_example : val
:= λ: <>,
  let: "x" := ref NONE in (
  (* tryset *) (λ: "n",
    CAS "x" NONE (SOME "n")),
  (* check  *) (λ: <>,
    let: "y" := !"x" in λ: <>,
    match: "y" with
      NONE => #()
    | SOME "n" =>
       match: !"x" with
         NONE => assert: #false
       | SOME "m" => assert: "n" = "m"
       end
    end)).
(* tests/one_shot.v *)
Definition one_shotR
:= csumR (exclR unitO) (agreeR ZO).
(* tests/one_shot.v *)
Definition Pending : one_shotR
:= Cinl (Excl ()).
(* tests/one_shot.v *)
Definition Shot (n : Z) : one_shotR
:= Cinr (to_agree n).
(* tests/one_shot.v *)
Class one_shotG Σ
:= { #[local] one_shot_inG :: inG Σ one_shotR }.
(* tests/one_shot.v *)
Definition one_shotΣ : gFunctors
:= #[GFunctor one_shotR].
(* tests/one_shot.v *)
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. solve_inG. Qed.
(* tests/one_shot.v *)
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ
:=
  (l ↦ NONEV ∗ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.