phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
Proof using SI. rewrite comm. apply dfrac_valid_own_r. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid_discarded : ✓ DfracDiscarded.
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid_own_discarded q :
    ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1)%Qp.
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Instance dfrac_is_op q q1 q2 :
    IsOp q q1 q2 →
    IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
(* iris/algebra/dfrac.v *)
(* Discarding a fraction is a frame preserving update. *)
Lemma dfrac_discard_update dq : dq ~~> DfracDiscarded.
Proof.
    intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
    - apply dfrac_valid_own_r.
    - apply cmra_valid_op_r.
  Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_undiscard_update : DfracDiscarded ~~>: λ k, ∃ q, k = DfracOwn q.
Proof.
    apply cmra_discrete_updateP. intros [[q'| |q']|].
    - intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
      split; first by eexists. apply dfrac_valid_own.
      rewrite Hqd Qp.add_comm -Qp.add_le_mono_l.
      by apply Qp.div_le.
    - intros _. exists (DfracOwn (1/2)); split; first by eexists.
      by apply dfrac_valid_own_discarded.
    - intros [qd Hqd]%Qp.lt_sum. exists (DfracOwn (qd/2)%Qp).
      split; first by eexists. rewrite /= /op /valid /cmra_op /cmra_valid /=.
      rewrite Hqd Qp.add_comm -Qp.add_lt_mono_l.
      by apply Qp.div_lt.
    - intros _. exists (DfracOwn 1); split; first by eexists.
      by apply dfrac_valid_own.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
(* The camera [dyn_reservation_map A] over a camera [A] extends [gmap positive
A] with a notion of "reservation tokens" for a (potentially infinite) set [E :
coPset] which represent the right to allocate a map entry at any position [k ∈
E].  Unlike [reservation_map], [dyn_reservation_map] supports dynamically
allocating these tokens, including infinite sets of them.  This is useful when
syncing the keys of this map with another API that dynamically allocates names:
we can first reserve a fresh infinite set [E] of tokens here, then allocate a
new name *in [E]* with the other API (assuming it offers the usual "allocate a
fresh name in an infinite set" API), and then use our tokens to allocate the
same name here.  In effect, we have performed synchronized allocation of the
same name across two maps, without the other API having to have dedicated
support for this.

The key connectives are [dyn_reservation_map_data k a] (the "points-to"
assertion of this map), which associates data [a : A] with a key [k : positive],
and [dyn_reservation_map_token E] (the reservation token), which says
that no data has been associated with the indices in the mask [E]. The important
properties of this camera are:

- The lemma [dyn_reservation_map_reserve] provides a frame-preserving update to
  obtain ownership of [dyn_reservation_map_token E] for some fresh infinite [E].
- The lemma [dyn_reservation_map_alloc] provides a frame preserving update to
  associate data to a key: [dyn_reservation_map_token E ~~> dyn_reservation_map_data k a]
  provided [k ∈ E] and [✓ a].

In the future, it could be interesting to generalize this map to arbitrary key
types instead of hard-coding [positive]. *)
Record dyn_reservation_map (A : Type)
:= DynReservationMap {
  dyn_reservation_map_data_proj : gmap positive A;
  dyn_reservation_map_token_proj : coPset_disj
}.
(* iris/algebra/dyn_reservation_map.v *)
Instance : Params (@DynReservationMap) 1
:= {}.
(* iris/algebra/dyn_reservation_map.v *)
Instance : Params (@dyn_reservation_map_data_proj) 1
:= {}.
(* iris/algebra/dyn_reservation_map.v *)
Instance : Params (@dyn_reservation_map_token_proj) 1
:= {}.
(* iris/algebra/dyn_reservation_map.v *)
Definition dyn_reservation_map_data {SI : sidx} {A : cmra}
    (k : positive) (a : A) : dyn_reservation_map A
:=
  DynReservationMap {[ k := a ]} ε.
(* iris/algebra/dyn_reservation_map.v *)
Definition dyn_reservation_map_token {SI : sidx} {A : cmra}
    (E : coPset) : dyn_reservation_map A
:=
  DynReservationMap ∅ (CoPset E).
(* iris/algebra/dyn_reservation_map.v *)
Instance : Params (@dyn_reservation_map_data) 3
:= {}.
(* iris/algebra/dyn_reservation_map.v *)
Definition to_reservation_map x : reservation_map A
:=
    ReservationMap (dyn_reservation_map_data_proj x) (dyn_reservation_map_token_proj x).
(* iris/algebra/dyn_reservation_map.v *)
Definition from_reservation_map (x : reservation_map A) : dyn_reservation_map A
:=
    DynReservationMap (reservation_map_data_proj x) (reservation_map_token_proj x).
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_equiv : Equiv (dyn_reservation_map A)
:= λ x y,
    dyn_reservation_map_data_proj x ≡ dyn_reservation_map_data_proj y ∧
    dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_dist : Dist (dyn_reservation_map A)
:= λ n x y,
    dyn_reservation_map_data_proj x ≡{n}≡ dyn_reservation_map_data_proj y ∧
    dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.
(* iris/algebra/dyn_reservation_map.v *)
Instance DynReservationMap_ne :
    NonExpansive2 (@DynReservationMap A).
Proof. by split. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance DynReservationMap_proper :
    Proper ((≡) ==> (=) ==> (≡)) (@DynReservationMap A).
Proof. by split. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_proj_ne :
    NonExpansive (@dyn_reservation_map_data_proj A).
Proof. by destruct 1. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_proj_proper :
    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data_proj A).
Proof. by destruct 1. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Definition dyn_reservation_map_ofe_mixin : OfeMixin (dyn_reservation_map A).
Proof.
    by apply (iso_ofe_mixin to_reservation_map).
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Canonical dyn_reservation_mapO
:=
    Ofe (dyn_reservation_map A) dyn_reservation_map_ofe_mixin.
(* iris/algebra/dyn_reservation_map.v *)
Instance DynReservationMap_discrete a b :
    Discrete a → Discrete b → Discrete (DynReservationMap a b).
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete_0. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_ofe_discrete :
    OfeDiscrete A → OfeDiscrete dyn_reservation_mapO.
Proof. intros ? [??]; apply _. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_ne i :
    NonExpansive (@dyn_reservation_map_data SI A i).
Proof. intros ? ???. rewrite /dyn_reservation_map_data. solve_proper. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_proper N :
    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data SI A N).
Proof. solve_proper. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_discrete N a :
    Discrete a → Discrete (dyn_reservation_map_data N a).
Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_token_discrete E :
    Discrete (@dyn_reservation_map_token SI A E).
Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_valid_instance : Valid (dyn_reservation_map A)
:= λ x,
    match dyn_reservation_map_token_proj x with
    | CoPset E =>
      ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
      (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
      (∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E)
    | CoPsetInvalid => False
    end.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_validN_instance : ValidN (dyn_reservation_map A)
:= λ n x,
    match dyn_reservation_map_token_proj x with
    | CoPset E =>
      ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
      (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
      (∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E)
    | CoPsetInvalid => False
    end.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_pcore_instance : PCore (dyn_reservation_map A)
:= λ x,
    Some (DynReservationMap (core (dyn_reservation_map_data_proj x)) ε).
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_op_instance : Op (dyn_reservation_map A)
:= λ x y,
    DynReservationMap (dyn_reservation_map_data_proj x ⋅ dyn_reservation_map_data_proj y)
                   (dyn_reservation_map_token_proj x ⋅ dyn_reservation_map_token_proj y).
(* iris/algebra/dyn_reservation_map.v *)
Definition dyn_reservation_map_valid_eq :
    valid = λ x, match dyn_reservation_map_token_proj x with
                 | CoPset E =>
                   ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
                   (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
                   ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
                 | CoPsetInvalid => False
                 end
:= eq_refl _.
(* iris/algebra/dyn_reservation_map.v *)
Definition dyn_reservation_map_validN_eq :
    validN = λ n x, match dyn_reservation_map_token_proj x with
                    | CoPset E =>
                      ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
                      (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
                      ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
                    | CoPsetInvalid => False
                    end
:= eq_refl _.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_included x y :
    x ≼ y ↔
      dyn_reservation_map_data_proj x ≼ dyn_reservation_map_data_proj y ∧
      dyn_reservation_map_token_proj x ≼ dyn_reservation_map_token_proj y.
Proof.
    split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (DynReservationMap z1 z2); split; auto.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_data_proj_validN n x : ✓{n} x → ✓{n} dyn_reservation_map_data_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_token_proj_validN n x : ✓{n} x → ✓{n} dyn_reservation_map_token_proj x.
Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_cmra_mixin : CmraMixin (dyn_reservation_map A).
Proof.
    apply (iso_cmra_mixin_restrict_validity from_reservation_map to_reservation_map); try done.
    - intros n [m [E|]];
        rewrite dyn_reservation_map_validN_eq reservation_map_validN_eq /=;
        naive_solver.
    - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[?[??]]; split; simplify_eq/=.
      + by rewrite -Hm.
      + split; first done. intros i. by rewrite -(dist_None n) -Hm dist_None.
    - pose 0ᵢ.
      intros [m [E|]]; rewrite dyn_reservation_map_valid_eq
        dyn_reservation_map_validN_eq /= ?cmra_valid_validN; naive_solver.
    - intros n m [r [E|]]; rewrite dyn_reservation_map_validN_eq /=;
        naive_solver eauto using cmra_validN_le.
    - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite dyn_reservation_map_validN_eq /=.
      rewrite {1}/op /cmra_op /=. case_decide; last done.
      intros [Hm [Hinf Hdisj]]; split; first by eauto using cmra_validN_op_l.
      split.
      + rewrite ->difference_union_distr_r_L in Hinf.
        eapply set_infinite_subseteq, Hinf. set_solver.
      + intros i. move: (Hdisj i). rewrite lookup_op.
        case: (m1 !! i); case: (m2 !! i); set_solver.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Canonical dyn_reservation_mapR
:=
    Cmra (dyn_reservation_map A) dyn_reservation_map_cmra_mixin.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_cmra_discrete :
    CmraDiscrete A → CmraDiscrete dyn_reservation_mapR.
Proof.
    split; first apply _.
    intros [m [E|]]; rewrite dyn_reservation_map_validN_eq dyn_reservation_map_valid_eq //=.
      by intros [?%cmra_discrete_valid ?].
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_empty_instance : Unit (dyn_reservation_map A)
:=
    DynReservationMap ε ε.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_ucmra_mixin : UcmraMixin (dyn_reservation_map A).
Proof.
    split; simpl.
    - rewrite dyn_reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. split.
      + rewrite difference_empty_L. apply top_infinite.
      + set_solver.
    - split; simpl; [by rewrite left_id|by rewrite left_id_L].
    - do 2 constructor; [apply (core_id_core _)|done].
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Canonical dyn_reservation_mapUR
:=
    Ucmra (dyn_reservation_map A) dyn_reservation_map_ucmra_mixin.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_core_id k a :
    CoreId a → CoreId (dyn_reservation_map_data k a).
Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_data_valid k a :
    ✓ (dyn_reservation_map_data k a) ↔ ✓ a.
Proof.
    rewrite dyn_reservation_map_valid_eq /= singleton_valid.
    split; first naive_solver. intros Ha.
    split; first done. split; last set_solver.
    rewrite difference_empty_L. apply top_infinite.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_token_valid E :
    ✓ (dyn_reservation_map_token E) ↔ set_infinite (⊤ ∖ E).
Proof.
    rewrite dyn_reservation_map_valid_eq /=. split; first naive_solver.
    intros Hinf. do 2 (split; first done). by left.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_data_op k a b :
    dyn_reservation_map_data k (a ⋅ b) = dyn_reservation_map_data k a ⋅ dyn_reservation_map_data k b.
Proof.
    by rewrite {2}/op /dyn_reservation_map_op_instance
      /dyn_reservation_map_data /= singleton_op left_id_L.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_data_mono k a b :
    a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Instance dyn_reservation_map_data_is_op k a b1 b2 :
    IsOp a b1 b2 →
    IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite dyn_reservation_map_data_op. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_token_union E1 E2 :
    E1 ## E2 →
    dyn_reservation_map_token (E1 ∪ E2) = dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token E2.
Proof.
    intros. by rewrite /op /dyn_reservation_map_op_instance
      /dyn_reservation_map_token /= coPset_disj_union // left_id_L.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_token_difference E1 E2 :
    E1 ⊆ E2 →
    dyn_reservation_map_token E2 = dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token (E2 ∖ E1).
Proof.
    intros. rewrite -dyn_reservation_map_token_union; last set_solver.
    by rewrite -union_difference_L.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_token_valid_op E1 E2 :
    ✓ (dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token E2) ↔
      E1 ## E2 ∧ set_infinite (⊤ ∖ (E1 ∪ E2)).
Proof.
    split.
    - rewrite dyn_reservation_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
      naive_solver.
    - intros [Hdisj Hinf]. rewrite -dyn_reservation_map_token_union //.
      apply dyn_reservation_map_token_valid. done.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_reserve (Q : dyn_reservation_map A → Prop) :
    (∀ E, set_infinite E → Q (dyn_reservation_map_token E)) →
    ε ~~>: Q.
Proof.
    intros HQ. apply cmra_total_updateP=> n [mf [Ef|]];
      rewrite left_id {1}dyn_reservation_map_validN_eq /=; last done.
    intros [Hmap [Hinf Hdisj]].
    (* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
       such that both that set [E1] and the remainder [E2] are infinite. *)
    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ (gset_to_coPset $ dom mf)))) as
        (E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
    { rewrite -difference_difference_l_L.
      by apply difference_infinite, gset_to_coPset_finite. }
    exists (dyn_reservation_map_token E1).
    split; first by apply HQ. clear HQ.
    rewrite dyn_reservation_map_validN_eq /=.
    rewrite coPset_disj_union; last set_solver.
    split; first by rewrite left_id_L. split.
    - eapply set_infinite_subseteq, HE2inf. set_solver.
    - intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
      destruct (mf !! i) as [p|] eqn:Hp; last by left.
      apply elem_of_dom_2, elem_of_gset_to_coPset in Hp. right. set_solver.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_reserve' :
    ε ~~>: λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E.
Proof. eauto using dyn_reservation_map_reserve. Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_alloc E k a :
    k ∈ E → ✓ a → dyn_reservation_map_token E ~~> dyn_reservation_map_data k a.
Proof.
    intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
    rewrite dyn_reservation_map_validN_eq /= {1}/op {1}/cmra_op /=.
    case_decide; last done.
    rewrite !left_id_L. intros [Hmf [Hinf Hdisj]]; split; last split.
    - destruct (Hdisj k) as [Hmfi|]; last set_solver.
      intros j. rewrite lookup_op.
      destruct (decide (k = j)) as [<-|].
      + rewrite Hmfi lookup_singleton_eq right_id_L. by apply cmra_valid_validN.
      + by rewrite lookup_singleton_ne // left_id_L.
    - eapply set_infinite_subseteq, Hinf. set_solver.
    - intros j. destruct (decide (k = j)); first set_solver.
      rewrite lookup_op lookup_singleton_ne //.
      destruct (Hdisj j) as [Hmfi|?]; last set_solver. rewrite Hmfi; auto.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_updateP P (Q : dyn_reservation_map A → Prop) k a :
    a ~~>: P →
    (∀ a', P a' → Q (dyn_reservation_map_data k a')) →
    dyn_reservation_map_data k a ~~>: Q.
Proof.
    intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
    rewrite dyn_reservation_map_validN_eq /= left_id_L. intros [Hmf [Hinf Hdisj]].
    destruct (Hup n (mf !! k)) as (a'&?&?).
    { move: (Hmf (k)).
      by rewrite lookup_op lookup_singleton_eq Some_op_opM. }
    exists (dyn_reservation_map_data k a'); split; first by eauto.
    rewrite /= left_id_L. split; last split.
    - intros j. destruct (decide (k = j)) as [<-|].
      + by rewrite lookup_op lookup_singleton_eq Some_op_opM.
      + rewrite lookup_op lookup_singleton_ne // left_id_L.
        move: (Hmf j). rewrite lookup_op. eauto using cmra_validN_op_r.
    - done.
    - intros j. move: (Hdisj j).
      rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
  Qed.
(* iris/algebra/dyn_reservation_map.v *)
Lemma dyn_reservation_map_update k a b :
    a ~~> b →
    dyn_reservation_map_data k a ~~> dyn_reservation_map_data k b.
Proof.
    rewrite !cmra_update_updateP. eauto using dyn_reservation_map_updateP with subst.
  Qed.
(* iris/algebra/excl.v *)
Inductive excl (A : Type)
:=
  | Excl : A → excl A
  | ExclInvalid : excl A.
(* iris/algebra/excl.v *)
Instance : Params (@Excl) 1
:= {}.
(* iris/algebra/excl.v *)
Instance : Params (@ExclInvalid) 1
:= {}.
(* iris/algebra/excl.v *)
Notation excl' A
:= (option (excl A)).
(* iris/algebra/excl.v *)
Notation Excl' x
:= (Some (Excl x)).
(* iris/algebra/excl.v *)
Notation ExclInvalid'
:= (Some ExclInvalid).
(* iris/algebra/excl.v *)
Instance maybe_Excl {A} : Maybe (@Excl A)
:= λ x,
  match x with Excl a => Some a | _ => None end.
(* iris/algebra/excl.v *)
(* Cofe *)
Inductive excl_equiv : Equiv (excl A)
:=
  | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
  | ExclInvalid_equiv : ExclInvalid ≡ ExclInvalid.
(* iris/algebra/excl.v *)
Inductive excl_dist : Dist (excl A)
:=
  | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
  | ExclInvalid_dist n : ExclInvalid ≡{n}≡ ExclInvalid.
(* iris/algebra/excl.v *)
Instance Excl_ne : NonExpansive (@Excl A).
Proof. by constructor. Qed.
(* iris/algebra/excl.v *)
Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
Proof. by constructor. Qed.
(* iris/algebra/excl.v *)
Instance Excl_inj : Inj (≡) (≡) (@Excl A).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/excl.v *)
Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/excl.v *)
Definition excl_ofe_mixin : OfeMixin (excl A).
Proof.
  apply (iso_ofe_mixin (maybe Excl)).
  - by intros [a|] [b|]; split; inversion_clear 1; constructor.
  - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
Qed.
(* iris/algebra/excl.v *)
Canonical exclO : ofe
:= Ofe (excl A) excl_ofe_mixin.
(* iris/algebra/excl.v *)
Instance excl_cofe `{!Cofe A} : Cofe exclO.
Proof.
  apply (iso_cofe (from_option Excl ExclInvalid) (maybe Excl)).
  - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
  - by intros []; constructor.
Qed.
(* iris/algebra/excl.v *)
Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclO.
Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
(* iris/algebra/excl.v *)
Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
(* iris/algebra/excl.v *)
Instance Excl_discrete a : Discrete a → Discrete (Excl a).
Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
(* iris/algebra/excl.v *)
Instance ExclInvalid_discrete : Discrete (@ExclInvalid A).
Proof. by inversion_clear 1; constructor. Qed.
(* iris/algebra/excl.v *)
(* CMRA *)
Instance excl_valid_instance : Valid (excl A)
:= λ x,
  match x with Excl _ => True | ExclInvalid => False end.
(* iris/algebra/excl.v *)
Instance excl_validN_instance : ValidN (excl A)
:= λ n x,
  match x with Excl _ => True | ExclInvalid => False end.
(* iris/algebra/excl.v *)
Instance excl_pcore_instance : PCore (excl A)
:= λ _, None.
(* iris/algebra/excl.v *)
Instance excl_op_instance : Op (excl A)
:= λ x y, ExclInvalid.
(* iris/algebra/excl.v *)
Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof.
  split; try discriminate.
  - by intros [] n; destruct 1; constructor.
  - by destruct 1; intros ?.
  - intros x; split; [done|]. by move=> /(_ 0ᵢ).
  - intros n m [?|]; simpl; auto.
  - by intros [?|] [?|] [?|]; constructor.
  - by intros [?|] [?|]; constructor.
  - by intros n [?|] [?|].
  - intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
Qed.
(* iris/algebra/excl.v *)
Canonical exclR
:= Cmra (excl A) excl_cmra_mixin.
(* iris/algebra/excl.v *)
Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
Proof. split; first apply _. by intros []. Qed.
(* iris/algebra/excl.v *)
Lemma excl_included x y : x ≼ y ↔ y = ExclInvalid.
Proof.
  split.
  - destruct x, y; intros [[] Hxy]; by inv Hxy.
  - intros ->. by exists ExclInvalid.
Qed.
(* iris/algebra/excl.v *)
Lemma excl_includedN n x y : x ≼{n} y ↔ y = ExclInvalid.
Proof.
  split.
  - destruct x, y; intros [[] Hxy]; by inv Hxy.
  - intros ->. by exists ExclInvalid.
Qed.
(* iris/algebra/excl.v *)
(* Exclusive *)
Instance excl_exclusive x : Exclusive x.
Proof. by destruct x; intros n []. Qed.
(* iris/algebra/excl.v *)
(* Option excl *)
Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.
Proof. by destruct mx. Qed.
(* iris/algebra/excl.v *)
Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
Proof. by destruct mx. Qed.
(* iris/algebra/excl.v *)
Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b ↔ a ≡{n}≡ b.
Proof.
  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
Qed.
(* iris/algebra/excl.v *)
Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
Proof.
  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
Qed.
(* iris/algebra/excl.v *)
Lemma ExclInvalid_included ea : ea ≼ ExclInvalid.
Proof. by exists ExclInvalid. Qed.
(* iris/algebra/excl.v *)
(* Functor *)
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B
:=
  match x with Excl a => Excl (f a) | ExclInvalid => ExclInvalid end.
(* iris/algebra/excl.v *)
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed.