phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/local_updates.v *)
Lemma op_local_update_frame x y x' y' yf :
    (x,y) ~l~> (x',y') → (x,y ⋅ yf) ~l~> (x', y' ⋅ yf).
Proof.
    intros Hup n mz Hxv Hx; simpl in *.
    destruct (Hup n (Some (yf ⋅? mz))); [done|by rewrite /= -cmra_op_opM_assoc|].
    by rewrite cmra_op_opM_assoc.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma cancel_local_update x y z `{!Cancelable x} :
    (x ⋅ y, x ⋅ z) ~l~> (y, z).
Proof.
    intros n f ? Heq. split; first by eapply cmra_validN_op_r.
    apply (cancelableN x); first done. by rewrite -cmra_op_opM_assoc.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma replace_local_update x y `{!IdFree x} :
    ✓ y → (x, x) ~l~> (y, y).
Proof.
    intros ? n mz ? Heq; simpl in *; split; first by apply cmra_valid_validN.
    destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
  Qed.
(* iris/algebra/local_updates.v *)
Lemma core_id_local_update x y z `{!CoreId y} :
    y ≼ x → (x, z) ~l~> (x, z ⋅ y).
Proof.
    intros Hincl n mf ? Heq; simpl in *; split; first done.
    rewrite [x]core_id_extract // Heq. destruct mf as [f|]; last done.
    simpl. rewrite -assoc [f ⋅ y]comm assoc //.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
    (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
Proof.
    rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
    setoid_rewrite <-(λ n, discrete_iff n x _).
    setoid_rewrite <-(λ n, discrete_iff n x' _). pose 0ᵢ. naive_solver.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_valid0 x y x' y' :
    (✓{0ᵢ} x → ✓{0ᵢ} y → Some y ≼{0ᵢ} Some x → (x,y) ~l~> (x',y')) →
    (x,y) ~l~> (x',y').
Proof.
    intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
    - by apply (cmra_validN_le n), SIdx.le_0_l.
    - apply (cmra_validN_le n), SIdx.le_0_l.
      move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
    - eapply (cmra_includedN_le n), SIdx.le_0_l.
      apply Some_includedN_opM. eauto.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_valid `{!CmraDiscrete A} x y x' y' :
    (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
Proof.
    rewrite !(cmra_discrete_valid_iff 0ᵢ) (cmra_discrete_included_iff 0ᵢ).
    apply local_update_valid0.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_total_valid0 `{!CmraTotal A} x y x' y' :
    (✓{0ᵢ} x → ✓{0ᵢ} y → y ≼{0ᵢ} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
Proof.
    intros Hup. apply local_update_valid0=> ?? Hincl. apply Hup; auto.
    by apply Some_includedN_total.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_total_valid `{!CmraTotal A, !CmraDiscrete A} x y x' y' :
    (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
Proof.
    rewrite !(cmra_discrete_valid_iff 0ᵢ) (cmra_discrete_included_iff 0ᵢ).
    apply local_update_total_valid0.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_unital x y x' y' :
    (x,y) ~l~> (x',y') ↔ ∀ n z,
      ✓{n} x → x ≡{n}≡ y ⋅ z → ✓{n} x' ∧ x' ≡{n}≡ y' ⋅ z.
Proof.
    split.
    - intros Hup n z. apply (Hup _ (Some z)).
    - intros Hup n [z|]; simpl; [by auto|].
      rewrite -(right_id ε op y) -(right_id ε op y'). auto.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma local_update_unital_discrete `{!CmraDiscrete A} (x y x' y' : A) :
    (x,y) ~l~> (x',y') ↔ ∀ z, ✓ x → x ≡ y ⋅ z → ✓ x' ∧ x' ≡ y' ⋅ z.
Proof.
    rewrite local_update_discrete. split.
    - intros Hup z. apply (Hup (Some z)).
    - intros Hup [z|]; simpl; [by auto|].
      rewrite -(right_id ε op y) -(right_id ε op y'). auto.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma cancel_local_update_unit x y `{!Cancelable x} :
    (x ⋅ y, x) ~l~> (y, ε).
Proof. rewrite -{2}(right_id ε op x). by apply cancel_local_update. Qed.
(* iris/algebra/local_updates.v *)
(* * Unit *)
Lemma unit_local_update (x y x' y' : unit) : (x, y) ~l~> (x', y').
Proof. destruct x,y,x',y'; reflexivity. Qed.
(* iris/algebra/local_updates.v *)
(* * Dependently-typed functions over a discrete domain *)
Lemma discrete_fun_local_update {A} {B : A → ucmra} (f g f' g' : discrete_fun B) :
    (∀ x : A, (f x, g x) ~l~> (f' x, g' x)) →
    (f, g) ~l~> (f', g').
Proof.
    setoid_rewrite local_update_unital. intros Hupd n h Hf Hg.
    split=> x; eapply Hupd, Hg; eauto.
  Qed.
(* iris/algebra/local_updates.v *)
(* * Product *)
Lemma prod_local_update {A B : cmra} (x y x' y' : A * B) :
    (x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →
    (x,y) ~l~> (x',y').
Proof.
    intros Hup1 Hup2 n mz [??] [??]; simpl in *.
    destruct (Hup1 n (fst <$> mz)); [done|by destruct mz|].
    destruct (Hup2 n (snd <$> mz)); [done|by destruct mz|].
    by destruct mz.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma prod_local_update' {A B : cmra} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
    (x1,y1) ~l~> (x1',y1') → (x2,y2) ~l~> (x2',y2') →
    ((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')).
Proof. intros. by apply prod_local_update. Qed.
(* iris/algebra/local_updates.v *)
Lemma prod_local_update_1 {A B : cmra} (x1 y1 x1' y1' : A) (x2 y2 : B) :
    (x1,y1) ~l~> (x1',y1') → ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)).
Proof. intros. by apply prod_local_update. Qed.
(* iris/algebra/local_updates.v *)
Lemma prod_local_update_2 {A B : cmra} (x1 y1 : A) (x2 y2 x2' y2' : B) :
    (x2,y2) ~l~> (x2',y2') → ((x1,x2),(y1,y2)) ~l~> ((x1,x2'),(y1,y2')).
Proof. intros. by apply prod_local_update. Qed.
(* iris/algebra/local_updates.v *)
(* TODO: Investigate whether we can use these in proving the very similar local
    updates on finmaps. *)
Lemma option_local_update {A : cmra} (x y x' y' : A) :
    (x, y) ~l~> (x',y') →
    (Some x, Some y) ~l~> (Some x', Some y').
Proof.
    intros Hup. apply local_update_unital=>n mz Hxv Hx; simpl in *.
    destruct (Hup n mz); first done.
    { destruct mz as [?|]; inversion_clear Hx; auto. }
    split; first done. destruct mz as [?|]; constructor; auto.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma option_local_update_None {A: ucmra} (x x' y': A):
    (x, ε) ~l~> (x', y') ->
    (Some x, None) ~l~> (Some x', Some y').
Proof.
    intros Hup. apply local_update_unital=> n mz.
    rewrite left_id=> ? <-.
    destruct (Hup n (Some x)); simpl in *; first done.
    - by rewrite left_id.
    - split; first done. rewrite -Some_op. by constructor.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma alloc_option_local_update {A : cmra} (x : A) y :
    ✓ x →
    (None, y) ~l~> (Some x, Some x).
Proof.
    move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
    { rewrite Some_validN. apply cmra_valid_validN. done. }
    destruct z as [z|]; last done. destruct y; inversion Heq.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma delete_option_local_update {A : cmra} (x : option A) (y : A) :
    Exclusive y → (x, Some y) ~l~> (None, None).
Proof.
    move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
    destruct z as [z|]; last done. exfalso.
    move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
    eapply cmra_validN_le, SIdx.le_0_l. eapply Hy.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma delete_option_local_update_cancelable {A : cmra} (mx : option A) :
    Cancelable mx → (mx, mx) ~l~> (None, None).
Proof.
    intros ?. apply local_update_unital=>n mf /= Hmx Heq. split; first done.
    rewrite left_id. eapply (cancelableN mx); by rewrite right_id_L.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Definition max_prefix_list (A : Type)
:= gmap nat (agree A).
(* iris/algebra/max_prefix_list.v *)
Definition max_prefix_listR {SI : sidx} (A : ofe)
:= gmapUR nat (agreeR A).
(* iris/algebra/max_prefix_list.v *)
Definition max_prefix_listUR {SI : sidx} (A : ofe)
:= gmapUR nat (agreeR A).
(* iris/algebra/max_prefix_list.v *)
Definition to_max_prefix_list {A} (l : list A) : gmap nat (agree A)
:=
  to_agree <$> map_seq 0 l.
(* iris/algebra/max_prefix_list.v *)
Instance : Params (@to_max_prefix_list) 1
:= {}.
(* iris/algebra/max_prefix_list.v *)
Instance to_max_prefix_list_ne : NonExpansive (@to_max_prefix_list A).
Proof. solve_proper. Qed.
(* iris/algebra/max_prefix_list.v *)
Instance to_max_prefix_list_proper :
    Proper ((≡) ==> (≡)) (@to_max_prefix_list A).
Proof. solve_proper. Qed.
(* iris/algebra/max_prefix_list.v *)
Instance to_max_prefix_list_dist_inj n :
    Inj (dist n) (dist n) (@to_max_prefix_list A).
Proof.
    rewrite /to_max_prefix_list. intros l1 l2 Hl. apply list_dist_lookup=> i.
    move: (Hl i). rewrite !lookup_fmap !lookup_map_seq Nat.sub_0_r.
    rewrite !option_guard_True; [|lia..].
    destruct (l1 !! i), (l2 !! i); inversion_clear 1;
      constructor; by apply (inj to_agree).
  Qed.
(* iris/algebra/max_prefix_list.v *)
Instance to_max_prefix_list_inj : Inj (≡) (≡) (@to_max_prefix_list A).
Proof.
    intros l1 l2. rewrite !equiv_dist=> ? n. by apply (inj to_max_prefix_list).
  Qed.
(* iris/algebra/max_prefix_list.v *)
Instance mono_list_lb_core_id (m : max_prefix_list A) : CoreId m
:= _.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
Proof.
    intros i. rewrite /to_max_prefix_list lookup_fmap.
    by destruct (map_seq 0 l !! i).
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
Proof. apply cmra_valid_validN, to_max_prefix_list_valid. Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_app l1 l2 :
    to_max_prefix_list (l1 ++ l2) ≡
    to_max_prefix_list l1 ⋅ (to_agree <$> map_seq (length l1) l2).
Proof.
    rewrite /to_max_prefix_list map_seq_app=> i /=. rewrite lookup_op !lookup_fmap.
    destruct (map_seq 0 l1 !! i) as [x|] eqn:Hl1; simpl; last first.
    { by rewrite lookup_union_r // left_id. }
    rewrite (lookup_union_Some_l _ _ _ x) //=.
    assert (map_seq (M:=gmap nat A) (length l1) l2 !! i = None) as ->.
    { apply lookup_map_seq_None.
      apply lookup_map_seq_Some in Hl1 as [_ ?%lookup_lt_Some]. lia. }
    by rewrite /= right_id.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_op_l l1 l2 :
    l1 `prefix_of` l2 →
    to_max_prefix_list l1 ⋅ to_max_prefix_list l2 ≡ to_max_prefix_list l2.
Proof. intros [l ->]. by rewrite to_max_prefix_list_app assoc -core_id_dup. Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_op_r l1 l2 :
    l1 `prefix_of` l2 →
    to_max_prefix_list l2 ⋅ to_max_prefix_list l1 ≡ to_max_prefix_list l2.
Proof. intros. by rewrite comm to_max_prefix_list_op_l. Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma max_prefix_list_included_includedN (ml1 ml2 : max_prefix_list A) :
    ml1 ≼ ml2 ↔ ∀ n, ml1 ≼{n} ml2.
Proof.
    split; [intros; by apply: cmra_included_includedN|].
    intros Hincl. exists ml2. apply equiv_dist=> n. destruct (Hincl n) as [l ->].
    by rewrite assoc -core_id_dup.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_includedN_aux n l1 l2 :
    to_max_prefix_list l1 ≼{n} to_max_prefix_list l2 →
    l2 ≡{n}≡ l1 ++ drop (length l1) l2.
Proof.
    rewrite lookup_includedN=> Hincl. apply list_dist_lookup=> i.
    rewrite lookup_app. move: (Hincl i).
    rewrite /to_max_prefix_list !lookup_fmap !lookup_map_seq Nat.sub_0_r.
    rewrite !option_guard_True; [|lia..].
    rewrite option_includedN_total fmap_None.
    intros [Hi|(?&?&(a2&->&->)%fmap_Some&(a1&->&->)%fmap_Some&Ha)].
    - rewrite lookup_drop Hi. apply lookup_ge_None in Hi. f_equiv; lia.
    - f_equiv. symmetry. by apply to_agree_includedN.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_includedN n l1 l2 :
    to_max_prefix_list l1 ≼{n} to_max_prefix_list l2 ↔ ∃ l, l2 ≡{n}≡ l1 ++ l.
Proof.
    split.
    - intros. eexists. by apply to_max_prefix_list_includedN_aux.
    - intros [l ->]. rewrite to_max_prefix_list_app. apply: cmra_includedN_l.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_included l1 l2 :
    to_max_prefix_list l1 ≼ to_max_prefix_list l2 ↔ ∃ l, l2 ≡ l1 ++ l.
Proof.
    split.
    - intros. eexists. apply equiv_dist=> n.
      apply to_max_prefix_list_includedN_aux. by apply: cmra_included_includedN.
    - intros [l ->]. rewrite to_max_prefix_list_app. eauto.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_included_L `{!LeibnizEquiv A} l1 l2 :
    to_max_prefix_list l1 ≼ to_max_prefix_list l2 ↔ l1 `prefix_of` l2.
Proof. rewrite to_max_prefix_list_included /prefix. naive_solver. Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_op_validN_aux n l1 l2 :
    length l1 ≤ length l2 →
    ✓{n} (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) →
    l2 ≡{n}≡ l1 ++ drop (length l1) l2.
Proof.
    intros Hlen Hvalid. apply list_dist_lookup=> i. move: (Hvalid i).
    rewrite /to_max_prefix_list lookup_op !lookup_fmap !lookup_map_seq Nat.sub_0_r.
    rewrite !option_guard_True; [|lia..].
    intros ?. rewrite lookup_app.
    destruct (l1 !! i) as [x1|] eqn:Hi1, (l2 !! i) as [x2|] eqn:Hi2; simpl in *.
    - f_equiv. symmetry. by apply to_agree_op_validN.
    - apply lookup_lt_Some in Hi1; apply lookup_ge_None in Hi2. lia.
    - apply lookup_ge_None in Hi1. rewrite lookup_drop -Hi2. f_equiv; lia.
    - apply lookup_ge_None in Hi1. rewrite lookup_drop -Hi2. f_equiv; lia.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_op_validN n l1 l2 :
    ✓{n} (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) ↔
    (∃ l, l2 ≡{n}≡ l1 ++ l) ∨ (∃ l, l1 ≡{n}≡ l2 ++ l).
Proof.
    split.
    - destruct (decide (length l1 ≤ length l2)).
      + left. eexists. by eapply to_max_prefix_list_op_validN_aux.
      + right. eexists. eapply to_max_prefix_list_op_validN_aux; [lia|by rewrite comm].
    - intros [[l ->]|[l ->]].
      + rewrite to_max_prefix_list_op_l; last by apply prefix_app_r.
        apply to_max_prefix_list_validN.
      + rewrite to_max_prefix_list_op_r; last by apply prefix_app_r.
        apply to_max_prefix_list_validN.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_op_valid l1 l2 :
    ✓ (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) ↔
    (∃ l, l2 ≡ l1 ++ l) ∨ (∃ l, l1 ≡ l2 ++ l).
Proof.
    split.
    - destruct (decide (length l1 ≤ length l2)).
      + left. eexists. apply equiv_dist=> n'.
        by eapply to_max_prefix_list_op_validN_aux, cmra_valid_validN.
      + right. eexists. apply equiv_dist=> n'.
        by eapply to_max_prefix_list_op_validN_aux,
          cmra_valid_validN; [lia|by rewrite comm].
    - intros [[l ->]|[l ->]].
      + rewrite to_max_prefix_list_op_l; last by apply prefix_app_r.
        apply to_max_prefix_list_valid.
      + rewrite to_max_prefix_list_op_r; last by apply prefix_app_r.
        apply to_max_prefix_list_valid.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma to_max_prefix_list_op_valid_L `{!LeibnizEquiv A} l1 l2 :
    ✓ (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) ↔
    l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
Proof. rewrite to_max_prefix_list_op_valid /prefix. naive_solver. Qed.
(* iris/algebra/max_prefix_list.v *)
Lemma max_prefix_list_local_update l1 l2 :
    l1 `prefix_of` l2 →
    (to_max_prefix_list l1, to_max_prefix_list l1) ~l~>
      (to_max_prefix_list l2, to_max_prefix_list l2).
Proof.
    intros [l ->]. rewrite to_max_prefix_list_app (comm _ (to_max_prefix_list l1)).
    apply op_local_update=> n _. rewrite comm -to_max_prefix_list_app.
    apply to_max_prefix_list_validN.
  Qed.
(* iris/algebra/max_prefix_list.v *)
Definition max_prefix_listURF {SI : sidx} (F : oFunctor) : urFunctor
:=
  gmapURF nat (agreeRF F).
(* iris/algebra/max_prefix_list.v *)
Instance max_prefix_listURF_contractive {SI : sidx} F :
  oFunctorContractive F → urFunctorContractive (max_prefix_listURF F).
Proof. apply _. Qed.
(* iris/algebra/max_prefix_list.v *)
Definition max_prefix_listRF {SI : sidx} (F : oFunctor) : rFunctor
:=
  gmapRF nat (agreeRF F).
(* iris/algebra/max_prefix_list.v *)
Instance max_prefix_listRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (max_prefix_listRF F).
Proof. apply _. Qed.
(* iris/algebra/monoid.v *)
(* The [Monoid] class is used for the generic big operators in the file
[algebra/big_op]. The operation [o] and unit [u] are arguments instead of
fields of [Monoid] because we want to support multiple monoids over the same
carrier type (for example, on BIs we have monoids for [∗]/[emp], [∧]/[True],
and [∨]/[False]).

There are two classes, [MonoidOps] just groups the operation and unit, while
[Monoid] contains the laws. Definitions (e.g., the big operators) should use
[MonoidOps] so they do not depend on proofs, while lemmas should use [Monoid].
In definitions, the argument [o] is typically given, and [u] is an implicit
argument that is infered through search for a [MonoidOps] instance. Hence [o]
has input mode, and [u] output mode. *)
Class MonoidOps {M} (o : M → M → M) (u : M)
:= {}.
(* iris/algebra/monoid.v *)
(* Note that [Monoid] has an argument [M : ofe]. We could in principle consider
monoids and big operators over setoids instead of OFEs. However, since we do not
have a canonical structure for setoids, we do not go that way.

Further note that we do not declare any of the projections as type class
instances (i.e., we use [:] instead of [::]). That is because we only need them
in the [big_op] file, and nowhere else. Hence, we declare these instances locally
there to avoid them being used elsewhere. *)
Class Monoid {SI : sidx} {M : ofe} (o : M → M → M) (u : M)
:= {
  monoid_ne : NonExpansive2 o;
  monoid_assoc : Assoc (≡) o;
  monoid_comm : Comm (≡) o;
  monoid_left_id : LeftId (≡) u o;
}.
(* iris/algebra/monoid.v *)
(* This is the only instance for [MonoidOps] that should exist. *)
Instance monoid_ops {SI : sidx} `{Monoid M o u} : MonoidOps o u
:= {}.
(* iris/algebra/monoid.v *)
Lemma monoid_proper {SI : sidx} `{Monoid M o u} : Proper ((≡) ==> (≡) ==> (≡)) o.
Proof. apply ne_proper_2, monoid_ne. Qed.
(* iris/algebra/monoid.v *)
Lemma monoid_right_id {SI : sidx} `{Monoid M o u} : RightId (≡) u o.
Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
(* iris/algebra/monoid.v *)
(* The [Homomorphism] classes give rise to generic lemmas about big operators
commuting with each other. We also consider a [WeakMonoidHomomorphism] which
does not necessarily commute with unit; an example is the [own] connective: we
only have [True ==∗ own γ ∅], not [True ↔ own γ ∅]. *)
Class WeakMonoidHomomorphism {SI : sidx} {M1 M2 : ofe}
    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) {u1 u2} `{!Monoid o1 u1, !Monoid o2 u2}
    (R : relation M2) (f : M1 → M2)
:= {
  monoid_homomorphism_rel_po : PreOrder R;
  monoid_homomorphism_rel_proper : Proper ((≡) ==> (≡) ==> iff) R;
  monoid_homomorphism_op_proper : Proper (R ==> R ==> R) o2;
  monoid_homomorphism_ne : NonExpansive f;
  monoid_homomorphism x y : R (f (o1 x y)) (o2 (f x) (f y))
}.
(* iris/algebra/monoid.v *)
Class MonoidHomomorphism {SI : sidx} {M1 M2 : ofe}
    (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) {u1 u2} `{!Monoid o1 u1, !Monoid o2 u2}
    (R : relation M2) (f : M1 → M2)
:= {
  #[global] monoid_homomorphism_weak :: WeakMonoidHomomorphism o1 o2 R f;
  monoid_homomorphism_unit : R (f u1) u2
}.
(* iris/algebra/monoid.v *)
Lemma weak_monoid_homomorphism_proper {SI : sidx}
  `{WeakMonoidHomomorphism M1 M2 o1 o2 u1 u2 R f} : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, monoid_homomorphism_ne. Qed.
(* iris/algebra/mra.v *)
(* Given a preorder [R] on a type [A] we construct the "monotone" resource
algebra [mra R] and an injection [to_mra : A → mra R] such that:

   [R x y] iff [to_mra x ≼ to_mra y]

Here, [≼] is the extension order of the [mra R] resource algebra. This is
exactly what the lemma [to_mra_included] shows.

This resource algebra is useful for reasoning about monotonicity. See the
following paper for more details ([to_mra] is called "principal"):

  Reasoning About Monotonicity in Separation Logic
  Amin Timany and Lars Birkedal
  in Certified Programs and Proofs (CPP) 2021

Note that unlike most Iris algebra constructions [mra A] works on [A : Type],
not on [A : ofe]. See the comment at [mraO] below for more information. If [A]
has an [Equiv A] (i.e., is a setoid), there are some results at the bottom of
this file. *)
Record mra {A} (R : relation A)
:= { mra_car : list A }.
(* iris/algebra/mra.v *)
Definition to_mra {A} {R : relation A} (a : A) : mra R
:=
  {| mra_car := [a] |}.
(* iris/algebra/mra.v *)
(* Pronounced [a] is below [x]. *)
Definition mra_below (a : A) (x : mra R)
:= ∃ b, b ∈ mra_car x ∧ R a b.
(* iris/algebra/mra.v *)
Lemma mra_below_to_mra a b : mra_below a (to_mra b) ↔ R a b.
Proof. set_solver. Qed.
(* iris/algebra/mra.v *)
(* OFE *)
Instance mra_equiv : Equiv (mra R)
:= λ x y,
    ∀ a, mra_below a x ↔ mra_below a y.
(* iris/algebra/mra.v *)
Instance mra_equiv_equiv : Equivalence mra_equiv.
Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
(* iris/algebra/mra.v *)
(* Generalizing [mra A] to [A : ofe] and [R : A -n> A -n> siProp] is not
  obvious. It is not clear what axioms to impose on [R] for the "extension
  axiom" to hold:

    cmra_extend :
      x ≡{n}≡ y1 ⋅ y2 →
      ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ y1 ≡{n}≡ z1 ∧ y2 ≡{n}≡ z2

  To prove this, assume ([⋅] is defined as [++], see [mra_op]):

    x ≡{n}≡ y1 ++ y2

  When defining [dist] as the step-indexed version of [mra_equiv], this means:

    ∀ n' a, n' ≤ n →
            mra_below a x n' ↔ mra_below a y1 n' ∨ mra_below a y2 n'

  From this assumption it is not clear how to obtain witnesses [z1] and [z2]. *)
Canonical mraO
:= discreteO (mra R).
(* iris/algebra/mra.v *)
(* CMRA *)
Instance mra_valid : Valid (mra R)
:= λ x, True.
(* iris/algebra/mra.v *)
Instance mra_validN : ValidN (mra R)
:= λ n x, True.
(* iris/algebra/mra.v *)
Instance mra_op : Op (mra R)
:= λ x y,
    {| mra_car := mra_car x ++ mra_car y |}.
(* iris/algebra/mra.v *)
Instance mra_pcore : PCore (mra R)
:= Some.
(* iris/algebra/mra.v *)
Lemma mra_cmra_mixin : CmraMixin (mra R).
Proof.
    apply discrete_cmra_mixin; first apply _.
    apply ra_total_mixin; try done.
    - (* [Proper] of [op] *) intros x y z Hyz a. specialize (Hyz a). set_solver.
    - (* [Proper] of [core] *) apply _.
    - (* [Assoc] *) intros x y z a. set_solver.
    - (* [Comm] *) intros x y a. set_solver.
    - (* [core x ⋅ x ≡ x] *) intros x a. set_solver.
  Qed.
(* iris/algebra/mra.v *)
Canonical mraR : cmra
:= Cmra (mra R) mra_cmra_mixin.
(* iris/algebra/mra.v *)
Instance mra_cmra_total : CmraTotal mraR.
Proof. rewrite /CmraTotal; eauto. Qed.
(* iris/algebra/mra.v *)
Instance mra_core_id x : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/mra.v *)
Instance mra_cmra_discrete : CmraDiscrete mraR.
Proof. split; last done. intros ? ?; done. Qed.
(* iris/algebra/mra.v *)
Instance mra_unit : Unit (mra R)
:= {| mra_car := [] |}.
(* iris/algebra/mra.v *)
Lemma auth_ucmra_mixin : UcmraMixin (mra R).
Proof. split; done. Qed.
(* iris/algebra/mra.v *)
Canonical mraUR
:= Ucmra (mra R) auth_ucmra_mixin.
(* iris/algebra/mra.v *)
(* Laws *)
Lemma mra_idemp x : x ⋅ x ≡ x.
Proof. intros a. set_solver. Qed.
(* iris/algebra/mra.v *)
Lemma mra_included x y : x ≼ y ↔ y ≡ x ⋅ y.
Proof using SI.
    split; [|by intros ?; exists y].
    intros [z ->]; rewrite assoc mra_idemp; done.
  Qed.
(* iris/algebra/mra.v *)
Lemma to_mra_R_op `{!Transitive R} a b :
    R a b →
    to_mra a ⋅ to_mra b ≡ to_mra b.
Proof. intros Hab c. set_solver. Qed.
(* iris/algebra/mra.v *)
Lemma to_mra_included `{!PreOrder R} a b :
    to_mra a ≼ to_mra b ↔ R a b.
Proof.
    split.
    - move=> [z Hz]. specialize (Hz a). set_solver.
    - intros ?; exists (to_mra b). by rewrite to_mra_R_op.
  Qed.
(* iris/algebra/mra.v *)
Lemma mra_local_update_grow `{!Transitive R} a x b:
    R a b →
    (to_mra a, x) ~l~> (to_mra b, to_mra b).
Proof.
    intros Hana. apply local_update_unital_discrete=> z _ Habz.
    split; first done. intros c. specialize (Habz c). set_solver.
  Qed.
(* iris/algebra/mra.v *)
Lemma mra_local_update_get_frag `{!PreOrder R} a b:
    R b a →
    (to_mra a, ε) ~l~> (to_mra a, to_mra b).
Proof.
    intros Hana. apply local_update_unital_discrete=> z _.
    rewrite left_id. intros <-. split; first done.
    apply mra_included; by apply to_mra_included.
  Qed.
(* iris/algebra/mra.v *)
Lemma to_mra_rel_proper :
    Reflexive S →
    Proper (S ==> S ==> iff) R →
    Proper (S ==> (≡@{mra R})) (to_mra).
Proof. intros ? HR a1 a2 Ha b. rewrite !mra_below_to_mra. by apply HR. Qed.