phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/cmra.v *)
Lemma prod_pcore_Some (x cx : A * B) :
    pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.2).
Proof. destruct x, cx; by intuition simplify_option_eq. Qed.
(* iris/algebra/cmra.v *)
Lemma prod_pcore_Some' (x cx : A * B) :
    pcore x ≡ Some cx ↔ pcore (x.1) ≡ Some (cx.1) ∧ pcore (x.2) ≡ Some (cx.2).
Proof.
    split; [by intros (cx'&[-> ->]%prod_pcore_Some&<-)%Some_equiv_eq|].
    rewrite {3}/pcore /prod_pcore_instance. (* TODO: use setoid rewrite *)
    intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
    by constructor.
  Qed.
(* iris/algebra/cmra.v *)
Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
Proof.
    split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
  Qed.
(* iris/algebra/cmra.v *)
Lemma prod_includedN (x y : A * B) n : x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2.
Proof.
    split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
  Qed.
(* iris/algebra/cmra.v *)
Definition prod_cmra_mixin : CmraMixin (A * B).
Proof.
    split; try apply _.
    - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
    - intros n x y cx; setoid_rewrite prod_pcore_Some=> -[??] [??].
      destruct (cmra_pcore_ne n (x.1) (y.1) (cx.1)) as (z1&->&?); auto.
      destruct (cmra_pcore_ne n (x.2) (y.2) (cx.2)) as (z2&->&?); auto.
      exists (z1,z2); repeat constructor; auto.
    - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
    - intros n m x [??]; split; by eapply cmra_validN_le.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
    - intros x y [??]%prod_pcore_Some;
        constructor; simpl; eauto using cmra_pcore_l.
    - intros x y; rewrite prod_pcore_Some prod_pcore_Some'.
      naive_solver eauto using cmra_pcore_idemp.
    - intros x y cx; rewrite prod_included prod_pcore_Some=> -[??] [??].
      destruct (cmra_pcore_mono (x.1) (y.1) (cx.1)) as (z1&?&?); auto.
      destruct (cmra_pcore_mono (x.2) (y.2) (cx.2)) as (z2&?&?); auto.
      exists (z1,z2). by rewrite prod_included prod_pcore_Some.
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
    - intros n x y1 y2 [??] [??]; simpl in *.
      destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z11&z12&?&?&?); auto.
      destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
      by exists (z11,z21), (z12,z22).
  Qed.
(* iris/algebra/cmra.v *)
Canonical prodR
:= Cmra (prod A B) prod_cmra_mixin.
(* iris/algebra/cmra.v *)
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_validN (a : A) (b : B) n : ✓{n} (a, b) ↔ ✓{n} a ∧ ✓{n} b.
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_included (a a' : A) (b b' : B) :
    (a, b) ≼ (a', b') ↔ a ≼ a' ∧ b ≼ b'.
Proof. apply prod_included. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_includedN (a a' : A) (b b' : B) n :
    (a, b) ≼{n} (a', b') ↔ a ≼{n} a' ∧ b ≼{n} b'.
Proof. apply prod_includedN. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_pcore (a : A) (b : B) :
    pcore (a, b) = c1 ← pcore a; c2 ← pcore b; Some (c1, c2).
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
    core (a, b) = (core a, core b).
Proof.
    rewrite /core {1}/pcore /=.
    rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
  Qed.
(* iris/algebra/cmra.v *)
Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
Proof.
    intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
    exists (ca,cb); by simplify_option_eq.
  Qed.
(* iris/algebra/cmra.v *)
Instance prod_cmra_discrete :
    CmraDiscrete A → CmraDiscrete B → CmraDiscrete prodR.
Proof. split; [apply _|]. by intros ? []; split; apply cmra_discrete_valid. Qed.
(* iris/algebra/cmra.v *)
(* FIXME(Coq #6294): This is not an instance because we need it to use the new
  unification. *)
Lemma pair_core_id x y :
    CoreId x → CoreId y → CoreId (x,y).
Proof. by rewrite /CoreId prod_pcore_Some'. Qed.
(* iris/algebra/cmra.v *)
Instance pair_exclusive_l x y : Exclusive x → Exclusive (x,y).
Proof. by intros ?[][?%exclusive0_l]. Qed.
(* iris/algebra/cmra.v *)
Instance pair_exclusive_r x y : Exclusive y → Exclusive (x,y).
Proof. by intros ?[][??%exclusive0_l]. Qed.
(* iris/algebra/cmra.v *)
Instance pair_cancelable x y :
    Cancelable x → Cancelable y → Cancelable (x,y).
Proof. intros ???[][][][]. constructor; simpl in *; by eapply cancelableN. Qed.
(* iris/algebra/cmra.v *)
Instance pair_id_free_l x y : IdFree x → IdFree (x,y).
Proof. move=> Hx [a b] [? _] [/=? _]. apply (Hx a); eauto. Qed.
(* iris/algebra/cmra.v *)
Instance pair_id_free_r x y : IdFree y → IdFree (x,y).
Proof. move=> Hy [a b] [_ ?] [_ /=?]. apply (Hy b); eauto. Qed.
(* iris/algebra/cmra.v *)
Instance prod_unit_instance `{Unit A, Unit B} : Unit (A * B)
:= (ε, ε).
(* iris/algebra/cmra.v *)
Lemma prod_ucmra_mixin : UcmraMixin (A * B).
Proof.
    split.
    - split; apply ucmra_unit_valid.
    - by split; rewrite /=left_id.
    - rewrite prod_pcore_Some'; split; apply (core_id _).
  Qed.
(* iris/algebra/cmra.v *)
Canonical prodUR
:= Ucmra (prod A B) prod_ucmra_mixin.
(* iris/algebra/cmra.v *)
Lemma pair_split (a : A) (b : B) : (a, b) ≡ (a, ε) ⋅ (ε, b).
Proof. by rewrite -pair_op left_id right_id. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
    (x, y) = (x, ε) ⋅ (ε, y).
Proof. unfold_leibniz. apply pair_split. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_op_1 (a a': A) : (a ⋅ a', ε) ≡@{A*B} (a, ε) ⋅ (a', ε).
Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_op_1_L `{!LeibnizEquiv A, !LeibnizEquiv B} (a a': A) :
    (a ⋅ a', ε) =@{A*B} (a, ε) ⋅ (a', ε).
Proof. unfold_leibniz. apply pair_op_1. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_op_2 (b b': B) : (ε, b ⋅ b') ≡@{A*B} (ε, b) ⋅ (ε, b').
Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.
(* iris/algebra/cmra.v *)
Lemma pair_op_2_L `{!LeibnizEquiv A, !LeibnizEquiv B} (b b': B) :
    (ε, b ⋅ b') =@{A*B} (ε, b) ⋅ (ε, b').
Proof. unfold_leibniz. apply pair_op_2. Qed.
(* iris/algebra/cmra.v *)
Instance prod_map_cmra_morphism
    {SI : sidx} {A A' B B' : cmra} (f : A → A') (g : B → B') :
  CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
Proof.
  split; first apply _.
  - by intros n x [??]; split; simpl; apply cmra_morphism_validN.
  - intros [x1 x2]. rewrite /= !pair_pcore /=.
    pose proof (Hf := cmra_morphism_pcore f (x1)).
    destruct (pcore (f (x1))), (pcore (x1)); inv Hf=>//=.
    pose proof (Hg := cmra_morphism_pcore g (x2)).
    destruct (pcore (g (x2))), (pcore (x2)); inv Hg=>//=.
    by setoid_subst.
  - intros. by rewrite /prod_map /= !cmra_morphism_op.
Qed.
(* iris/algebra/cmra.v *)
Definition prodRF {SI : sidx} (F1 F2 : rFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
  by apply prodO_map_ne; apply rFunctor_map_ne.
Qed.
(* iris/algebra/cmra.v *)
Notation "F1 * F2"
:= (prodRF F1%RF F2%RF) : rFunctor_scope.
(* iris/algebra/cmra.v *)
Instance prodRF_contractive {SI : sidx} F1 F2 :
  rFunctorContractive F1 → rFunctorContractive F2 →
  rFunctorContractive (prodRF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodO_map_ne; apply rFunctor_map_contractive.
Qed.
(* iris/algebra/cmra.v *)
Definition prodURF {SI : sidx} (F1 F2 : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
  intros ? F1 F2 A1 ? A2 ? B1 ? B2 ? n ???.
  by apply prodO_map_ne; apply urFunctor_map_ne.
Qed.
(* iris/algebra/cmra.v *)
Notation "F1 * F2"
:= (prodURF F1%URF F2%URF) : urFunctor_scope.
(* iris/algebra/cmra.v *)
Instance prodURF_contractive {SI : sidx} F1 F2 :
  urFunctorContractive F1 → urFunctorContractive F2 →
  urFunctorContractive (prodURF F1 F2).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
    by apply prodO_map_ne; apply urFunctor_map_contractive.
Qed.
(* iris/algebra/cmra.v *)
Instance option_valid_instance : Valid (option A)
:= λ ma,
    match ma with Some a => ✓ a | None => True end.
(* iris/algebra/cmra.v *)
Instance option_validN_instance : ValidN (option A)
:= λ n ma,
    match ma with Some a => ✓{n} a | None => True end.
(* iris/algebra/cmra.v *)
Instance option_pcore_instance : PCore (option A)
:= λ ma,
    Some (ma ≫= pcore).
(* iris/algebra/cmra.v *)
Instance option_op_instance : Op (option A)
:=
    union_with (λ a b, Some (a ⋅ b)).
(* iris/algebra/cmra.v *)
Definition Some_valid a : ✓ Some a ↔ ✓ a
:= reflexivity _.
(* iris/algebra/cmra.v *)
Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a
:= reflexivity _.
(* iris/algebra/cmra.v *)
Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b
:= eq_refl.
(* iris/algebra/cmra.v *)
Lemma Some_core `{!CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
(* iris/algebra/cmra.v *)
Lemma pcore_Some a : pcore (Some a) = Some (pcore a).
Proof. done. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_op_opM a ma : Some a ⋅ ma = Some (a ⋅? ma).
Proof. by destruct ma. Qed.
(* iris/algebra/cmra.v *)
Lemma option_included ma mb :
    ma ≼ mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ (a ≡ b ∨ a ≼ b).
Proof.
    split.
    - intros [mc Hmc].
      destruct ma as [a|]; [right|by left].
      destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
      destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
        setoid_subst; eauto.
    - intros [->|(a&b&->&->&[Hc|[c Hc]])].
      + exists mb. by destruct mb.
      + exists None; by constructor.
      + exists (Some c); by constructor.
  Qed.
(* iris/algebra/cmra.v *)
Lemma option_included_total `{!CmraTotal A} ma mb :
    ma ≼ mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ a ≼ b.
Proof.
    rewrite option_included. split; last naive_solver.
    intros [->|(a&b&->&->&[Hab|?])]; [by eauto| |by eauto 10].
    right. exists a, b. by rewrite {3}Hab.
  Qed.
(* iris/algebra/cmra.v *)
Lemma option_includedN n ma mb :
    ma ≼{n} mb ↔ ma = None ∨
                 ∃ x y, ma = Some x ∧ mb = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y).
Proof.
    split.
    - intros [mc Hmc].
      destruct ma as [a|]; [right|by left].
      destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
      destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
        ofe_subst; eauto using cmra_includedN_l.
    - intros [->|(a&y&->&->&[Hc|[c Hc]])].
      + exists mb. by destruct mb.
      + exists None; by constructor.
      + exists (Some c); by constructor.
  Qed.
(* iris/algebra/cmra.v *)
Lemma option_includedN_total `{!CmraTotal A} n ma mb :
    ma ≼{n} mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ a ≼{n} b.
Proof.
    rewrite option_includedN. split; last naive_solver.
    intros [->|(a&b&->&->&[Hab|?])]; [by eauto| |by eauto 10].
    right. exists a, b. by rewrite {3}Hab.
  Qed.
(* iris/algebra/cmra.v *)
(* See below for more [included] lemmas. *)
Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
    apply cmra_total_mixin.
    - eauto.
    - by intros [a|] n; destruct 1; constructor; ofe_subst.
    - destruct 1; by ofe_subst.
    - by destruct 1; rewrite /validN /option_validN_instance //=; ofe_subst.
    - intros [a|]; [apply cmra_valid_validN|done].
    - intros n m [a|];
        unfold validN, option_validN_instance; eauto using cmra_validN_le.
    - intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
    - intros [a|] [b|]; constructor; rewrite 1?comm; auto.
    - intros [a|]; simpl; auto.
      destruct (pcore a) as [ca|] eqn:?; constructor; eauto using cmra_pcore_l.
    - intros [a|]; simpl; auto.
      destruct (pcore a) as [ca|] eqn:?; simpl; eauto using cmra_pcore_idemp.
    - intros ma mb; setoid_rewrite option_included.
      intros [->|(a&b&->&->&[?|?])]; simpl; eauto.
      + destruct (pcore a) as [ca|] eqn:?; eauto.
        destruct (cmra_pcore_proper a b ca) as (?&?&?); eauto 10.
      + destruct (pcore a) as [ca|] eqn:?; eauto.
        destruct (cmra_pcore_mono a b ca) as (?&?&?); eauto 10.
    - intros n [a|] [b|]; rewrite /validN /option_validN_instance /=;
        eauto using cmra_validN_op_l.
    - intros n ma mb1 mb2.
      destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
        (try by exfalso; inversion Hx'); (try (apply (inj Some) in Hx')).
      + destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto.
        by exists (Some c1), (Some c2); repeat constructor.
      + by exists (Some a), None; repeat constructor.
      + by exists None, (Some a); repeat constructor.
      + exists None, None; repeat constructor.
  Qed.
(* iris/algebra/cmra.v *)
Canonical optionR
:= Cmra (option A) option_cmra_mixin.
(* iris/algebra/cmra.v *)
Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
(* iris/algebra/cmra.v *)
Instance option_unit_instance : Unit (option A)
:= None.
(* iris/algebra/cmra.v *)
Lemma option_ucmra_mixin : UcmraMixin optionR.
Proof. split; [done|  |done]. by intros []. Qed.
(* iris/algebra/cmra.v *)
Canonical optionUR
:= Ucmra (option A) option_ucmra_mixin.
(* iris/algebra/cmra.v *)
(* Misc *)
Lemma op_None ma mb : ma ⋅ mb = None ↔ ma = None ∧ mb = None.
Proof. destruct ma, mb; naive_solver. Qed.
(* iris/algebra/cmra.v *)
Lemma op_is_Some ma mb : is_Some (ma ⋅ mb) ↔ is_Some ma ∨ is_Some mb.
Proof. rewrite -!not_eq_None_Some op_None. destruct ma, mb; naive_solver. Qed.
(* iris/algebra/cmra.v *)
(* When the goal is already of the form [None ⋅ x], the [LeftId] instance for
     [ε] does not fire. *)
Instance op_None_left_id : LeftId (=) None (@op (option A) _).
Proof. intros [a|]; done. Qed.
(* iris/algebra/cmra.v *)
Instance op_None_right_id : RightId (=) None (@op (option A) _).
Proof. intros [a|]; done. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_opM_opM_assoc a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? (mb ⋅ mc).
Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_opM_opM_assoc_L `{!LeibnizEquiv A} a mb mc :
    a ⋅? mb ⋅? mc = a ⋅? (mb ⋅ mc).
Proof. unfold_leibniz. apply cmra_opM_opM_assoc. Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_opM_opM_swap a mb mc : a ⋅? mb ⋅? mc ≡ a ⋅? mc ⋅? mb.
Proof. by rewrite !cmra_opM_opM_assoc (comm _ mb). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_opM_opM_swap_L `{!LeibnizEquiv A} a mb mc :
    a ⋅? mb ⋅? mc = a ⋅? mc ⋅? mb.
Proof. by rewrite !cmra_opM_opM_assoc_L (comm_L _ mb). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_opM_fmap_Some ma1 ma2 : ma1 ⋅? (Some <$> ma2) = ma1 ⋅ ma2.
Proof. by destruct ma1, ma2. Qed.
(* iris/algebra/cmra.v *)
Instance Some_core_id a : CoreId a → CoreId (Some a).
Proof. by constructor. Qed.
(* iris/algebra/cmra.v *)
Instance option_core_id ma : (∀ x : A, CoreId x) → CoreId ma.
Proof. intros. destruct ma; apply _. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
    ✓{n} (Some a ⋅ mb) → mb = None.
Proof. destruct mb; last done. move=> /(exclusiveN_l _ a) []. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusiveN_Some_r n a `{!Exclusive a} mb :
    ✓{n} (mb ⋅ Some a) → mb = None.
Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusive_Some_l a `{!Exclusive a} mb : ✓ (Some a ⋅ mb) → mb = None.
Proof. destruct mb; last done. move=> /(exclusive_l a) []. Qed.
(* iris/algebra/cmra.v *)
Lemma exclusive_Some_r a `{!Exclusive a} mb : ✓ (mb ⋅ Some a) → mb = None.
Proof. rewrite comm. by apply exclusive_Some_l. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN n a b : Some a ≼{n} Some b ↔ a ≡{n}≡ b ∨ a ≼{n} b.
Proof. rewrite option_includedN; naive_solver. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_1 n a b : Some a ≼{n} Some b → a ≡{n}≡ b ∨ a ≼{n} b.
Proof. rewrite Some_includedN. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_2 n a b : a ≡{n}≡ b ∨ a ≼{n} b → Some a ≼{n} Some b.
Proof. rewrite Some_includedN. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_mono n a b : a ≼{n} b → Some a ≼{n} Some b.
Proof. rewrite Some_includedN. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_refl n a b : a ≡{n}≡ b → Some a ≼{n} Some b.
Proof. rewrite Some_includedN. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_is_Some n x mb : Some x ≼{n} mb → is_Some mb.
Proof. rewrite option_includedN. naive_solver. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included a b : Some a ≼ Some b ↔ a ≡ b ∨ a ≼ b.
Proof. rewrite option_included; naive_solver. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_1 a b : Some a ≼ Some b → a ≡ b ∨ a ≼ b.
Proof. rewrite Some_included. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_2 a b : a ≡ b ∨ a ≼ b → Some a ≼ Some b.
Proof. rewrite Some_included. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_mono a b : a ≼ b → Some a ≼ Some b.
Proof. rewrite Some_included. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_refl a b : a ≡ b → Some a ≼ Some b.
Proof. rewrite Some_included. auto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_is_Some x mb : Some x ≼ mb → is_Some mb.
Proof. rewrite option_included. naive_solver. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_opM n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc.
Proof.
    rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
  Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_opM a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
Proof.
    rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
  Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_validN_Some_includedN n a b : ✓{n} a → Some b ≼{n} Some a → ✓{n} b.
Proof. apply: (cmra_validN_includedN _ (Some _) (Some _)). Qed.
(* iris/algebra/cmra.v *)
Lemma cmra_valid_Some_included a b : ✓ a → Some b ≼ Some a → ✓ b.
Proof. apply: (cmra_valid_included (Some _) (Some _)). Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_total `{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
    Some a ≼{n} Some b → ✓{n} b → a ≡{n}≡ b.
Proof. move=> /Some_includedN [//|/exclusive_includedN]; tauto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_included_exclusive a `{!Exclusive a} b :
    Some a ≼ Some b → ✓ b → a ≡ b.
Proof. move=> /Some_included [//|/exclusive_included]; tauto. Qed.
(* iris/algebra/cmra.v *)
Lemma is_Some_includedN n ma mb : ma ≼{n} mb → is_Some ma → is_Some mb.
Proof. rewrite -!not_eq_None_Some option_includedN. naive_solver. Qed.
(* iris/algebra/cmra.v *)
Lemma is_Some_included ma mb : ma ≼ mb → is_Some ma → is_Some mb.
Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
(* iris/algebra/cmra.v *)
Instance cancelable_Some a :
    IdFree a → Cancelable a → Cancelable (Some a).
Proof.
    intros Hirr ? n [b|] [c|] ? EQ; inversion_clear EQ.
    - constructor. by apply (cancelableN a).
    - destruct (Hirr b); [|eauto using dist_le, SIdx.le_0_l].
      by eapply (cmra_validN_op_l 0ᵢ a b), (cmra_validN_le n), SIdx.le_0_l.
    - destruct (Hirr c); [|symmetry; eauto using dist_le, SIdx.le_0_l].
      by eapply (cmra_validN_le n), SIdx.le_0_l.
    - done.
  Qed.
(* iris/algebra/cmra.v *)
Instance option_cancelable (ma : option A) :
    (∀ a : A, IdFree a) → (∀ a : A, Cancelable a) → Cancelable ma.
Proof. destruct ma; apply _. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_includedN n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ Some b1 ≼{n} Some b2.
Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_includedN_l n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2.
Proof. intros. eapply Some_pair_includedN. done. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_includedN_r n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some b1 ≼{n} Some b2.
Proof. intros. eapply Some_pair_includedN. done. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_includedN_total_1 `{!CmraTotal A} n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → a1 ≼{n} a2 ∧ Some b1 ≼{n} Some b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ a1). Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_includedN_total_2 `{!CmraTotal B} n a1 a2 b1 b2 :
    Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ b1 ≼{n} b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ b1). Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_included a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ Some b1 ≼ Some b2.
Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_included_l a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2.
Proof. intros. eapply Some_pair_included. done. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_included_r a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some b1 ≼ Some b2.
Proof. intros. eapply Some_pair_included. done. Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_included_total_1 `{!CmraTotal A} a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → a1 ≼ a2 ∧ Some b1 ≼ Some b2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total a1). Qed.
(* iris/algebra/cmra.v *)
Lemma Some_pair_included_total_2 `{!CmraTotal B} a1 a2 b1 b2 :
    Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ b1 ≼ b2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
(* iris/algebra/cmra.v *)
Lemma option_fmap_mono {SI : sidx} {A B : cmra} (f : A → B) (ma mb : option A) :
  Proper ((≡) ==> (≡)) f →
  (∀ a b, a ≼ b → f a ≼ f b) →
  ma ≼ mb → f <$> ma ≼ f <$> mb.
Proof.
  intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.
(* iris/algebra/cmra.v *)
Instance option_fmap_cmra_morphism {SI : sidx}
    {A B : cmra} (f: A → B) `{!CmraMorphism f} :
  CmraMorphism (fmap f : option A → option B).
Proof.
  split; first apply _.
  - intros n [a|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
  - move=> [a|] //. by apply Some_proper, cmra_morphism_pcore.
  - move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
Qed.
(* iris/algebra/cmra.v *)
Definition optionURF {SI : sidx} (F : rFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  by apply optionO_map_ne, rFunctor_map_ne.
Qed.
(* iris/algebra/cmra.v *)
Instance optionURF_contractive {SI : sidx} F :
  rFunctorContractive F → urFunctorContractive (optionURF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  by apply optionO_map_ne, rFunctor_map_contractive.
Qed.
(* iris/algebra/cmra.v *)
Definition optionRF {SI : sidx} (F : rFunctor) : rFunctor
:= {|
  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
|}.
(* iris/algebra/cmra.v *)
Instance optionRF_contractive {SI : sidx} F :
  rFunctorContractive F → rFunctorContractive (optionRF F).
Proof. apply optionURF_contractive. Qed.
(* iris/algebra/cmra.v *)
Instance discrete_fun_op_instance : Op (discrete_fun B)
:= λ f g x,
    f x ⋅ g x.
(* iris/algebra/cmra.v *)
Instance discrete_fun_pcore_instance : PCore (discrete_fun B)
:= λ f,
    Some (λ x, core (f x)).
(* iris/algebra/cmra.v *)
Instance discrete_fun_valid_instance : Valid (discrete_fun B)
:= λ f,
    ∀ x, ✓ f x.