algebra/coPset.v

-From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
-From iris.prelude Require Export collections coPset.
-
-(** This is pretty much the same as algebra/gset, but I was not able to
-generalize the construction without breaking canonical structures. *)
-
-Inductive coPset_disj :=
-  | CoPset : coPset → coPset_disj
-  | CoPsetBot : coPset_disj.
-
-Section coPset.
-  Arguments op _ _ !_ !_ /.
-  Canonical Structure coPset_disjC := leibnizC coPset_disj.
-
-  Instance coPset_disj_valid : Valid coPset_disj := λ X,
-    match X with CoPset _ => True | CoPsetBot => False end.
-  Instance coPset_disj_empty : Empty coPset_disj := CoPset ∅.
-  Instance coPset_disj_op : Op coPset_disj := λ X Y,
-    match X, Y with
-    | CoPset X, CoPset Y => if decide (X ⊥ Y) then CoPset (X ∪ Y) else CoPsetBot
-    | _, _ => CoPsetBot
-    end.
-  Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ∅.
-
-  Ltac coPset_disj_solve :=
-    repeat (simpl || case_decide);
-    first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto.
-
-  Lemma coPset_disj_valid_inv_l X Y :
-    ✓ (CoPset X ⋅ Y) → ∃ Y', Y = CoPset Y' ∧ X ⊥ Y'.
-  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
-  Lemma coPset_disj_union X Y : X ⊥ Y → CoPset X ⋅ CoPset Y = CoPset (X ∪ Y).
-  Proof. intros. by rewrite /= decide_True. Qed.
-  Lemma coPset_disj_valid_op X Y : ✓ (CoPset X ⋅ CoPset Y) ↔ X ⊥ Y.
-  Proof. simpl. case_decide; by split. Qed.
-
-  Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
-  Proof.
-    apply ra_total_mixin; eauto.
-    - intros [?|]; destruct 1; coPset_disj_solve.
-    - by constructor.
-    - by destruct 1.
-    - intros [X1|] [X2|] [X3|]; coPset_disj_solve.
-    - intros [X1|] [X2|]; coPset_disj_solve.
-    - intros [X|]; coPset_disj_solve.
-    - exists (CoPset ∅); coPset_disj_solve.
-    - intros [X1|] [X2|]; coPset_disj_solve.
-  Qed.
-  Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
-
-  Lemma coPset_disj_ucmra_mixin : UCMRAMixin coPset_disj.
-  Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
-  Canonical Structure coPset_disjUR :=
-    discreteUR coPset_disj coPset_disj_ra_mixin coPset_disj_ucmra_mixin.
-End coPset.

algebra/dec_agree.v

-From iris.algebra Require Export cmra.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-Local Arguments op _ _ _ !_ /.
-Local Arguments pcore _ _ !_ /.
-
-(* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type := 
-  | DecAgree : A → dec_agree A
-  | DecAgreeBot : dec_agree A.
-Arguments DecAgree {_} _.
-Arguments DecAgreeBot {_}.
-Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
-  match x with DecAgree a => Some a | _ => None end.
-
-Section dec_agree.
-Context {A : Type} `{∀ x y : A, Decision (x = y)}.
-
-Instance dec_agree_valid : Valid (dec_agree A) := λ x,
-  if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
-
-Instance dec_agree_op : Op (dec_agree A) := λ x y,
-  match x, y with
-  | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
-  | _, _ => DecAgreeBot
-  end.
-Instance dec_agree_pcore : PCore (dec_agree A) := Some.
-
-Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
-Proof.
-  split.
-  - apply _.
-  - intros x y cx ? [=<-]; eauto.
-  - apply _.
-  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] ? [=<-]; by repeat (simplify_eq/= || case_match).
-  - intros [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|] ?? [=<-]; eauto.
-  - by intros [?|] [?|] ?.
-Qed.
-
-Canonical Structure dec_agreeR : cmraT :=
-  discreteR (dec_agree A) dec_agree_ra_mixin.
-
-(* Some properties of this CMRA *)
-Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
-Proof. by constructor. Qed.
-
-Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
-Proof. intros. by rewrite /= decide_False. Qed.
-
-Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x = x.
-Proof. destruct x; by rewrite /= ?decide_True. Qed.
-
-Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
-Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
-End dec_agree.
-
-Arguments dec_agreeC : clear implicits.
-Arguments dec_agreeR _ {_}.

algebra/dra.v

-From iris.algebra Require Export cmra updates.
-
-Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
-  (* setoids *)
-  mixin_dra_equivalence : Equivalence ((≡) : relation A);
-  mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
-  mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
-  mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
-  mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
-  (* validity *)
-  mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  mixin_dra_core_valid x : ✓ x → ✓ core x;
-  (* monoid *)
-  mixin_dra_assoc : Assoc (≡) (⋅);
-  mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
-  mixin_dra_disjoint_move_l x y z :
-    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
-  mixin_dra_symmetric : Symmetric (@disjoint A _);
-  mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
-  mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
-  mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
-  mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_mono x y : 
-    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
-}.
-Structure draT := DRAT {
-  dra_car :> Type;
-  dra_equiv : Equiv dra_car;
-  dra_core : Core dra_car;
-  dra_disjoint : Disjoint dra_car;
-  dra_op : Op dra_car;
-  dra_valid : Valid dra_car;
-  dra_mixin : DRAMixin dra_car
-}.
-Arguments DRAT _ {_ _ _ _ _} _.
-Arguments dra_car : simpl never.
-Arguments dra_equiv : simpl never.
-Arguments dra_core : simpl never.
-Arguments dra_disjoint : simpl never.
-Arguments dra_op : simpl never.
-Arguments dra_valid : simpl never.
-Arguments dra_mixin : simpl never.
-Add Printing Constructor draT.
-Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
-
-(** Lifting properties from the mixin *)
-Section dra_mixin.
-  Context {A : draT}.
-  Implicit Types x y : A.
-  Global Instance dra_equivalence : Equivalence ((≡) : relation A).
-  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
-  Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
-  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
-  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
-  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
-  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
-  Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y).
-  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
-  Lemma dra_core_valid x : ✓ x → ✓ core x.
-  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
-  Global Instance dra_assoc : Assoc (≡) (@op A _).
-  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
-  Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
-  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
-  Lemma dra_disjoint_move_l x y z :
-    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z.
-  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
-  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
-  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
-  Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x.
-  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
-  Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x.
-  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
-  Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
-  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
-  Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
-  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_mono x y : 
-    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
-  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
-End dra_mixin.
-
-Record validity (A : draT) := Validity {
-  validity_car : A;
-  validity_is_valid : Prop;
-  validity_prf : validity_is_valid → valid validity_car
-}.
-Add Printing Constructor validity.
-Arguments Validity {_} _ _ _.
-Arguments validity_car {_} _.
-Arguments validity_is_valid {_} _.
-
-Definition to_validity {A : draT} (x : A) : validity A :=
-  Validity x (valid x) id.
-
-(* The actual construction *)
-Section dra.
-Context (A : draT).
-Implicit Types a b : A.
-Implicit Types x y z : validity A.
-Arguments valid _ _ !_ /.
-
-Instance validity_valid : Valid (validity A) := validity_is_valid.
-Instance validity_equiv : Equiv (validity A) := λ x y,
-  (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Instance validity_equivalence : Equivalence (@equiv (validity A) _).
-Proof.
-  split; unfold equiv, validity_equiv.
-  - by intros [x px ?]; simpl.
-  - intros [x px ?] [y py ?]; naive_solver.
-  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
-    split; [|intros; trans y]; tauto.
-Qed.
-Canonical Structure validityC : cofeT := discreteC (validity A).
-
-Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
-Proof. by split; apply: dra_valid_proper. Qed.
-Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
-Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
-Proof.
-  intros x1 x2 Hx y1 y2 Hy; split.
-  - by rewrite Hy (symmetry_iff (⊥) x1) (symmetry_iff (⊥) x2) Hx.
-  - by rewrite -Hy (symmetry_iff (⊥) x2) (symmetry_iff (⊥) x1) -Hx.
-Qed.
-
-Lemma dra_disjoint_rl a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b.
-Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c.
-Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_move_r a b c :
-  ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c.
-Proof.
-  intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
-  apply dra_disjoint_move_l; auto; by rewrite dra_comm.
-Qed.
-Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
-
-Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
-Proof. apply validity_prf. Qed.
-Hint Resolve validity_valid_car_valid.
-Program Instance validity_pcore : PCore (validity A) := λ x,
-  Some (Validity (core (validity_car x)) (✓ x) _).
-Solve Obligations with naive_solver eauto using dra_core_valid.
-Program Instance validity_op : Op (validity A) := λ x y,
-  Validity (validity_car x ⋅ validity_car y)
-           (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
-Solve Obligations with naive_solver eauto using dra_op_valid.
-
-Definition validity_ra_mixin : RAMixin (validity A).
-Proof.
-  apply ra_total_mixin; first eauto.
-  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
-    split; intros (?&?&?); split_and!;
-      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
-  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
-  - intros ?? [??]; naive_solver.
-  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
-      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |intros; by rewrite assoc].
-  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
-  - intros [x px ?]; split;
-      naive_solver eauto using dra_core_l, dra_core_disjoint_l.
-  - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
-  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
-    destruct (dra_core_mono x z) as (z'&Hz').
-    unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
-    { intros (?&?&?); apply Hz'; tauto. }
-    + tauto.
-    + intros. rewrite Hy //. tauto.
-  - by intros [x px ?] [y py ?] (?&?&?).
-Qed.
-Canonical Structure validityR : cmraT :=
-  discreteR (validity A) validity_ra_mixin.
-
-Global Instance validity_cmra_total : CMRATotal validityR.
-Proof. rewrite /CMRATotal; eauto. Qed.
-
-Lemma validity_update x y :
-  (∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
-Proof.
-  intros Hxy; apply cmra_discrete_update=> z [?[??]].
-  split_and!; try eapply Hxy; eauto.
-Qed.
-
-Lemma to_validity_op a b :
-  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) →
-  to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
-Proof. split; naive_solver eauto using dra_op_valid. Qed.
-
-(* TODO: This has to be proven again. *)
-(*
-Lemma to_validity_included x y:
-  (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
-Proof.
-  split.
-  - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
-    destruct Hvl' as [? [? ?]]; split; first done.
-    exists (validity_car z); eauto.
-  - intros (Hvl & z & EQ & ? & ?).
-    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
-    split; first done. exists (to_validity z). split; first split.
-    + intros _. simpl. by split_and!.
-    + intros _. setoid_subst. by apply dra_op_valid. 
-    + intros _. rewrite /= EQ //.
-Qed.
-*)
-End dra.

algebra/frac.v

-From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
-
-Notation frac := Qp (only parsing).
-
-Section frac.
-Canonical Structure fracC := leibnizC frac.
-
-Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
-Instance frac_pcore : PCore frac := λ _, None.
-Instance frac_op : Op frac := λ x y, (x + y)%Qp.
-
-Definition frac_ra_mixin : RAMixin frac.
-Proof.
-  split; try apply _; try done.
-  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
-  rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
-Qed.
-Canonical Structure fracR := discreteR frac frac_ra_mixin.
-End frac.
-
-(** Internalized properties *)
-Lemma frac_equivI {M} (x y : frac) : x ≡ y ⊣⊢ (x = y : uPred M).
-Proof. by uPred.unseal. Qed.
-Lemma frac_validI {M} (x : frac) : ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M).
-Proof. by uPred.unseal. Qed.
-
-(** Exclusive *)
-Global Instance frac_full_exclusive : Exclusive 1%Qp.
-Proof.
-  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
-Qed.

algebra/gset.v

-From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
-From iris.prelude Require Export collections gmap.
-
-Inductive gset_disj K `{Countable K} :=
-  | GSet : gset K → gset_disj K
-  | GSetBot : gset_disj K.
-Arguments GSet {_ _ _} _.
-Arguments GSetBot {_ _ _}.
-
-Section gset.
-  Context `{Countable K}.
-  Arguments op _ _ !_ !_ /.
-
-  Canonical Structure gset_disjC := leibnizC (gset_disj K).
-
-  Instance gset_disj_valid : Valid (gset_disj K) := λ X,
-    match X with GSet _ => True | GSetBot => False end.
-  Instance gset_disj_empty : Empty (gset_disj K) := GSet ∅.
-  Instance gset_disj_op : Op (gset_disj K) := λ X Y,
-    match X, Y with
-    | GSet X, GSet Y => if decide (X ⊥ Y) then GSet (X ∪ Y) else GSetBot
-    | _, _ => GSetBot
-    end.
-  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ∅.
-
-  Ltac gset_disj_solve :=
-    repeat (simpl || case_decide);
-    first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.
-
-  Lemma gset_disj_valid_inv_l X Y : ✓ (GSet X ⋅ Y) → ∃ Y', Y = GSet Y' ∧ X ⊥ Y'.
-  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
-  Lemma gset_disj_union X Y : X ⊥ Y → GSet X ⋅ GSet Y = GSet (X ∪ Y).
-  Proof. intros. by rewrite /= decide_True. Qed.
-  Lemma gset_disj_valid_op X Y : ✓ (GSet X ⋅ GSet Y) ↔ X ⊥ Y.
-  Proof. simpl. case_decide; by split. Qed.
-
-  Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
-  Proof.
-    apply ra_total_mixin; eauto.
-    - intros [?|]; destruct 1; gset_disj_solve.
-    - by constructor.
-    - by destruct 1.
-    - intros [X1|] [X2|] [X3|]; gset_disj_solve.
-    - intros [X1|] [X2|]; gset_disj_solve.
-    - intros [X|]; gset_disj_solve.
-    - exists (GSet ∅); gset_disj_solve.
-    - intros [X1|] [X2|]; gset_disj_solve.
-  Qed.
-  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.
-
-  Lemma gset_disj_ucmra_mixin : UCMRAMixin (gset_disj K).
-  Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
-  Canonical Structure gset_disjUR :=
-    discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.
-
-  Arguments op _ _ _ _ : simpl never.
-
-  Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
-    (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
-    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
-  Proof.
-    intros Hfresh HQ.
-    apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
-    destruct (Hfresh (X ∪ Y)) as (i&?&?); first set_solver.
-    exists (GSet ({[ i ]} ∪ X)); split.
-    - apply HQ; set_solver by eauto.
-    - apply gset_disj_valid_op. set_solver by eauto.
-  Qed.
-  Lemma gset_alloc_updateP_strong' P X :
-    (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
-    GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i.
-  Proof. eauto using gset_alloc_updateP_strong. Qed.
-
-  Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
-    (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
-    (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q.
-  Proof.
-    intros. apply (gset_alloc_updateP_strong P); eauto.
-    intros i; rewrite right_id_L; auto.
-  Qed.
-  Lemma gset_alloc_empty_updateP_strong' P :
-    (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
-    GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i.
-  Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
-
-  Section fresh_updates.
-    Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-
-    Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
-      (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
-    Proof.
-      intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
-      intros Y ?; exists (fresh Y); eauto using is_fresh.
-    Qed.
-    Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
-    Proof. eauto using gset_alloc_updateP. Qed.
-
-    Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) :
-      (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
-    Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
-    Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
-    Proof. eauto using gset_alloc_empty_updateP. Qed.
-  End fresh_updates.
-
-  Lemma gset_alloc_local_update X i Xf :
-    i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
-  Proof.
-    intros ??; apply local_update_total; split; simpl.
-    - rewrite !gset_disj_valid_op; set_solver.
-    - intros mZ ?%gset_disj_valid_op HXf.
-      rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
-  Qed.
-  Lemma gset_alloc_empty_local_update i Xf :
-    i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf).
-  Proof.
-    intros. rewrite -(right_id_L _ _ {[i]}).
-    apply gset_alloc_local_update; set_solver.
-  Qed.
-End gset.
-
-Arguments gset_disjR _ {_ _}.
-Arguments gset_disjUR _ {_ _}.

benchmark/.gitignore

-__pycache__
-build-times.log*
-gitlab-extract