ReactorJet/Coq-Iris huggingface dataset:
(* iris_heap_lang/adequacy.v *)
From iris.algebra Require Import auth
From iris.base_logic.lib Require Import mono_nat
From iris.proofmode Require Import proofmode
From iris.program_logic Require Export weakestpre adequacy
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Class heapGpreSΣ := HeapGpreS {
  #[global] heapGpreS_iris :: invGpreS Σ;
  #[global] heapGpreS_heap :: gen_heapGpreS loc (option val) Σ;
  #[global] heapGpreS_inv_heap :: inv_heapGpreS loc (option val) Σ;
  #[global] heapGpreS_proph :: proph_mapGpreS proph_id (val * val) Σ;
  #[global] heapGS_step_cnt :: mono_natG Σ;
}.

Definition heapΣ: gFunctors :=
  #[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val);
    proph_mapΣ proph_id (val * val); mono_natΣ].

Global InstancesubG_heapGpreS {Σ} : subG heapΣ Σ → heapGpreS Σ.
Proof. solve_inG. Qed.

Lemma heap_adequacyΣ `{!heapGpreS Σ} s e σ φ :
  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
  adequate s e σ (λ v _, φ v).
Proof.
  intros Hwp.
  apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
  eapply (wp_strong_adequacy Σ _); [|done].
  iIntros (Hinv).
  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
  iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
  iMod (mono_nat_own_alloc) as (γ) "[Hsteps _]".
  iDestruct (Hwp (HeapGS _ _ _ _ _ _ _ _) with "Hi") as "Hwp".
  iModIntro.
  iExists (λ σ ns κs nt, (gen_heap_interp σ.(heap) ∗
                          proph_map_interp κs σ.(used_proph_id) ∗
                          mono_nat_auth_own γ 1 ns))%I.
  iExists [(λ v, ⌜φ v⌝%I)], (λ _, True)%I, _ => /=.
  iFrame.
  iIntros (es' t2' -> ? ?) " _ H _".
  iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
  iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
  iDestruct (big_sepL2_nil_inv_r with "H") as %->.
  iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
Qed.
(* iris_heap_lang/locations.v *)
From stdpp Require Import countable numbers gmap
From iris.prelude Require Export prelude
From iris.prelude Require Import options

Record loc:= Loc { loc_car : Z }.
Add Printing Constructor loc.

Local OpenScope Z_scope.

Lemma eq_specl1 l2 : l1 = l2 ↔ loc_car l1 = loc_car l2.
  Proof. destruct l1, l2; naive_solver. Qed.

Global Instanceeq_dec : EqDecision loc.
  Proof. solve_decision. Defined.

Global Instanceinhabited : Inhabited loc := populate {|loc_car := 0 |}.

Global Instancecountable : Countable loc.
  Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.

Global ProgramInstance infinite : Infinite loc :=
    inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
  Next Obligation. done. Qed.

Definition add(l : loc) (off : Z) : loc :=
    {| loc_car := loc_car l + off|}.

Definition le(l1 l2 : loc) : Prop := loc_car l1 ≤ loc_car l2.

Definition lt(l1 l2 : loc) : Prop := loc_car l1 < loc_car l2.

Lemma add_assocl i j : l +ₗ i +ₗ j = l +ₗ (i + j).
  Proof. rewrite eq_spec /=. lia. Qed.

Lemma add_0l : l +ₗ 0 = l.
  Proof. rewrite eq_spec /=; lia. Qed.

Global Instanceadd_inj l : Inj eq eq (add l).
  Proof. intros x1 x2. rewrite eq_spec /=. lia. Qed.

Global Instancele_dec l1 l2 : Decision (l1 ≤ₗ l2).
  Proof. rewrite /le. apply _. Qed.

Global Instancelt_dec l1 l2 : Decision (l1 <ₗ l2).
  Proof. rewrite /lt. apply _. Qed.

Global Instancele_po : PartialOrder le.
  Proof.
    rewrite /le. split; [split|].
    - by intros ?.
    - intros [x] [y] [z]; lia.
    - intros [x] [y] ??; f_equal/=; lia.
  Qed.

Global Instancele_total : Total le.
  Proof. rewrite /Total /le. lia. Qed.

Lemma le_ngtl1 l2 : l1 ≤ₗ l2 ↔ ¬l2 <ₗ l1.
  Proof. apply Z.le_ngt. Qed.

Lemma le_lteql1 l2 : l1 ≤ₗ l2 ↔ l1 <ₗ l2 ∨ l1 = l2.
  Proof. rewrite eq_spec. apply Z.le_lteq. Qed.

Lemma add_le_monol1 l2 i1 i2 :
    l1 ≤ₗ l2 → i1 ≤ i2 → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
  Proof. apply Z.add_le_mono. Qed.

Definition fresh(ls : gset loc) : loc :=
    {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.

Lemma fresh_freshls i : 0 ≤ i → fresh ls +ₗ i ∉ ls.
  Proof.
    intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh ls) + i).
    { intros help Hf%help. simpl in *. lia. }
    apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)));
      set_solver by eauto with lia.
  Qed.

Global Opaquefresh.
(* iris_heap_lang/notation.v *)
From iris.program_logic Require Import language
From iris.heap_lang Require Export lang
From iris.prelude Require Import options

Coercion LitInt: Z >-> base_lit.

Coercion LitBool: bool >-> base_lit.

Coercion LitLoc: loc >-> base_lit.

Coercion LitProphecy: proph_id >-> base_lit.

Coercion App: expr >-> Funclass.

Coercion Val: val >-> expr.

Coercion Var: string >-> expr.

Notation Lamx e := (Rec BAnon x e) (only parsing).

Notation Letx e1 e2 := (App (Lam x e2) e1) (only parsing).

Notation Seqe1 e2 := (Let BAnon e1 e2) (only parsing).

Notation LamVx e := (RecV BAnon x e) (only parsing).

Notation LetCtxx e2 := (AppRCtx (LamV x e2)) (only parsing).

Notation SeqCtxe2 := (LetCtx BAnon e2) (only parsing).

Notation Matche0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).

Notation Alloce := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).

Notation CASl e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing).

Notation Skip:= (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUnit)).

Notation NONE:= (InjL (LitV LitUnit)) (only parsing).

Notation NONEV:= (InjLV (LitV LitUnit)) (only parsing).

Notation SOMEx := (InjR x) (only parsing).

Notation SOMEVx := (InjRV x) (only parsing).

Notation ResolveProphe1 e2 := (Resolve Skip e1 e2) (only parsing).
(* iris_heap_lang/pretty.v *)
From stdpp Require Export pretty
From iris.heap_lang Require Import lang
From iris.prelude Require Import options

Global Instancepretty_loc : Pretty loc :=
  λ l, pretty l.(loc_car).

Global Instancepretty_base_lit : Pretty base_lit :=
  λ l, match l with
       | LitInt z => pretty z
       | LitBool b => if b then "true" else "false"
       | LitUnit => "()"
       | LitPoison => "<poison>"
       | LitLoc l => "(loc " +:+ pretty l +:+ ")"
       | LitProphecy i => "(prophecy " +:+ pretty i +:+ ")"
       end.

Global Instancepretty_binder : Pretty binder :=
  λ b, match b with
       | BNamed x => x
       | BAnon => "<>"
       end.

Global Instancepretty_val : Pretty val :=
  fix go v :=
    match v with
    | LitV l => "#" +:+ pretty l
    | RecV f x e =>
      match f with
      | BNamed f => "rec: " +:+ f +:+ " " +:+ pretty x +:+ " := <body>"
      | BAnon => "λ: " +:+ pretty x +:+ ", <body>"
      end
    | PairV v1 v2 => "(" +:+ go v1 +:+ ", " +:+ go v2 +:+ ")"
    | InjLV v => "inl (" +:+ go v +:+ ")"
    | InjRV v => "inr (" +:+ go v +:+ ")"
    end.

Global Instancepretty_un_op : Pretty un_op :=
  λ op, match op with
        | NegOp => "~"
        | MinusUnOp => "-"
        end.

Global Instancepretty_bin_op : Pretty bin_op :=
  λ op, match op with
        | PlusOp => "+"
        | MinusOp => "-"
        | MultOp => "*"
        | QuotOp => "`quot`"
        | RemOp => "`rem`"
        | AndOp => "&"
        | OrOp => "|"
        | XorOp => "`xor`"
        | ShiftLOp => "<<"
        | ShiftROp => ">>"
        | LeOp => "≤"
        | LtOp => "<"
        | EqOp => "="
        | OffsetOp => "+ₗ"
        end.
(* iris_heap_lang/tactics.v *)
From stdpp Require Import fin_maps
From iris.heap_lang Require Export lang
From iris.prelude Require Import options

Ltac reshape_expre tac :=

Ltac inv_base_step:=
  repeat match goal with
  | _ => progress simplify_map_eq/=
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : base_step ?e _ _ _ _ _ |- _ =>
     try (is_var e; fail 1);
     inversion H; subst; clear H
  end.
Create HintDb base_step.

Global HintExtern 0 (base_reducible _ _) => eexists _, _, _, _; simpl : base_step.

Global HintExtern 0 (base_reducible_no_obs _ _) => eexists _, _, _; simpl : base_step.

Global HintExtern 1 (base_step _ _ _ _ _ _) => econstructor : base_step.

Global HintExtern 0 (base_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : base_step.

Global HintExtern 0 (base_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : base_step.

Global HintExtern 0 (base_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : base_step.
(* iris_heap_lang/total_adequacy.v *)
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import mono_nat
From iris.program_logic Require Export total_adequacy
From iris.heap_lang Require Export adequacy
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Definition heap_totalΣ `{!heapGpreS Σ} s e σ φ :
  (∀ `{!heapGS_gen HasNoLc Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
  sn erased_step ([e], σ).
Proof.
  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
  iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
  iMod (mono_nat_own_alloc 0) as (γ) "[Hsteps _]".
  iModIntro.
  iExists
    (λ σ ns κs _, (gen_heap_interp σ.(heap) ∗
                   proph_map_interp κs σ.(used_proph_id) ∗
                   mono_nat_auth_own γ 1 ns)%I),
    id, (λ _, True%I), _; iFrame.
  by iApply (Hwp (HeapGS _ _ _ _ _ _ _ _)).
Qed.
(* tests/algebra.v *)
From iris.algebra Require Import frac ufrac auth excl lib.gmap_view
From iris.base_logic.lib Require Import invariants
From iris.prelude Require Import options
From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)

Lemma discrete_fun_inhabited{SI : sidx} {A} (B : A → ofe)
  `{∀ x, Inhabited (B x)} : Inhabited (discrete_funO B).
Proof. apply _. Qed.

Lemma list_dist_lookup{A : ofe} n (l1 l2 : list A) :
    l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
  Abort.

Lemma list_equiv_lookup_ofe{A : ofe} (l1 l2 : list A) :
    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
  Abort.

Definition tag:= nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. reflexivity. Qed.

Global Instancetest_cofe {Σ} : Cofe (iPrePropO Σ) := _.

Program Definitiontest : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
    λne P v, (▷ (P v))%I.
  Solve Obligations with solve_proper.

Definition testR:= authR (prodUR
        (prodUR
          (optionUR (exclR unitO))
          (optionUR (exclR unitO)))
        (optionUR (agreeR (boolO)))).

Lemma test_prod_persistentγ :
    Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))).
  Proof. apply _. Qed.

Definition auth_check{A : ucmra} :
  auth A = authO A := eq_refl.

Definition gmap_view_check{K : Type} `{Countable K} {V : cmra} :
  gmap_view K V = gmap_viewO K V := eq_refl.

Lemma uncurry_ne_test{A B C : ofe} (f : A → B → C) :
  NonExpansive2 f → NonExpansive (uncurry f).
Proof. apply _. Qed.

Lemma uncurry3_ne_test{A B C D : ofe} (f : A → B → C → D) :
  NonExpansive3 f → NonExpansive (uncurry3 f).
Proof. apply _. Qed.

Lemma uncurry4_ne_test{A B C D E : ofe} (f : A → B → C → D → E) :
  NonExpansive4 f → NonExpansive (uncurry4 f).
Proof. apply _. Qed.

Lemma curry_ne_test{A B C : ofe} (f : A * B → C) :
  NonExpansive f → NonExpansive2 (curry f).
Proof. apply _. Qed.

Lemma curry3_ne_test{A B C D : ofe} (f : A * B * C → D) :
  NonExpansive f → NonExpansive3 (curry3 f).
Proof. apply _. Qed.

Lemma curry4_ne_test{A B C D E : ofe} (f : A * B * C * D → E) :
  NonExpansive f → NonExpansive4 (curry4 f).
Proof. apply _. Qed.

Lemma list_bind_ne_test{A B : ofe} (f : A → list B) :
  NonExpansive f → NonExpansive (mbind f : list A → list B).
Proof. apply _. Qed.

Definition big_op_test(l : list Qp) : option Qp :=
  [^op list] x ∈ l, Some x.

Lemma big_opL_should_be_eql :
  ([^op list] x ∈ (l : list (option frac)), x) =
  ([^op list] x ∈ (l : list (option ufrac)), x).
Proof. reflexivity. Qed.

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.

Lemma big_opS_should_be_eqX :
  ([^op set] x ∈ (X : gset (option frac)), x) =
  ([^op set] x ∈ (X : gset (option ufrac)), x).
Proof. reflexivity. Qed.

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/bi.v *)
From stdpp Require Import strings
From iris.bi Require Import bi plainly big_op

Lemma test_impl_persistent_1`{!Sbi PROP, !BiPersistentlyImplSiPure PROP} :
  Persistent (PROP:=PROP) (True → True).
Proof. apply _. Qed.

Lemma test_impl_persistent_2`{!Sbi PROP, !BiPersistentlyImplSiPure PROP} :
  Persistent (PROP:=PROP) (True → True → True).
Proof. apply _. Qed.

Lemma test_bi_scope{PROP : bi} : True.
Proof.

Definition big_sepM_pattern_value{PROP : bi} (m : gmap nat (nat * nat)) : PROP :=
  [∗ map] '(x,y) ∈ m, ⌜ 10 = x ⌝.

Definition big_sepM_pattern_value_tt{PROP : bi} (m : gmap nat ()) : PROP :=
  [∗ map] '() ∈ m, True.

Inductive foo:= Foo (n : nat).

Definition big_sepM_pattern_value_custom{PROP : bi} (m : gmap nat foo) : PROP :=
  [∗ map] '(Foo x) ∈ m, ⌜ 10 = x ⌝.

Definition big_sepM_pattern_key{PROP : bi} (m : gmap (nat * nat) nat) : PROP :=
  [∗ map] '(k,_) ↦ _ ∈ m, ⌜ 10 = k ⌝.

Definition big_sepM_pattern_both{PROP : bi} (m : gmap (nat * nat) (nat * nat)) : PROP :=
  [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.

Definition big_sepM2_pattern{PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP :=
  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.

Definition big_sepM_cast{PROP : bi} (m : gmap nat nat) : PROP :=
  [∗ map] (x:nat) ∈ m, ⌜ 10%Z = x ⌝.

Definition big_sepM_implicit_type{PROP : bi} (m : gmap nat nat) : PROP :=
    [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.

Lemma big_sepL_simpl{PROP : bi} {A} (Φ : A → PROP) :
  ⊢ ([∗ list] x ∈ [], Φ x).
Proof.
  simpl.

Lemma match_persistent:
    Persistent (PROP:=PROP) (∃ b : bool, if b then False else False).
  Proof. apply _. Qed.

Lemma match_affine:
    Affine (PROP:=PROP) (∃ b : bool, if b then False else False).
  Proof. apply _. Qed.

Lemma match_absorbing:
    Absorbing (PROP:=PROP) (∃ b : bool, if b then False else False).
  Proof. apply _. Qed.

Lemma match_timeless:
    Timeless (PROP:=PROP) (∃ b : bool, if b then False else False).
  Proof. apply _. Qed.

Lemma match_plain`{!Sbi PROP} :
    Plain (PROP:=PROP) (∃ b : bool, if b then False else False).
  Proof. apply _. Qed.

Lemma match_list_persistent:
    Persistent (PROP:=PROP)
      (∃ l : list nat, match l with [] => False | _ :: _ => False end).
  Proof. apply _. Qed.

Lemma pair_timeless`{!Timeless (emp%I : PROP)} (m : gset (nat * nat)) :
    Timeless (PROP:=PROP) ([∗ set] '(k1, k2) ∈ m, False).
  Proof. apply _. Qed.
  Check "match_def_unfold_fail".

Definition match_foo(b : bool) : PROP := if b then False%I else False%I.

Lemma match_def_unfold_failb :
    Persistent (match_foo b).
  Proof. Fail apply _. Abort.
(* tests/bi_ascii_parsing.v *)
Require Import Stdlib.Strings.String
Require Import iris.bi.bi
Require Import iris.bi.ascii

Local OpenScope string_scope.

Local OpenScope stdpp_scope.

Ltac pg:=
    match goal with
    | |- ?X => idtac X
    end.

Ltac foog :=
    lazymatch g with
    | |- ?T => idtac T
    | ?U |- ?T => idtac U T
    end.

Ltac bar:=
    match goal with
    | |- ?G => foo G
    end.
  Check "test1".

Lemma test1: |-@{PROP} True.
  Proof. bar. pg. Abort.
  Check "test2".

Lemma test2: False |-@{PROP} True.
  Proof. bar. pg. Abort.
(* tests/fixpoint.v *)
From iris.bi Require Import lib.fixpoint_mono
From iris.proofmode Require Import proofmode
From iris.prelude Require Import options

Definition L:= bi_least_fixpoint F.

Definition G:= bi_greatest_fixpoint F.

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.

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 *)
From iris.algebra Require Import gset stepindex_finite

Lemma test_op(X Y : gset nat) : X ⊆ Y → X ⋅ Y = Y.
Proof. set_solver. Qed.

Lemma test_included(X Y : gset nat) : X ≼ Y → X ∪ Y = Y ∧ X ∩ Y = X.
Proof. set_solver. Qed.

Lemma test_disj_included(X Y : gset nat) : GSet X ≼ GSet Y → X ∪ Y = Y ∧ X ∩ Y = X.
Proof. set_solver. Qed.

Lemma test_disj_equivn : GSet (∅ : gset nat) ≡ GSet {[n]} → False.
Proof. set_solver. Qed.

Lemma test_disj_eqn : GSet (∅ : gset nat) = GSet {[n]} → False.
Proof. set_solver. Qed.

Lemma test_disj_valid(X Y : gset nat) : ✓ (GSet X ⋅ GSet Y) → X ∩ Y = ∅.
Proof. set_solver. Qed.
(* tests/heap_lang_printing.v *)
From iris.base_logic.lib Require Import gen_inv_heap invariants
From iris.program_logic Require Export weakestpre total_weakestpre
From iris.heap_lang Require Import lang adequacy proofmode notation
From iris.heap_lang Require Import lang
From iris.prelude Require Import options

Lemma ref_print:
    True -∗ WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

Lemma wp_print_long_expr(fun1 fun2 fun3 : expr) :
    True -∗ WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
  Proof.
    iIntros "_". Show.
    wp_bind (fun1 #()). Show.
  Abort.

Lemma wp_print_long_expr(fun1 fun2 fun3 : expr) long_post :
    True -∗ WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"
    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
  Proof.
    iIntros "_". Show.
    wp_bind (fun1 #()). Show.
  Abort.

Lemma wp_print_long_expr(l1 : loc) (fun2 fun3 : expr) long_post N E_long :
    ↑N ⊆ E_long →
    inv N True -∗ WP let: "val1" := ! #l1 in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"
    @ E_long
    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
  Proof.
    iIntros (?) "Hinv". Show.
    wp_bind (! #l1)%E. Show.
    iInv "Hinv" as "_". Show.
  Abort.

Lemma texan_triple_long_expr(fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.

Lemma texan_triple_long_expr_mask(fun1 fun2 fun3 : expr) E_mask_is_long_too :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    @ E_mask_is_long_too
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.

Lemma texan_triple_long_expr_mask_post(fun1 fun2 fun3 : expr) long_post E_mask_is_long_too :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    @ E_mask_is_long_too
    {{{ (x y : val) (z : Z), RET (x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}.
  Proof. Show. Abort.
(* tests/heap_lang_printing2.v *)
From iris.proofmode Require Import proofmode
From iris.heap_lang Require Export primitive_laws notation
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Lemma vs_print(P Q : iProp Σ) :
    P ={⊤}=∗ Q.
  Proof. Show. Abort.

Lemma wp_print_long_expr(fun1 fun2 fun3 : expr) :
    True -∗ WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

Lemma texan_triple_long_expr(fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.
(* tests/heap_lang_proph.v *)
From iris.program_logic Require Export weakestpre total_weakestpre
From iris.heap_lang Require Import lang adequacy proofmode notation
From iris.prelude Require Import options

Lemma test_resolve1E (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 with "Hp"); first done.
    wp_cmpxchg_suc. iIntros "!>" (ws ->) "Hp". eauto with iFrame.
  Qed.

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.

Lemma test_resolve2E (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.

Lemma test_resolve3s 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.

Lemma test_resolve4s 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/iprop.v *)
From Stdlib Require Import Logic.Eqdep
From iris.base_logic Require Import iprop

Definition foo:=
  eq_dep
    ((Type -> Type) -> Type)
    (sigT (A:=Type -> Type)).
From iris.base_logic Require Import iprop.

Lemma bi_ofeO_iPropΣ : bi_ofeO (iPropI Σ) = iPropO Σ.
Proof. reflexivity. Qed.

Lemma bi_cofe_iPropΣ : bi_cofe (iPropI Σ) = @uPred_cofe (iResUR Σ).
Proof. reflexivity. Qed.