phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/coPset.v *)
Instance coPset_disj_cmra_discrete : CmraDiscrete coPset_disjR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
(* iris/algebra/coPset.v *)
Canonical coPset_disjUR
:= Ucmra coPset_disj coPset_disj_ucmra_mixin.
(* iris/algebra/csum.v *)
Inductive csum (A B : Type)
:=
  | Cinl : A → csum A B
  | Cinr : B → csum A B
  | CsumInvalid : csum A B.
(* iris/algebra/csum.v *)
Instance : Params (@Cinl) 2
:= {}.
(* iris/algebra/csum.v *)
Instance : Params (@Cinr) 2
:= {}.
(* iris/algebra/csum.v *)
Instance : Params (@CsumInvalid) 2
:= {}.
(* iris/algebra/csum.v *)
Instance maybe_Cinl {A B} : Maybe (@Cinl A B)
:= λ x,
  match x with Cinl a => Some a | _ => None end.
(* iris/algebra/csum.v *)
Instance maybe_Cinr {A B} : Maybe (@Cinr A B)
:= λ x,
  match x with Cinr b => Some b | _ => None end.
(* iris/algebra/csum.v *)
(* Cofe *)
Inductive csum_equiv : Equiv (csum A B)
:=
  | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
  | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
  | CsumInvalid_equiv : CsumInvalid ≡ CsumInvalid.
(* iris/algebra/csum.v *)
Inductive csum_dist : Dist (csum A B)
:=
  | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
  | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
  | CsumInvalid_dist n : CsumInvalid ≡{n}≡ CsumInvalid.
(* iris/algebra/csum.v *)
Instance Cinl_ne : NonExpansive (@Cinl A B).
Proof. by constructor. Qed.
(* iris/algebra/csum.v *)
Instance Cinl_proper : Proper ((≡) ==> (≡)) (@Cinl A B).
Proof. by constructor. Qed.
(* iris/algebra/csum.v *)
Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/csum.v *)
Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_ne : NonExpansive (@Cinr A B).
Proof. by constructor. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_proper : Proper ((≡) ==> (≡)) (@Cinr A B).
Proof. by constructor. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_inj : Inj (≡) (≡) (@Cinr A B).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/csum.v *)
Definition csum_ofe_mixin : OfeMixin (csum A B).
Proof.
  split.
  - intros mx my; split.
    + by destruct 1; constructor; try apply equiv_dist.
    + intros Hxy; oinversion (Hxy 0ᵢ); subst; constructor; try done;
      apply equiv_dist=> n; by oinversion (Hxy n).
  - intros n; split.
    + by intros [|a|]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
  - inversion_clear 1; intros Hlt; constructor; eauto using dist_le.
Qed.
(* iris/algebra/csum.v *)
Canonical csumO : ofe
:= Ofe (csum A B) csum_ofe_mixin.
(* iris/algebra/csum.v *)
Definition csum_chain_l (c : chain csumO) (a : A) : chain A :=
  {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
(* iris/algebra/csum.v *)
Definition csum_chain_r (c : chain csumO) (b : B) : chain B :=
  {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
(* iris/algebra/csum.v *)
Definition csum_compl `{!Cofe A, !Cofe B} : Compl csumO
:= λ c,
  match c 0ᵢ with
  | Cinl a => Cinl (compl (csum_chain_l c a))
  | Cinr b => Cinr (compl (csum_chain_r c b))
  | CsumInvalid => CsumInvalid
  end.
(* iris/algebra/csum.v *)
Definition csum_bchain_l {α} (c : bchain csumO α) (a : A) : bchain A α :=
  {| bchain_car β Hβ := match c β Hβ return _ with Cinl a' => a' | _ => a end |}.
Next Obligation.
  intros α c a β γ Hle Hβ Hγ. simpl.
  by destruct (bchain_cauchy _ c β γ Hle Hβ Hγ).
Qed.
(* iris/algebra/csum.v *)
Definition csum_bchain_r {α} (c : bchain csumO α) (b : B) : bchain B α :=
  {| bchain_car β Hβ := match c β Hβ return _ with Cinr b' => b' | _ => b end |}.
Next Obligation.
  intros α c b β γ Hle Hβ Hγ. simpl.
  by destruct (bchain_cauchy _ c β γ Hle Hβ Hγ).
Qed.
(* iris/algebra/csum.v *)
Definition csum_lbcompl `{!Cofe A, !Cofe B} : LBCompl csumO
:= λ n Hn c,
  match c _ (SIdx.limit_lt_0 _ Hn) with
  | Cinl a => Cinl (lbcompl Hn (csum_bchain_l c a))
  | Cinr b => Cinr (lbcompl Hn (csum_bchain_r c b))
  | CsumInvalid => CsumInvalid
  end.
(* iris/algebra/csum.v *)
Instance csum_cofe `{!Cofe A, !Cofe B} : Cofe csumO :=
  {| compl := csum_compl; lbcompl := csum_lbcompl |}.
Next Obligation.
  intros ?? n c; rewrite /compl /csum_compl.
  oinversion (chain_cauchy c 0ᵢ n); first apply SIdx.le_0_l; constructor.
  - rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
  - rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
Qed.
(* iris/algebra/csum.v *)
Instance csum_ofe_discrete :
  OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumO.
Proof. by inversion_clear 3; constructor; apply (discrete_0 _). Qed.
(* iris/algebra/csum.v *)
Instance csum_leibniz :
  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumO.
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
(* iris/algebra/csum.v *)
Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
(* iris/algebra/csum.v *)
Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
Proof. by inversion_clear 2; constructor; apply (discrete_0 _). Qed.
(* iris/algebra/csum.v *)
(* Functor on COFEs *)
Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
                    (x : csum A B) : csum A' B'
:=
  match x with
  | Cinl a => Cinl (fA a)
  | Cinr b => Cinr (fB b)
  | CsumInvalid => CsumInvalid
  end.
(* iris/algebra/csum.v *)
Instance : Params (@csum_map) 4
:= {}.
(* iris/algebra/csum.v *)
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed.
(* iris/algebra/csum.v *)
Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
                       (g : B → B') (g' : B' → B'') (x : csum A B) :
  csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
Proof. by destruct x. Qed.
(* iris/algebra/csum.v *)
Lemma csum_map_ext {SI : sidx} {A A' B B' : ofe} (f f' : A → A') (g g' : B → B') x :
  (∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
Proof. by destruct x; constructor. Qed.
(* iris/algebra/csum.v *)
Instance csum_map_cmra_ne {SI : sidx} {A A' B B' : ofe} n :
  Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
         (@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
(* iris/algebra/csum.v *)
Definition csumO_map {SI : sidx} {A A' B B'} (f : A -n> A') (g : B -n> B') :
  csumO A B -n> csumO A' B'
:=
  OfeMor (csum_map f g).
(* iris/algebra/csum.v *)
Instance csumO_map_ne {SI : sidx} A A' B B' :
  NonExpansive2 (@csumO_map SI A A' B B').
Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
(* iris/algebra/csum.v *)
(* CMRA *)
Instance csum_valid_instance : Valid (csum A B)
:= λ x,
  match x with
  | Cinl a => ✓ a
  | Cinr b => ✓ b
  | CsumInvalid => False
  end.
(* iris/algebra/csum.v *)
Instance csum_validN_instance : ValidN (csum A B)
:= λ n x,
  match x with
  | Cinl a => ✓{n} a
  | Cinr b => ✓{n} b
  | CsumInvalid => False
  end.
(* iris/algebra/csum.v *)
Instance csum_pcore_instance : PCore (csum A B)
:= λ x,
  match x with
  | Cinl a => Cinl <$> pcore a
  | Cinr b => Cinr <$> pcore b
  | CsumInvalid => Some CsumInvalid
  end.
(* iris/algebra/csum.v *)
Instance csum_op_instance : Op (csum A B)
:= λ x y,
  match x, y with
  | Cinl a, Cinl a' => Cinl (a ⋅ a')
  | Cinr b, Cinr b' => Cinr (b ⋅ b')
  | _, _ => CsumInvalid
  end.
(* iris/algebra/csum.v *)
Lemma Cinl_op a a' : Cinl (a ⋅ a') = Cinl a ⋅ Cinl a'.
Proof. done. Qed.
(* iris/algebra/csum.v *)
Lemma Cinr_op b b' : Cinr (b ⋅ b') = Cinr b ⋅ Cinr b'.
Proof. done. Qed.
(* iris/algebra/csum.v *)
Lemma Cinl_valid a : ✓ (Cinl a) ↔ ✓ a.
Proof. done. Qed.
(* iris/algebra/csum.v *)
Lemma Cinr_valid b : ✓ (Cinr b) ↔ ✓ b.
Proof. done. Qed.
(* iris/algebra/csum.v *)
Lemma csum_included x y :
  x ≼ y ↔ y = CsumInvalid ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
                      ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
Proof.
  split.
  - unfold included. intros [[a'|b'|] Hy]; destruct x as [a|b|];
      inversion_clear Hy; eauto 10.
  - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
    + destruct x; exists CsumInvalid; constructor.
    + exists (Cinl c); by constructor.
    + exists (Cinr c); by constructor.
Qed.
(* iris/algebra/csum.v *)
Lemma Cinl_included a a' : Cinl a ≼ Cinl a' ↔ a ≼ a'.
Proof. rewrite csum_included. naive_solver. Qed.
(* iris/algebra/csum.v *)
Lemma Cinr_included b b' : Cinr b ≼ Cinr b' ↔ b ≼ b'.
Proof. rewrite csum_included. naive_solver. Qed.
(* iris/algebra/csum.v *)
Lemma CsumInvalid_included x : x ≼ CsumInvalid.
Proof. exists CsumInvalid. by destruct x. Qed.
(* iris/algebra/csum.v *)
(* We register a hint for [CsumInvalid_included] below. *)
Lemma csum_includedN n x y :
  x ≼{n} y ↔ y = CsumInvalid ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
                         ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼{n} b').
Proof.
  split.
  - unfold includedN. intros [[a'|b'|] Hy]; destruct x as [a|b|];
      inversion_clear Hy; eauto 10.
  - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
    + destruct x; exists CsumInvalid; constructor.
    + exists (Cinl c); by constructor.
    + exists (Cinr c); by constructor.
Qed.
(* iris/algebra/csum.v *)
Lemma csum_cmra_mixin : CmraMixin (csum A B).
Proof.
  split.
  - intros [] n; destruct 1; constructor; by ofe_subst.
  - intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
    + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
      destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
      exists (Cinl ca'); by repeat constructor.
    + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
      destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
      exists (Cinr cb'); by repeat constructor.
  - intros ? [a|b|] [a'|b'|] H; inversion_clear H; ofe_subst; done.
  - pose 0ᵢ. intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver.
  - intros n m [a|b|]; simpl; eauto using cmra_validN_le.
  - intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
  - intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm.
  - intros [a|b|] ? [=]; subst; auto.
    + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
      constructor; eauto using cmra_pcore_l.
    + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
      constructor; eauto using cmra_pcore_l.
  - intros [a|b|] ? [=]; subst; auto.
    + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
      oinversion (cmra_pcore_idemp a ca); repeat constructor; auto.
    + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
      oinversion (cmra_pcore_idemp b cb); repeat constructor; auto.
  - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
    + exists CsumInvalid. rewrite csum_included; eauto.
    + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
      destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
      exists (Cinl ca'). rewrite csum_included; eauto 10.
    + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
      destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
      exists (Cinr cb'). rewrite csum_included; eauto 10.
  - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
  - intros n [a|b|] y1 y2 Hx Hx'.
    + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'.
      destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); [done|apply (inj Cinl), Hx'|].
      exists (Cinl z1), (Cinl z2). by repeat constructor.
    + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'.
      destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); [done|apply (inj Cinr), Hx'|].
      exists (Cinr z1), (Cinr z2). by repeat constructor.
    + by exists CsumInvalid, CsumInvalid; destruct y1, y2; inversion_clear Hx'.
Qed.
(* iris/algebra/csum.v *)
Canonical csumR
:= Cmra (csum A B) csum_cmra_mixin.
(* iris/algebra/csum.v *)
Instance csum_cmra_discrete :
  CmraDiscrete A → CmraDiscrete B → CmraDiscrete csumR.
Proof.
  split; first apply _.
  by move=>[a|b|] HH /=; try apply cmra_discrete_valid.
Qed.
(* iris/algebra/csum.v *)
Instance Cinl_core_id a : CoreId a → CoreId (Cinl a).
Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_core_id b : CoreId b → CoreId (Cinr b).
Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
(* iris/algebra/csum.v *)
Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a).
Proof. by move=> H[]? =>[/H||]. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
Proof. by move=> H[]? =>[|/H|]. Qed.
(* iris/algebra/csum.v *)
Instance Cinl_cancelable a : Cancelable a → Cancelable (Cinl a).
Proof.
  move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
  constructor. by eapply (cancelableN a).
Qed.
(* iris/algebra/csum.v *)
Instance Cinr_cancelable b : Cancelable b → Cancelable (Cinr b).
Proof.
  move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
  constructor. by eapply (cancelableN b).
Qed.
(* iris/algebra/csum.v *)
Instance Cinl_id_free a : IdFree a → IdFree (Cinl a).
Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
(* iris/algebra/csum.v *)
Instance Cinr_id_free b : IdFree b → IdFree (Cinr b).
Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
(* iris/algebra/csum.v *)
(* Interaction with [option] *)
Lemma Some_csum_includedN x y n :
  Some x ≼{n} Some y ↔
    y = CsumInvalid ∨
    (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ Some a ≼{n} Some a') ∨
    (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ Some b ≼{n} Some b').
Proof.
  repeat setoid_rewrite Some_includedN. rewrite csum_includedN. split.
  - intros [Hxy|?]; [inversion Hxy|]; naive_solver.
  - naive_solver by f_equiv.
Qed.
(* iris/algebra/csum.v *)
Lemma Some_csum_included x y :
  Some x ≼ Some y ↔
    y = CsumInvalid ∨
    (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ Some a ≼ Some a') ∨
    (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ Some b ≼ Some b').
Proof.
  repeat setoid_rewrite Some_included. rewrite csum_included. split.
  - intros [Hxy|?]; [inversion Hxy|]; naive_solver.
  - naive_solver by f_equiv.
Qed.
(* iris/algebra/csum.v *)
(* Updates *)
Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 → Cinl a1 ~~> Cinl a2.
Proof.
  intros Ha n [[a|b|]|] ?; simpl in *; auto.
  - by apply (Ha n (Some a)).
  - by apply (Ha n None).
Qed.
(* iris/algebra/csum.v *)
Lemma csum_update_r (b1 b2 : B) : b1 ~~> b2 → Cinr b1 ~~> Cinr b2.
Proof.
  intros Hb n [[a|b|]|] ?; simpl in *; auto.
  - by apply (Hb n (Some b)).
  - by apply (Hb n None).
Qed.
(* iris/algebra/csum.v *)
Lemma csum_updateP_l (P : A → Prop) (Q : csum A B → Prop) a :
  a ~~>: P → (∀ a', P a' → Q (Cinl a')) → Cinl a ~~>: Q.
Proof.
  intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm.
  - destruct (Hx n (Some a')) as (c&?&?); naive_solver.
  - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
(* iris/algebra/csum.v *)
Lemma csum_updateP_r (P : B → Prop) (Q : csum A B → Prop) b :
  b ~~>: P → (∀ b', P b' → Q (Cinr b')) → Cinr b  ~~>: Q.
Proof.
  intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm.
  - destruct (Hx n (Some b')) as (c&?&?); naive_solver.
  - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
(* iris/algebra/csum.v *)
Lemma csum_updateP'_l (P : A → Prop) a :
  a ~~>: P → Cinl a ~~>: λ m', ∃ a', m' = Cinl a' ∧ P a'.
Proof. eauto using csum_updateP_l. Qed.
(* iris/algebra/csum.v *)
Lemma csum_updateP'_r (P : B → Prop) b :
  b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
Proof. eauto using csum_updateP_r. Qed.
(* iris/algebra/csum.v *)
Lemma csum_local_update_l (a1 a2 a1' a2' : A) :
  (a1,a2) ~l~> (a1',a2') → (Cinl a1,Cinl a2) ~l~> (Cinl a1',Cinl a2').
Proof.
  intros Hup n mf ? Ha1; simpl in *.
  destruct (Hup n (mf ≫= maybe Cinl)); auto.
  { by destruct mf as [[]|]; inversion_clear Ha1. }
  split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
Qed.
(* iris/algebra/csum.v *)
Lemma csum_local_update_r (b1 b2 b1' b2' : B) :
  (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2').
Proof.
  intros Hup n mf ? Ha1; simpl in *.
  destruct (Hup n (mf ≫= maybe Cinr)); auto.
  { by destruct mf as [[]|]; inversion_clear Ha1. }
  split; first done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
Qed.
(* iris/algebra/csum.v *)
(* Functor *)
Instance csum_map_cmra_morphism {SI : sidx} {A A' B B' : cmra}
    (f : A → A') (g : B → B') :
  CmraMorphism f → CmraMorphism g → CmraMorphism (csum_map f g).
Proof.
  split; try apply _.
  - intros n [a|b|]; simpl; auto using cmra_morphism_validN.
  - move=> [a|b|]=>//=; rewrite -cmra_morphism_pcore; by destruct pcore.
  - intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
Qed.
(* iris/algebra/csum.v *)
Definition csumRF {SI : sidx} (Fa Fb : rFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
|}.
Next Obligation.
  intros ? Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg;
    by apply csumO_map_ne; try apply rFunctor_map_ne.
Qed.
(* iris/algebra/csum.v *)
Instance csumRF_contractive {SI : sidx} Fa Fb :
  rFunctorContractive Fa → rFunctorContractive Fb →
  rFunctorContractive (csumRF Fa Fb).
Proof.
  intros ??? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  by apply csumO_map_ne; try apply rFunctor_map_contractive.
Qed.
(* iris/algebra/dfrac.v *)
(* An element of dfrac denotes ownership of a fraction, knowledge that a
    fraction has been discarded, or both. Note that [DfracBoth] can be written
    as [DfracOwn q ⋅ DfracDiscarded]. This should be used instead
    of [DfracBoth] which is for internal use only. *)
Inductive dfrac
:=
  | DfracOwn : Qp → dfrac
  | DfracDiscarded : dfrac
  | DfracBoth : Qp → dfrac.
(* iris/algebra/dfrac.v *)
Notation "{ dq }"
:= (dq) (in custom dfrac at level 0, dq constr).
(* iris/algebra/dfrac.v *)
Notation "□"
:= DfracDiscarded (in custom dfrac).
(* iris/algebra/dfrac.v *)
Notation "{# q }"
:= (DfracOwn q) (in custom dfrac at level 0, q constr).
(* iris/algebra/dfrac.v *)
Notation ""
:= (DfracOwn 1) (in custom dfrac).
(* iris/algebra/dfrac.v *)
Canonical dfracO
:= leibnizO dfrac.
(* iris/algebra/dfrac.v *)
Instance dfrac_inhabited : Inhabited dfrac
:= populate DfracDiscarded.
(* iris/algebra/dfrac.v *)
Instance dfrac_eq_dec : EqDecision dfrac.
Proof. solve_decision. Defined.
(* iris/algebra/dfrac.v *)
Instance dfrac_countable : Countable dfrac.
Proof.
    set (enc dq := match dq with
      | DfracOwn q => inl q
      | DfracDiscarded => inr (inl ())
      | DfracBoth q => inr (inr q)
      end).
    set (dec y := Some match y with
      | inl q => DfracOwn q
      | inr (inl ()) => DfracDiscarded
      | inr (inr q) => DfracBoth q
      end).
    refine (inj_countable enc dec _). by intros [].
  Qed.
(* iris/algebra/dfrac.v *)
Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
Proof. by injection 1. Qed.
(* iris/algebra/dfrac.v *)
Instance DfracBoth_inj : Inj (=) (=) DfracBoth.
Proof. by injection 1. Qed.
(* iris/algebra/dfrac.v *)
(* An element is valid as long as the sum of its content is less than one. *)
Instance dfrac_valid_instance : Valid dfrac
:= λ dq,
    match dq with
    | DfracOwn q => q ≤ 1
    | DfracDiscarded => True
    | DfracBoth q => q < 1
    end%Qp.
(* iris/algebra/dfrac.v *)
(* As in the fractional camera the core is undefined for elements denoting
     ownership of a fraction. For elements denoting the knowledge that a fraction has
     been discarded the core is the identity function. *)
Instance dfrac_pcore_instance : PCore dfrac
:= λ dq,
    match dq with
    | DfracOwn q => None
    | DfracDiscarded => Some DfracDiscarded
    | DfracBoth q => Some DfracDiscarded
    end.
(* iris/algebra/dfrac.v *)
(* When elements are combined, ownership is added together and knowledge of
     discarded fractions is preserved. *)
Instance dfrac_op_instance : Op dfrac
:= λ dq dp,
    match dq, dp with
    | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
    | DfracOwn q, DfracDiscarded => DfracBoth q
    | DfracOwn q, DfracBoth q' => DfracBoth (q + q')
    | DfracDiscarded, DfracOwn q' => DfracBoth q'
    | DfracDiscarded, DfracDiscarded => DfracDiscarded
    | DfracDiscarded, DfracBoth q' => DfracBoth q'
    | DfracBoth q, DfracOwn q' => DfracBoth (q + q')
    | DfracBoth q, DfracDiscarded => DfracBoth q
    | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
    end.
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid dq :
    ✓ dq ↔ match dq with
           | DfracOwn q => q ≤ 1
           | DfracDiscarded => True
           | DfracBoth q => q < 1
           end%Qp.
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p + q).
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_op_discarded :
    DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded.
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
Proof.
    rewrite Qp.lt_sum. split.
    - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
    - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
  Qed.
(* iris/algebra/dfrac.v *)
(* [dfrac] does not have a unit so reflexivity is not for granted! *)
Lemma dfrac_discarded_included :
    DfracDiscarded ≼ DfracDiscarded.
Proof. exists DfracDiscarded. done. Qed.
(* iris/algebra/dfrac.v *)
Definition dfrac_ra_mixin : RAMixin dfrac.
Proof.
    split; try apply _.
    - intros [?| |?] ? dq <-; intros [= <-]; eexists _; done.
    - intros [?| |?] [?| |?] [?| |?];
        rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
    - intros [?| |?] [?| |?];
        rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
    - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
        rewrite /op /dfrac_op_instance; done.
    - intros [?| |?] ? [= <-]; done.
    - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
        apply dfrac_discarded_included.
    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
      + apply Qp.lt_le_incl.
      + intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
  Qed.
(* iris/algebra/dfrac.v *)
Canonical dfracR
:= discreteR dfrac dfrac_ra_mixin.
(* iris/algebra/dfrac.v *)
Instance dfrac_cmra_discrete : CmraDiscrete dfracR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/dfrac.v *)
Instance dfrac_full_exclusive : Exclusive (DfracOwn 1).
Proof.
    intros [q| |q];
      rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
    - apply Qp.not_add_le_l.
    - move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
  Qed.
(* iris/algebra/dfrac.v *)
Instance dfrac_cancelable q : Cancelable (DfracOwn q).
Proof.
    apply: discrete_cancelable.
    intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
    - by destruct (Qp.add_id_free q q2).
    - by destruct (Qp.add_id_free q q1).
  Qed.
(* iris/algebra/dfrac.v *)
Instance dfrac_own_id_free q : IdFree (DfracOwn q).
Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.
(* iris/algebra/dfrac.v *)
Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
Proof. by constructor. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid_own_1 : ✓ DfracOwn 1.
Proof. done. Qed.
(* iris/algebra/dfrac.v *)
Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
Proof.
    destruct dq as [q'| |q']; [|done|].
    - apply Qp.lt_le_trans, Qp.lt_add_r.
    - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
  Qed.