phanerozoic/Coq-Iris huggingface dataset:
(* iris_unstable/heap_lang/interpreter.v *)
Ltac stuck_now
:=
    apply eventually_stuck_now, terminal_expr_stuck;
    [done
    |prove_terminal
    |let H := fresh "Hstep" in
     intros * H;
     try (inversion H; congruence) ].
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interpret_complete fuel : ∀ e s msg s',
    ∀ (Hwf: state_wf s),
      interpret fuel e s = (inr (Stuck msg), s') →
      eventually_stuck e s.(forked_threads) s.(lang_state) s'.(forked_threads) s'.(lang_state).
Proof.
    induction fuel as [|fuel]; simpl; intros e s msg s' **; [congruence|].
    destruct e; failure; stuck_steps; try stuck_fill;
      try (repeat case_match; failure; try stuck_now;
           let n := numgoals in guard n <= 1);
      simplify_eq.
    - (* App *)
      stuck_steps.
      eauto.
    - (* If *)
      repeat case_match; failure; try stuck_now.
      + stuck_steps; eauto.
      + stuck_steps; eauto.
    - (* Case *)
      repeat case_match; failure; try stuck_now.
      + stuck_steps; eauto.
      + stuck_steps; eauto.
    - (* CmpXchg *)
      success. stuck_now.
    - (* FAA *)
      lazymatch goal with
      | H: read_loc _ _ _ = (inl ?p, _) |- _ => destruct p as [l v]
      end.
      success.
      repeat case_match; failure; stuck_now.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Definition exec (fuel:nat) (e: expr) : val + Error
:=
  interp_monad.run (interpret fuel e).
(* iris_unstable/heap_lang/interpreter.v *)
Theorem exec_spec fuel e :
  match exec fuel e with
  | inl v =>
    (* if the interpreter runs to completion, it produces a valid execution of
    [e] *)
    ∃ tp' σ', rtc erased_step ([e], init_state) ([Val v] ++ tp', σ')
  | inr (Stuck _) =>
    (* if the interpreter produces a "stuck" error message, [e] can get stuck *)
    ∃ e' tp' σ', rtc erased_step ([e], init_state) ([e'] ++ tp', σ') ∧ stuck e' σ'
  | inr _ =>
    (* If the interpreter fails otherwise (due to running out of fuel or an
    unsupported prophecy variable operation), then it provides no guarantees. *)
    True
  end.
Proof.
  rewrite /exec /interp_monad.run.
  destruct (interpret fuel e init_interp_state) as [r s] eqn:Hinterpret.
  destruct r as [v | [msg|msg|] ]; simpl; auto.
  - apply interpret_sound in Hinterpret;
      eauto using init_interp_state_wf.
  - apply interpret_complete in Hinterpret;
      auto using init_interp_state_wf.
    destruct Hinterpret as (e' & Hexec & Hstuck); eauto.
Qed.
(* tests/algebra.v *)
(* Should follow from [forall_inhabited] in std++, test that the the OFE
abstractions are actually unfolded by type class search. *)
Lemma discrete_fun_inhabited{SI : sidx} {A} (B : A → ofe)
  `{∀ x, Inhabited (B x)} : Inhabited (discrete_funO B).
Proof. apply _. Qed.
(* tests/algebra.v *)
(* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
  From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
    l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
Abort.
(* tests/algebra.v *)
(* analogous test for [Equiv] and https://github.com/coq/coq/issues/14441.
  From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
Abort.
(* tests/algebra.v *)
(* Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
with carriers that are definitionally equal. See also
https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
Definition tag
:= nat.
(* tests/algebra.v *)
Canonical tagO
:= leibnizO tag.
(* tests/algebra.v *)
Instance test_cofe {Σ} : Cofe (iPrePropO Σ)
:= _.
(* tests/algebra.v *)
Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ)
:=
    λne P v, (▷ (P v))%I.
(* tests/algebra.v *)
(* Regression test for <https://gitlab.mpi-sws.org/iris/iris/issues/255>. *)
Definition testR
:= authR (prodUR
        (prodUR
          (optionUR (exclR unitO))
          (optionUR (exclR unitO)))
        (optionUR (agreeR (boolO)))).
(* tests/algebra.v *)
Lemma test_prod_persistent γ :
    Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))).
Proof. apply _. Qed.
(* tests/algebra.v *)
(* Make sure the [auth]/[gmap_view] notation does not mix up its arguments. *)
Definition auth_check {A : ucmra} :
  auth A = authO A
:= eq_refl.
(* tests/algebra.v *)
Definition gmap_view_check {K : Type} `{Countable K} {V : cmra} :
  gmap_view K V = gmap_viewO K V
:= eq_refl.
(* tests/algebra.v *)
Lemma uncurry_ne_test {A B C : ofe} (f : A → B → C) :
  NonExpansive2 f → NonExpansive (uncurry f).
Proof. apply _. Qed.
(* tests/algebra.v *)
Lemma uncurry3_ne_test {A B C D : ofe} (f : A → B → C → D) :
  NonExpansive3 f → NonExpansive (uncurry3 f).
Proof. apply _. Qed.
(* tests/algebra.v *)
Lemma uncurry4_ne_test {A B C D E : ofe} (f : A → B → C → D → E) :
  NonExpansive4 f → NonExpansive (uncurry4 f).
Proof. apply _. Qed.
(* tests/algebra.v *)
Lemma curry_ne_test {A B C : ofe} (f : A * B → C) :
  NonExpansive f → NonExpansive2 (curry f).
Proof. apply _. Qed.
(* tests/algebra.v *)
Lemma curry3_ne_test {A B C D : ofe} (f : A * B * C → D) :
  NonExpansive f → NonExpansive3 (curry3 f).
Proof. apply _. Qed.
(* tests/algebra.v *)
Lemma curry4_ne_test {A B C D E : ofe} (f : A * B * C * D → E) :
  NonExpansive f → NonExpansive4 (curry4 f).
Proof. apply _. Qed.
(* tests/algebra.v *)
(* Regression test for https://gitlab.mpi-sws.org/iris/iris/-/issues/577 *)
Lemma list_bind_ne_test {A B : ofe} (f : A → list B) :
  NonExpansive f → NonExpansive (mbind f : list A → list B).
Proof. apply _. Qed.
(* tests/algebra.v *)
(* Needs "new" unification for [Monoid] *)
Definition big_op_test (l : list Qp) : option Qp
:=
  [^op list] x ∈ l, Some x.
(* tests/algebra.v *)
(* [frac] and [ufrac] are different cameras on the same carrier (namely [Qp]).
They have the same operator (namely, addition on [Qp]), but different validity
predicates ([≤ 1] and [True], respectively). The big operators only rely on
the "monoid" part of [frac] and [ufrac] (i.e., not their validity), so it should
not matter via which camera we obtained the [Monoid] instance. We test that the
difference in [Monoid] instance (which is not even visible, unless one enables
printing of implicit arguments) does not affect definitional equality of big
operators. *)
Lemma big_opL_should_be_eq l :
  ([^op list] x ∈ (l : list (option frac)), x) =
  ([^op list] x ∈ (l : list (option ufrac)), x).
Proof. reflexivity. Qed.
(* tests/algebra.v *)
Lemma big_opM_should_be_eq `{Countable K} m :
  ([^op map] x ∈ (m : gmap K (option frac)), x) =
  ([^op map] x ∈ (m : gmap K (option ufrac)), x).
Proof. reflexivity. Qed.
(* tests/algebra.v *)
Lemma big_opS_should_be_eq X :
  ([^op set] x ∈ (X : gset (option frac)), x) =
  ([^op set] x ∈ (X : gset (option ufrac)), x).
Proof. reflexivity. Qed.
(* tests/algebra.v *)
Lemma big_opMS_should_be_eq `{Countable K} X :
  ([^op mset] x ∈ (X : gmultiset (option frac)), x) =
  ([^op mset] x ∈ (X : gmultiset (option ufrac)), x).
Proof. reflexivity. Qed.
(* tests/atomic.v *)
(* We can quantify over telescopes *inside* Iris and use them with atomic
  updates. *)
Definition AU_tele_quantify_iris : Prop
:=
    ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
        atomic_update Eo Ei α β Φ.
(* tests/atomic.v *)
(* iAuIntro works. *)
Lemma au_intro_1 (P : PROP) (α : TA → PROP) (β Φ : TA → TB → PROP) :
    P -∗ atomic_update Eo Ei α β Φ.
Proof. iIntros "HP". iAuIntro. Abort.
(* tests/atomic.v *)
Lemma test_awp_apply (Q : iProp Σ) (l : loc) v :
    heap_inv -∗ Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
Proof.
    iIntros "Hheap HQ Hl". awp_apply (load_spec with "Hheap"). Show.
    iAaccIntro with "Hl"; eauto with iFrame.
  Qed.
(* tests/atomic.v *)
Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
    heap_inv -∗ Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
Proof.
    iIntros "Hheap HQ Hl". awp_apply (load_spec with "Hheap") without "HQ". Show.
    iAaccIntro with "Hl"; eauto with iFrame.
  Qed.
(* tests/atomic.v *)
(* Without private postcondition or RET binders *)
Lemma print_both_quant (P : val → iProp Σ) :
    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ ∃∃ y, P y | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". rewrite difference_empty_L. Show.
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_first_quant l :
    ⊢ <<{ ∀∀ x, l ↦ x }>> code @ ∅ <<{ l ↦ x | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_second_quant l :
    ⊢ <<{ l ↦ #() }>> code @ ∅ <<{ ∃∃ y, l ↦ y | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_no_quant l :
    ⊢ <<{ l ↦ #() }>> code @ ∅ <<{ l ↦ #() | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_both_quant_long l :
    ⊢ <<{ ∀∀ x, l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ ∃ y, l ↦ y | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_both_quant_longpre l :
    ⊢ <<{ ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ ∃∃ y, l ↦ y | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_both_quant_longpost l :
    ⊢ <<{ ∀∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>> code @ ∅ <<{ ∃∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx | RET #() }>>.
Proof.
    Show. iIntros (Φ) "?". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_first_quant_long l :
    ⊢ <<{ ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ l ↦ x | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_second_quant_long l x :
    ⊢ <<{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ ∃∃ y, l ↦ y | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_no_quant_long l x :
    ⊢ <<{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ l ↦ #() | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_no_quant_longpre l xx yyyy :
    ⊢ <<{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>> code @ ∅ <<{ l ↦ yyyy | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
Lemma print_no_quant_longpost l xx yyyy :
    ⊢ <<{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>> code @ ∅ <<{ l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx | RET #() }>>.
Proof.
    Show. iIntros (Φ) "AU". Show.
  Abort.
(* tests/atomic.v *)
(* With private postcondition.
  (Makes no big difference for the AU so we only print the initial triple here.) *)
Lemma print_all (P : val → iProp Σ) :
    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ ∃∃ y, P y | z, RET z; P z }>>.
Proof. Show. Abort.
(* tests/atomic.v *)
Lemma print_no_ret (P : val → iProp Σ) :
    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ ∃∃ y, P y | RET y; P y }>>.
Proof. Show. Abort.
(* tests/atomic.v *)
Lemma print_no_ex_ret (P : val → iProp Σ) :
    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ P x | RET x; P x }>>.
Proof. Show. Abort.
(* tests/atomic.v *)
Lemma print_no_all_ret (P : val → iProp Σ) :
    ⊢ <<{ P #() }>> code @ ∅ <<{ ∃∃ y, P y | RET y; P y }>>.
Proof. Show. Abort.
(* tests/atomic.v *)
Lemma print_no_all_ex_ret (P : iProp Σ) :
    ⊢ <<{ P }>> code @ ∅ <<{ P | RET #42; P }>>.
Proof. Show. Abort.
(* tests/atomic.v *)
Lemma iMod_prettify (P : val → iProp Σ) :
    ⊢ <<{ ∀∀ x, P x }>> !#0 @ ∅ <<{ ∃∃ y, P y | RET #() }>>.
Proof.
    iIntros (Φ) "AU". iMod "AU". Show.
  Abort.
(* tests/bi.v *)
(* See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
Lemma test_impl_persistent_1 `{!Sbi PROP, !BiPersistentlyImplSiPure PROP} :
  Persistent (PROP:=PROP) (True → True).
Proof. apply _. Qed.
(* tests/bi.v *)
Lemma test_impl_persistent_2 `{!Sbi PROP, !BiPersistentlyImplSiPure PROP} :
  Persistent (PROP:=PROP) (True → True → True).
Proof. apply _. Qed.
(* tests/bi.v *)
(* Test that the right scopes are used. *)
Lemma test_bi_scope {PROP : bi} : True.
Proof.
  (* [<affine> True] is implicitly in %I scope. *)
  pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
Abort.
(* tests/bi.v *)
(* Some basic tests to make sure patterns work in big ops. *)
Definition big_sepM_pattern_value
    {PROP : bi} (m : gmap nat (nat * nat)) : PROP
:=
  [∗ map] '(x,y) ∈ m, ⌜ 10 = x ⌝.
(* tests/bi.v *)
Definition big_sepM_pattern_value_tt
    {PROP : bi} (m : gmap nat ()) : PROP
:=
  [∗ map] '() ∈ m, True.
(* tests/bi.v *)
Inductive foo
:= Foo (n : nat).
(* tests/bi.v *)
Definition big_sepM_pattern_value_custom
    {PROP : bi} (m : gmap nat foo) : PROP
:=
  [∗ map] '(Foo x) ∈ m, ⌜ 10 = x ⌝.
(* tests/bi.v *)
Definition big_sepM_pattern_key
    {PROP : bi} (m : gmap (nat * nat) nat) : PROP
:=
  [∗ map] '(k,_) ↦ _ ∈ m, ⌜ 10 = k ⌝.
(* tests/bi.v *)
Definition big_sepM_pattern_both
    {PROP : bi} (m : gmap (nat * nat) (nat * nat)) : PROP
:=
  [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.
(* tests/bi.v *)
Definition big_sepM2_pattern {PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP
:=
  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
(* tests/bi.v *)
(* With a cast, we can force Coq to type check the body with [x : nat] and
thereby insert the [nat] to [Z] coercion in the body. *)
Definition big_sepM_cast {PROP : bi} (m : gmap nat nat) : PROP
:=
  [∗ map] (x:nat) ∈ m, ⌜ 10%Z = x ⌝.
(* tests/bi.v *)
(* And we can do the same with an [Implicit Type]. *)
Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP
:=
    [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.
(* tests/bi.v *)
Lemma big_sepL_simpl {PROP : bi} {A} (Φ : A → PROP) :
  ⊢ ([∗ list] x ∈ [], Φ x).
Proof.
  simpl.
  (* Should [simpl] to [emp] *)
  Show.
Abort.
(* tests/bi.v *)
Lemma match_persistent :
    Persistent (PROP:=PROP) (∃ b : bool, if b then False else False).
Proof. apply _. Qed.
(* tests/bi.v *)
Lemma match_affine :
    Affine (PROP:=PROP) (∃ b : bool, if b then False else False).
Proof. apply _. Qed.
(* tests/bi.v *)
Lemma match_absorbing :
    Absorbing (PROP:=PROP) (∃ b : bool, if b then False else False).
Proof. apply _. Qed.
(* tests/bi.v *)
Lemma match_timeless :
    Timeless (PROP:=PROP) (∃ b : bool, if b then False else False).
Proof. apply _. Qed.
(* tests/bi.v *)
Lemma match_plain `{!Sbi PROP} :
    Plain (PROP:=PROP) (∃ b : bool, if b then False else False).
Proof. apply _. Qed.
(* tests/bi.v *)
Lemma match_list_persistent :
    Persistent (PROP:=PROP)
      (∃ l : list nat, match l with [] => False | _ :: _ => False end).
Proof. apply _. Qed.
(* tests/bi.v *)
(* From https://gitlab.mpi-sws.org/iris/iris/-/issues/576. *)
Lemma pair_timeless `{!Timeless (emp%I : PROP)} (m : gset (nat * nat)) :
    Timeless (PROP:=PROP) ([∗ set] '(k1, k2) ∈ m, False).
Proof. apply _. Qed.
(* tests/bi.v *)
(* Don't want instances to unfold def's. *)
Definition match_foo (b : bool) : PROP
:= if b then False%I else False%I.
(* tests/bi.v *)
Lemma match_def_unfold_fail b :
    Persistent (match_foo b).
Proof. Fail apply _. Abort.
(* tests/bi_ascii_parsing.v *)
Ltac pg
:=
    match goal with
    | |- ?X => idtac X
    end.
(* tests/bi_ascii_parsing.v *)
Ltac foo g
:=
    lazymatch g with
    | |- ?T => idtac T
    | ?U |- ?T => idtac U T
    end.
(* tests/bi_ascii_parsing.v *)
Ltac bar
:=
    match goal with
    | |- ?G => foo G
    end.
(* tests/bi_ascii_parsing.v *)
Lemma test1 : |-@{PROP} True.
Proof. bar. pg. Abort.
(* tests/bi_ascii_parsing.v *)
Lemma test2 : False |-@{PROP} True.
Proof. bar. pg. Abort.
(* tests/fixpoint.v *)
Definition L
:= bi_least_fixpoint F.
(* tests/fixpoint.v *)
Definition G
:= bi_greatest_fixpoint F.
(* tests/fixpoint.v *)
(* Make sure the lemmas [iApply] without having to repeat the induction
  predicate [Φ]. See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/967
  for details. *)
Lemma ind_test (a : A) :
    ∀ x, L x -∗ x ≡ a.
Proof.
    iApply (least_fixpoint_ind F); first by solve_proper. Undo.
    iApply (least_fixpoint_ind_wf F); first by solve_proper. Undo.
  Abort.
(* tests/fixpoint.v *)
Lemma coind_test (a : A) :
    ∀ x, x ≡ a -∗ G x.
Proof.
    iApply (greatest_fixpoint_coind F); first by solve_proper. Undo.
    iApply (greatest_fixpoint_paco F); first by solve_proper. Undo.
  Abort.
(* tests/gset.v *)
Lemma test_op (X Y : gset nat) : X ⊆ Y → X ⋅ Y = Y.
Proof. set_solver. Qed.
(* tests/gset.v *)
Lemma test_included (X Y : gset nat) : X ≼ Y → X ∪ Y = Y ∧ X ∩ Y = X.
Proof. set_solver. Qed.
(* tests/gset.v *)
Lemma test_disj_included (X Y : gset nat) : GSet X ≼ GSet Y → X ∪ Y = Y ∧ X ∩ Y = X.
Proof. set_solver. Qed.
(* tests/gset.v *)
Lemma test_disj_equiv n : GSet (∅ : gset nat) ≡ GSet {[n]} → False.
Proof. set_solver. Qed.
(* tests/gset.v *)
Lemma test_disj_eq n : GSet (∅ : gset nat) = GSet {[n]} → False.
Proof. set_solver. Qed.
(* tests/gset.v *)
Lemma test_disj_valid (X Y : gset nat) : ✓ (GSet X ⋅ GSet Y) → X ∩ Y = ∅.
Proof. set_solver. Qed.
(* tests/heapprop.v *)
(* This file constructs a simple non step-indexed linear separation logic as
predicates over heaps (modeled as maps from integer locations to integer values).
It shows that Iris's [bi] canonical structure can be inhabited, and the Iris
proof mode can be used to prove lemmas in this separation logic. *)
Definition loc
:= Z.
(* tests/heapprop.v *)
Record heapProp
:= HeapProp {
  heapProp_holds :> gmap loc val → Prop;
}.
(* tests/heapprop.v *)
Inductive heapProp_equiv' (P Q : heapProp) : Prop
:=
    { heapProp_in_equiv : ∀ σ, P σ ↔ Q σ }.
(* tests/heapprop.v *)
Instance heapProp_equiv : Equiv heapProp
:= heapProp_equiv'.
(* tests/heapprop.v *)
Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
(* tests/heapprop.v *)
Canonical heapPropO
:= discreteO heapProp.
(* tests/heapprop.v *)
(* logical entailement *)
Inductive heapProp_entails (P Q : heapProp) : Prop
:=
  { heapProp_in_entails : ∀ σ, P σ → Q σ }.
(* tests/heapprop.v *)
(* logical connectives *)
Definition heapProp_emp_def : heapProp
:=
  {| heapProp_holds σ := σ = ∅ |}.
(* tests/heapprop.v *)
Definition heapProp_emp_aux : seal (@heapProp_emp_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_emp
:= unseal heapProp_emp_aux.
(* tests/heapprop.v *)
Definition heapProp_emp_unseal :
  @heapProp_emp = @heapProp_emp_def
:= seal_eq heapProp_emp_aux.
(* tests/heapprop.v *)
Definition heapProp_pure_def (φ : Prop) : heapProp
:=
  {| heapProp_holds _ := φ |}.
(* tests/heapprop.v *)
Definition heapProp_pure_aux : seal (@heapProp_pure_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_pure
:= unseal heapProp_pure_aux.
(* tests/heapprop.v *)
Definition heapProp_pure_unseal :
  @heapProp_pure = @heapProp_pure_def
:= seal_eq heapProp_pure_aux.
(* tests/heapprop.v *)
Definition heapProp_and_def (P Q : heapProp) : heapProp
:=
  {| heapProp_holds σ := P σ ∧ Q σ |}.
(* tests/heapprop.v *)
Definition heapProp_and_aux : seal (@heapProp_and_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_and
:= unseal heapProp_and_aux.
(* tests/heapprop.v *)
Definition heapProp_and_unseal:
  @heapProp_and = @heapProp_and_def
:= seal_eq heapProp_and_aux.
(* tests/heapprop.v *)
Definition heapProp_or_def (P Q : heapProp) : heapProp
:=
  {| heapProp_holds σ := P σ ∨ Q σ |}.
(* tests/heapprop.v *)
Definition heapProp_or_aux : seal (@heapProp_or_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_or
:= unseal heapProp_or_aux.
(* tests/heapprop.v *)
Definition heapProp_or_unseal:
  @heapProp_or = @heapProp_or_def
:= seal_eq heapProp_or_aux.
(* tests/heapprop.v *)
Definition heapProp_impl_def (P Q : heapProp) : heapProp
:=
  {| heapProp_holds σ := P σ → Q σ |}.
(* tests/heapprop.v *)
Definition heapProp_impl_aux : seal (@heapProp_impl_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_impl
:= unseal heapProp_impl_aux.
(* tests/heapprop.v *)
Definition heapProp_impl_unseal :
  @heapProp_impl = @heapProp_impl_def
:= seal_eq heapProp_impl_aux.
(* tests/heapprop.v *)
Definition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp
:=
  {| heapProp_holds σ := ∀ a, Ψ a σ |}.
(* tests/heapprop.v *)
Definition heapProp_forall_aux : seal (@heapProp_forall_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_forall {A}
:= unseal heapProp_forall_aux A.
(* tests/heapprop.v *)
Definition heapProp_forall_unseal :
  @heapProp_forall = @heapProp_forall_def
:= seal_eq heapProp_forall_aux.
(* tests/heapprop.v *)
Definition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp
:=
  {| heapProp_holds σ := ∃ a, Ψ a σ |}.
(* tests/heapprop.v *)
Definition heapProp_exist_aux : seal (@heapProp_exist_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_exist {A}
:= unseal heapProp_exist_aux A.
(* tests/heapprop.v *)
Definition heapProp_exist_unseal :
  @heapProp_exist = @heapProp_exist_def
:= seal_eq heapProp_exist_aux.
(* tests/heapprop.v *)
Definition heapProp_sep_def (P Q : heapProp) : heapProp
:=
  {| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
(* tests/heapprop.v *)
Definition heapProp_sep_aux : seal (@heapProp_sep_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_sep
:= unseal heapProp_sep_aux.
(* tests/heapprop.v *)
Definition heapProp_sep_unseal:
  @heapProp_sep = @heapProp_sep_def
:= seal_eq heapProp_sep_aux.
(* tests/heapprop.v *)
Definition heapProp_wand_def (P Q : heapProp) : heapProp
:=
  {| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
(* tests/heapprop.v *)
Definition heapProp_wand_aux : seal (@heapProp_wand_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_wand
:= unseal heapProp_wand_aux.
(* tests/heapprop.v *)
Definition heapProp_wand_unseal:
  @heapProp_wand = @heapProp_wand_def
:= seal_eq heapProp_wand_aux.
(* tests/heapprop.v *)
Definition heapProp_persistently_def (P : heapProp) : heapProp
:=
  heapProp_pure (heapProp_entails heapProp_emp P).
(* tests/heapprop.v *)
Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
Proof. by eexists. Qed.
(* tests/heapprop.v *)
Definition heapProp_persistently
:= unseal heapProp_persistently_aux.
(* tests/heapprop.v *)
Definition heapProp_persistently_unseal:
  @heapProp_persistently = @heapProp_persistently_def
:= seal_eq heapProp_persistently_aux.
(* tests/heapprop.v *)
(* Iris's [bi] class requires the presence of a later modality, but for non
step-indexed logics, it can be defined as the identity. *)
Definition heapProp_later (P : heapProp) : heapProp
:= P.
(* tests/heapprop.v *)
Definition heapProp_unseal
:=
  (heapProp_emp_unseal, heapProp_pure_unseal, heapProp_and_unseal,
   heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
   heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
   heapProp_persistently_unseal).
(* tests/heapprop.v *)
Ltac unseal
:= rewrite !heapProp_unseal /=.
(* tests/heapprop.v *)
Lemma heapProp_bi_persistently_mixin :
    BiPersistentlyMixin
      heapProp_entails heapProp_emp heapProp_and
      (@heapProp_exist) heapProp_sep heapProp_persistently.
Proof.
    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
    - (* [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x] *)
      unseal. intros A Φ [H]. destruct (H ∅) as [x ?]; [done|].
      exists x. by split=> σ ->.
    - by rewrite heapProp_persistently_unseal.
  Qed.
(* tests/heapprop.v *)
Lemma heapProp_bi_later_mixin :
    BiLaterMixin
      heapProp_entails heapProp_pure heapProp_or heapProp_impl
      (@heapProp_forall) (@heapProp_exist)
      heapProp_sep heapProp_persistently heapProp_later.
Proof. eapply bi_later_mixin_id; [done|apply heapProp_bi_mixin]. Qed.
(* tests/heapprop.v *)
Canonical heapPropI : bi
:=
  {| bi_ofe_mixin := ofe_mixin_of heapProp;
     bi_bi_mixin := heapProp_bi_mixin;
     bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
     bi_bi_later_mixin := heapProp_bi_later_mixin |}.
(* tests/heapprop.v *)
Instance heapProp_pure_forall : BiPureForall heapPropI.
Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.