ReactorJet/Coq-Iris huggingface dataset:
(* tests/iris_notation.v *)
From iris.algebra Require Import frac
From iris.proofmode Require Import proofmode monpred
From iris.base_logic Require Import base_logic lib.fancy_updates

Definition use_bupd_uPred(n : nat) : uPred M :=
    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.

Definition use_plainly_uPred(n : nat) : uPred M :=
    ■ |==> ∃ m : nat , ⌜ n = 2 ⌝.

Definition big_op_scope_uPred_1(xs : list nat) : uPred M :=
    [∗ list] _ ↦ x ∈ xs, True.

Definition big_op_scope_uPred_2(xs : list nat) : uPred M :=
    [∗ list] x; y ∈ xs; xs, True.

Definition big_op_scope_uPred_3(m : gmap nat nat) : uPred M :=
    [∗ map] _ ↦ x ∈ m, True.

Definition big_op_scope_uPred_4(m : gmap nat nat) : uPred M :=
    [∗ map] x; y ∈ m; m, True.

Definition use_bupd_iProp(n : nat) : iProp Σ :=
    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.

Definition use_fupd_iProp(n : nat) : iProp Σ :=
    □ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.

Definition big_op_scope_iProp_1(xs : list nat) : iProp Σ :=
    [∗ list] _ ↦ x ∈ xs, True.

Definition big_op_scope_iProp_2(xs : list nat) : iProp Σ :=
    [∗ list] x; y ∈ xs; xs, True.

Definition big_op_scope_iProp_3(m : gmap nat nat) : iProp Σ :=
    [∗ map] _ ↦ x ∈ m, True.

Definition big_op_scope_iProp_4(m : gmap nat nat) : iProp Σ :=
    [∗ map] x; y ∈ m; m, True.
(* tests/later_credits_paper.v *)
From iris.proofmode Require Import proofmode
From iris.base_logic Require Import invariants ghost_var
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Lemma mini_later_credits_example`{!heapGS Σ} N (f : val) l :

Lemma nested_invariants_example`{!heapGS Σ} `{!ghost_varG Σ loc} γ (l : loc) :
(* tests/list_reverse.v *)
From iris.proofmode Require Export proofmode
From iris.program_logic Require Export total_weakestpre weakestpre
From iris.heap_lang Require Export lang
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

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.

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.

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

Lemma rev_wphd 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 *)
From iris.heap_lang Require Import proofmode notation adequacy lib.spin_lock
From iris.prelude Require Import options

Definition lock_client_gen: expr :=
    let: "l" := ref #10 in
    let: "lock" := newlock #() in
    acquire "lock";;
    "l" <- #42;;
    release "lock".

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.

Local ExistingInstance spin_lock.

Definition lock_client_spin: expr :=
    let: "l" := ref #10 in
    let: "lock" := newlock #() in
    acquire "lock";;
    "l" <- #42;;
    release "lock".

Lemma wp_lock_client_spin`{!heapGS Σ, !spin_lockG Σ} :
    ⊢ WP lock_client_spin {{ _, True }}.
  Proof.
    unfold lock_client_spin.

Local ExistingInstance spin_lock.

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.

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 *)
From stdpp Require Import strings
From iris.base_logic Require Import bi
From iris.bi Require Import embedding monpred

Local NotationmonPred := (monPred I (uPredI M)).
  Check "monPred_unseal_test_1".

Lemma monPred_unseal_test_1P Q (R : monPred) :
    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
  Proof.
    intros. split=> i. monPred.unseal.

Lemma monPred_unseal_test_2P Q (R : monPred) :
    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
  Proof.
    uPred.unseal.
(* tests/mosel_paper.v *)
From iris.bi Require Import monpred
From iris.proofmode Require Import proofmode monpred
From iris.prelude Require Import options

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.

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.

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.

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.

Lemma example_4{PROP : bi} {A : Type} (P Q : PROP) : □ P ∧ □ Q -∗ □ (P ∗ Q).
Proof. iIntros "[#HP #HQ]". Show. iModIntro. iSplitL; iAssumption. Qed.

Lemma example_monpred{I PROP} (Φ Ψ : monPred I PROP) : Φ ∗ (Φ -∗ Ψ) ⊢ Ψ.
Proof. iIntros "[H1 H2]". Show. iApply "H2". iAssumption. Qed.

Lemma example_monpred_model{I PROP} (Φ Ψ : monPred I PROP) : Φ ∗ (Φ -∗ Ψ) ⊢ Ψ.
Proof. iStartProof PROP. Show. iIntros (i) "[H1 H2]". iApply "H2". iAssumption. Qed.

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 *)
From stdpp Require Import propset gmap strings
From iris Require Import algebra.mra

Notation gset_mraK:= (mra (⊆@{gset K})).

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.

Notation propset_mraK := (mra (⊆@{propset K})).

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/proofmode_siprop.v *)
From iris.proofmode Require Import proofmode
From iris.si_logic Require Import bi
From iris.prelude Require Import options

Lemma test_everything_persistentP : P -∗ P.
  Proof. by iIntros "#HP". Qed.

Lemma test_everything_affineP : P -∗ True.
  Proof. by iIntros "_". Qed.

Lemma test_iIntro_implP Q R : ⊢ P → Q ∧ R → P ∧ R.
  Proof. iIntros "#HP #[HQ HR]". auto. Qed.

Lemma test_iApply_impl_1P Q R : ⊢ P → (P → Q) → Q.
  Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.

Lemma test_iApply_impl_2P Q R : ⊢ P → (P → Q) → Q.
  Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
(* tests/sbi_unfold.v *)
From stdpp Require Import strings
From iris.bi Require Import bi

Lemma test_impl{A : ofe} (x y z : A) :
    x ≡ y ⊢@{PROP} y ≡ z → x ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_impl_impl_and".

Lemma test_impl_impl_and{A : ofe} (x y z : A) :
    ⊢@{PROP} x ≡ y → y ≡ z → x ≡ z ∧ z ≡ x.
  Proof. sbi_unfold. Show. Abort.
  Check "test_exist_impl".

Lemma test_exist_impl{A : ofe} (x z : A) :
    ⊢@{PROP} (∃ y, x ≡ y ∧ y ≡ z) → x ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_exist_impl".

Lemma test_exist_impl{A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z → ∃ y, x ≡ y ∧ y ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_si_pure_exist".

Lemma test_si_pure_exist{A : ofe} (x z : A) :
    ⊢@{PROP} <si_pure> (∃ y, <si_pure> (x ≡ y) ∧ y ≡ z) → x ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_equiv_exist".

Lemma test_iff_exist{A : ofe} (x z : A) :
    x ≡ z ⊣⊢@{PROP} ∃ y, x ≡ y ∧ y ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_iff_exist".

Lemma test_iff_exist{A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z ↔ ∃ y, x ≡ y ∧ y ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_wand_iff_exist".

Lemma test_iff_exist{A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z ∗-∗ ∃ y, x ≡ y ∧ y ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_wand_iff_exist".

Lemma test_iff_exist_later{A : ofe} (x z : A) :
    ⊢@{PROP} ▷ (x ≡ z) ∗-∗ ∃ y, ▷ (x ≡ y ∧ y ≡ z).
  Proof. sbi_unfold. Show. Abort.

Lemma test_exist_impl{A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z → ∃ y, x ≡ y → y ≡ z.
  Proof. sbi_unfold. Show. Abort.
  Check "test_forall_impl".

Lemma test_forall_impl{A : ofe} (x z : A) :
    ⊢@{PROP} (∀ y, x ≡ y → y ≡ z) → x ≡ z.
  Proof. sbi_unfold. Show. Abort.
(* tests/siprop.v *)
From stdpp Require Import strings
From iris.si_logic Require Import bi

Lemma unseal_test(P Q : siProp) (Φ : nat → siProp) :
  P ∧ ▷ Q ∧ (∃ x, Φ x) ⊣⊢ ∃ x, P ∗ ▷ Q ∧ emp ∨ Φ x.
Proof.
  siProp.unseal.
  Show.
Abort.

Definition test: siProp := ▷ True.

Definition testI: siPropI := ▷ True.
(* tests/string_ident.v *)
From iris.proofmode Require Import string_ident
From Stdlib Require Import Strings.String
From stdpp Require Import base

Local OpenScope string.

Lemma test_basic_ident: ∀ (n:nat), n = n.
Proof.
  let x := fresh in intros x; rename_by_string x "n".
  exact (eq_refl n).
Qed.
Check "test_invalid_ident".

Lemma test_invalid_ident: ∀ (n:nat), True.
Proof.
  Fail let x := fresh in intros x; rename_by_string x "has a space".
Abort.
Check "test_not_string".

Lemma test_not_string: ∀ (n:nat), True.
Proof.
  Fail let x := fresh in intros x; rename_by_string x 4.
Abort.
Check "test_not_literal".

Lemma test_not_literal(s:string) : ∀ (n:nat), True.
Proof.
  Fail let x := fresh in intros x; rename_by_string x s.
Abort.
Check "test_string_to_ident_not_fresh".

Lemma test_string_to_ident_not_fresh(n:nat) : ∀ (n:nat), nat.
Proof.
(* tests/tree_sum.v *)
From iris.proofmode Require Export proofmode
From iris.program_logic Require Export weakestpre total_weakestpre
From iris.heap_lang Require Export lang
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Inductive tree:=
  | leaf : Z → tree
  | node : tree → tree → tree.

Fixpoint is_tree`{!heapGS Σ} (v : val) (t : tree) : iProp Σ :=
  match t with
  | leaf n => ⌜v = InjLV #n⌝
  | node tl tr =>
     ∃ (ll lr : loc) (vl vr : val),
       ⌜v = InjRV (#ll,#lr)⌝ ∗ ll ↦ vl ∗ is_tree vl tl ∗ lr ↦ vr ∗ is_tree vr tr
  end%I.

Fixpoint sum(t : tree) : Z :=
  match t with
  | leaf n => n
  | node tl tr => sum tl + sum tr
  end.

Definition sum_loop: val :=
  rec: "sum_loop" "t" "l" :=
    match: "t" with
      InjL "n" => "l" <- "n" + !"l"
    | InjR "tt" => "sum_loop" !(Fst "tt") "l" ;; "sum_loop" !(Snd "tt") "l"
    end.

Definition sum': val := λ: "t",
  let: "l" := ref #0 in
  sum_loop "t" "l";;
  !"l".

Lemma sum_loop_wp`{!heapGS Σ} v t l (n : Z) :
  [[{ l ↦ #n ∗ is_tree v t }]]
    sum_loop v #l
  [[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]].
Proof.
  iIntros (Φ) "[Hl Ht] HΦ".
  iInduction t as [n'|tl IHl tr IHr] forall (v l n Φ); simpl; wp_rec; wp_let.
  - iDestruct "Ht" as "%"; subst.
    wp_load. wp_store.
    by iApply ("HΦ" with "[$Hl]").
  - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
    wp_load. wp_apply ("IHl" with "Hl Htl"). iIntros "[Hl Htl]".
    wp_load. wp_apply ("IHr" with "Hl Htr"). iIntros "[Hl Htr]".
    iApply "HΦ". iSplitL "Hl".
    { by replace (sum tl + sum tr + n)%Z with (sum tr + (sum tl + n))%Z by lia. }
    iExists ll, lr, vl, vr. by iFrame.
Qed.

Lemma sum_wp`{!heapGS Σ} v t :
  [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
Proof.
  iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
  wp_lam. wp_alloc l as "Hl".
  wp_smart_apply (sum_loop_wp with "[$Hl $Ht]").
  rewrite Z.add_0_r.
  iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
Qed.
(* iris/algebra/cmra_big_op.v *)
From stdpp Require Import gmap gmultiset
From iris.algebra Require Export big_op cmra
From iris.prelude Require Import options

Lemma big_opL_None{SI : sidx} {M : cmra} {A} (f : nat → A → option M) l :
  ([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
Proof.
  revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
  - intros [??] [|k] y ?; naive_solver.
  - intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
Qed.

Lemma big_opM_None{SI : sidx}
    {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
  ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
Proof.
  induction m as [|i x m ? IH] using map_ind=> /=.
  { by rewrite big_opM_empty. }
  rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
  { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
  intros Hm; split.
  - apply (Hm i). by simplify_map_eq.
  - intros k y ?. apply (Hm k). by simplify_map_eq.
Qed.

Lemma big_opS_None{SI : sidx} {M : cmra} `{Countable A} (f : A → option M) X :
  ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
  induction X as [|x X ? IH] using set_ind_L.
  { by rewrite big_opS_empty. }
  rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
Qed.

Lemma big_opMS_None{SI : sidx} {M : cmra} `{Countable A} (f : A → option M) X :
  ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
  induction X as [|x X IH] using gmultiset_ind.
  { rewrite big_opMS_empty. multiset_solver. }
  rewrite -None_equiv_eq big_opMS_disj_union big_opMS_singleton None_equiv_eq op_None IH.
  multiset_solver.
Qed.
(* iris/algebra/frac.v *)
From iris.algebra Require Export cmra
From iris.algebra Require Import proofmode_classes
From iris.prelude Require Import options

Notation frac:= Qp (only parsing).

Local Instancefrac_valid_instance : Valid frac := λ x, (x ≤ 1)%Qp.

Local Instancefrac_pcore_instance : PCore frac := λ _, None.

Local Instancefrac_op_instance : Op frac := λ x y, (x + y)%Qp.

Lemma frac_validp : ✓ p ↔ (p ≤ 1)%Qp.
  Proof. done. Qed.

Lemma frac_valid_1: ✓ 1%Qp.
  Proof. done. Qed.

Lemma frac_opp q : p ⋅ q = (p + q)%Qp.
  Proof. done. Qed.

Lemma frac_includedp q : p ≼ q ↔ (p < q)%Qp.
  Proof. by rewrite Qp.lt_sum. Qed.
  Corollary frac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
  Proof. rewrite frac_included. apply Qp.lt_le_incl. Qed.

Definition frac_ra_mixin: RAMixin frac.
  Proof.
    split; try apply _; try done.
    intros p q. rewrite !frac_valid frac_op=> ?.
    trans (p + q)%Qp; last done. apply Qp.le_add_l.
  Qed.
  Canonical Structure fracR := discreteR frac frac_ra_mixin.

Global Instancefrac_cmra_discrete : CmraDiscrete fracR.
  Proof. apply discrete_cmra_discrete. Qed.

Global Instancefrac_full_exclusive : Exclusive 1%Qp.
  Proof. intros p. apply Qp.not_add_le_l. Qed.

Global Instancefrac_cancelable (q : frac) : Cancelable q.
  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.

Global Instancefrac_id_free (q : frac) : IdFree q.
  Proof. intros p _. apply Qp.add_id_free. Qed.

Global Instancefrac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
  Proof. done. Qed.

Global Instanceis_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
  Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
(* iris/algebra/monoid.v *)
From iris.algebra Require Export ofe
From iris.prelude Require Import options

Class MonoidOps{M} (o : M → M → M) (u : M) := {}.

Global HintMode MonoidOps - ! - : typeclass_instances.

Class Monoid{SI : sidx} {M : ofe} (o : M → M → M) (u : M) := {
  monoid_ne : NonExpansive2 o;
  monoid_assoc : Assoc (≡) o;
  monoid_comm : Comm (≡) o;
  monoid_left_id : LeftId (≡) u o;
}.

Global HintMode Monoid - ! ! - : typeclass_instances.

Global Instancemonoid_ops {SI : sidx} `{Monoid M o u} : MonoidOps o u := {}.

Lemma monoid_proper{SI : sidx} `{Monoid M o u} : Proper ((≡) ==> (≡) ==> (≡)) o.
Proof. apply ne_proper_2, monoid_ne. Qed.

Lemma monoid_right_id{SI : sidx} `{Monoid M o u} : RightId (≡) u o.
Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.

Class WeakMonoidHomomorphism{SI : sidx} {M1 M2 : ofe}
    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) {u1 u2} `{!Monoid o1 u1, !Monoid o2 u2}
    (R : relation M2) (f : M1 → M2) := {
  monoid_homomorphism_rel_po : PreOrder R;
  monoid_homomorphism_rel_proper : Proper ((≡) ==> (≡) ==> iff) R;
  monoid_homomorphism_op_proper : Proper (R ==> R ==> R) o2;
  monoid_homomorphism_ne : NonExpansive f;
  monoid_homomorphism x y : R (f (o1 x y)) (o2 (f x) (f y))
}.

Class MonoidHomomorphism{SI : sidx} {M1 M2 : ofe}
    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) {u1 u2} `{!Monoid o1 u1, !Monoid o2 u2}
    (R : relation M2) (f : M1 → M2) := {
  #[global] monoid_homomorphism_weak :: WeakMonoidHomomorphism o1 o2 R f;
  monoid_homomorphism_unit : R (f u1) u2
}.

Lemma weak_monoid_homomorphism_proper{SI : sidx}
  `{WeakMonoidHomomorphism M1 M2 o1 o2 u1 u2 R f} : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, monoid_homomorphism_ne. Qed.
(* iris/algebra/proofmode_classes.v *)
From iris.algebra Require Export cmra
From iris.prelude Require Import options

Class IsOp{SI : sidx} {A : cmra} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.

Global Argumentsis_op {_ _} _ _ _ {_}.

Global HintMode IsOp - + - - - : typeclass_instances.

Global Instanceis_op_op {SI : sidx} {A : cmra} (a b : A) : IsOp (a ⋅ b) a b | 100.
Proof. by rewrite /IsOp. Qed.

Class IsOp'{SI : sidx} {A : cmra} (a b1 b2 : A) :=
  #[global] is_op' :: IsOp a b1 b2.

Global HintMode IsOp' - + ! - - : typeclass_instances.

Global HintMode IsOp' - + - ! ! : typeclass_instances.

Class IsOp'LR{SI : sidx} {A : cmra} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.

Global ExistingInstance is_op_lr | 0.

Global HintMode IsOp'LR - + ! - - : typeclass_instances.

Global Instanceis_op_lr_op {SI : sidx} {A : cmra} (a b : A) : IsOp'LR (a ⋅ b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.

Global Instanceis_op_pair {SI : sidx} {A B : cmra} (a b1 b2 : A) (a' b1' b2' : B) :
  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.

Global Instanceis_op_pair_core_id_l {SI : sidx} {A B : cmra} (a : A) (a' b1' b2' : B) :
  CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.

Global Instanceis_op_pair_core_id_r {SI : sidx} {A B : cmra} (a b1 b2 : A) (a' : B) :
  CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.

Global Instanceis_op_Some {SI : sidx} {A : cmra} (a : A) b1 b2 :
  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
(* iris/algebra/stepindex_finite.v *)
From iris.algebra Require Import stepindex ofe cmra
From iris.prelude Require Import options

Lemma nat_sidx_mixin: SIdxMixin lt le 0 S.
Proof.
  constructor; try lia.
  - apply _.
  - exact lt_wf.
  - intros m n. destruct (lt_eq_lt_dec m n); naive_solver.
  - intros [|n]; eauto with lia.
Qed.

Global ExistingInstance natSI | 0.

Global Instancenat_sidx_finite : SIdxFinite natSI.
Proof. intros [|n]; eauto. Qed.

Local SetDefault Proof Using "Type*".

Lemma dist_later_S{A : ofe} (n : nat) (a b : A) :
    a ≡{n}≡ b ↔ dist_later (S n) a b.
  Proof. apply dist_later_S. Qed.

Lemma dist_S{A : ofe} n (x y : A) : x ≡{S n}≡ y → x ≡{n}≡ y.
  Proof. apply dist_S. Qed.

Lemma dist_le{A : ofe} (n m : nat) (x y : A) :
    x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y.
  Proof. by apply dist_le. Qed.

Lemma contractive_S{A B : ofe} (f : A → B) `{!Contractive f} (n : nat) x y :
    x ≡{n}≡ y → f x ≡{S n}≡ f y.
  Proof. by apply contractive_S. Qed.

Lemma conv_compl_S`{!Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
  Proof. apply conv_compl_S. Qed.

Lemma cmra_validN_S{A : cmra} n (x : A) : ✓{S n} x → ✓{n} x.
  Proof. intros ?. by eapply cmra_validN_lt, SIdx.lt_succ_diag_r. Qed.

Lemma cmra_includedN_S{A : cmra} n (x y : A) : x ≼{S n} y → x ≼{n} y.
  Proof. apply cmra_includedN_S. Qed.

Definition dist_later_fin{A : ofe} (n : nat) (x y : A) :=
    match n with 0 => True | S n => x ≡{n}≡ y end.

Lemma dist_later_fin_iff{A : ofe} (n : nat) (x y : A):
    dist_later n x y ↔ dist_later_fin n x y.
  Proof.
    destruct n; unfold dist_later_fin; first by split; eauto using dist_later_0.
    by rewrite dist_later_S.
  Qed.

Lemma ofe_mixin_finiteA `{!Equiv A, !Dist A} :
    (∀ x y : A, x ≡ y ↔ ∀ n, x ≡{n}≡ y) →
    (∀ n, Equivalence (@dist natSI A _ n)) →
    (∀ n (x y : A), x ≡{S n}≡ y → x ≡{n}≡ y) →
    OfeMixin A.
  Proof.
    intros; split; [done..|].
    intros n m x y Heq Hlt. induction Hlt; eauto.
  Qed.

Program Definitioncofe_finite {A} (compl : Compl A)
      (conv_compl: ∀ n c, compl c ≡{n}≡ c n) : Cofe A :=
    {| compl := compl; lbcompl n Hn := False_rect _ (SIdx.limit_finite _ Hn) |}.
  Next Obligation. auto. Qed.
  Next Obligation. intros. simpl. by destruct (SIdx.limit_finite _ _). Qed.
  Next Obligation. intros. simpl. by destruct (SIdx.limit_finite _ _). Qed.

Ltac dist_later_fin_intro:=
  match goal with
  | |- @dist_later _ ?A _ ?n ?x ?y =>
      apply dist_later_fin_iff;
      destruct n as [|n]; [exact I|change (@dist natSI A _ n x y)]
  end.
Tactic Notation "f_contractive_fin" :=
  f_contractive_prepare;
  try dist_later_fin_intro;
  try fast_reflexivity.
(* iris/algebra/ufrac.v *)
From iris.algebra Require Export cmra
From iris.algebra Require Import proofmode_classes
From iris.prelude Require Import options

Definition ufrac:= Qp.

Local Instanceufrac_valid_instance : Valid ufrac := λ x, True.

Local Instanceufrac_pcore_instance : PCore ufrac := λ _, None.

Local Instanceufrac_op_instance : Op ufrac := λ x y, (x + y)%Qp.

Lemma ufrac_opp q : p ⋅ q = (p + q)%Qp.
  Proof. done. Qed.

Lemma ufrac_includedp q : p ≼ q ↔ (p < q)%Qp.
  Proof. by rewrite Qp.lt_sum. Qed.
  Corollary ufrac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
  Proof. rewrite ufrac_included. apply Qp.lt_le_incl. Qed.

Definition ufrac_ra_mixin: RAMixin ufrac.
  Proof. split; try apply _; try done. Qed.
  Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.

Global Instanceufrac_cmra_discrete : CmraDiscrete ufracR.
  Proof. apply discrete_cmra_discrete. Qed.

Global Instanceufrac_cancelable q : Cancelable q.
  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.

Global Instanceufrac_id_free q : IdFree q.
  Proof. intros p _. apply Qp.add_id_free. Qed.

Global Instanceis_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
  Proof. by rewrite /IsOp' /IsOp ufrac_op Qp.div_2. Qed.