cap_machine.monotone

Author: Amin Timany

From iris.algebra Require Export cmra auth.
From iris.base_logic Require Import base_logic.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
Local Arguments ofe_dist !_ /.
Local Arguments ofe_equiv ! _ /.

Definition monotone {A : Type} (R : relation A) : Type := list A.

Definition principal {A : Type} (R : relation A) (a : A) :
  monotone R := [a].

Section monotone.
Local Set Default Proof Using "Type".
Context {A : ofe} {R : relation A}.
Implicit Types a b : A.
Implicit Types x y : monotone R.

Definition Below (a : A) (x : monotone R) := ∃ b, b ∈ x ∧ R a b.

Lemma Below_app a x y : Below a (x ++ y) ↔ Below a x ∨ Below a y.
Proof.
  split.
  - intros (b & [|]%elem_of_app & ?); [left|right]; exists b; eauto.
  - intros [(b & Hb1 & Hb2)|(b & Hb1 & Hb2)]; exists b; rewrite elem_of_app; eauto.
Unshelve. Fail idtac. Admitted.

Lemma Below_principal a b : Below a (principal R b) ↔ R a b.
Proof.
  split.
  - intros (c & ->%elem_of_list_singleton & ?); done.
  - intros Hab; exists b; split; first apply elem_of_list_singleton; done.
Unshelve. Fail idtac. Admitted.

(* OFE *)
Instance monotone_dist : Dist (monotone R) :=
  λ n x y, ∀ a, Below a x ↔ Below a y.

Instance monotone_equiv : Equiv (monotone R) := λ x y, ∀ n, x ≡{n}≡ y.

Definition monotone_ofe_mixin : OfeMixin (monotone R).
Proof.
  split.
  - rewrite /equiv /monotone_equiv /dist /monotone_dist; intuition auto using O.
  - intros n; split.
    + rewrite /dist /monotone_dist /equiv /monotone_equiv; intuition.
    + rewrite /dist /monotone_dist /equiv /monotone_equiv; intros ? ? Heq a.
      split; apply Heq.
    + rewrite /dist /monotone_dist /equiv /monotone_equiv;
        intros ? ? ? Heq Heq' a.
      split; intros Hxy.
      * apply Heq'; apply Heq; auto.
      * apply Heq; apply Heq'; auto.
  - intros n x y; rewrite /dist /monotone_dist; auto.
Unshelve. Fail idtac. Admitted.
Canonical Structure monotoneC := Ofe (monotone R) monotone_ofe_mixin.

(* CMRA *)
Instance monotone_validN : ValidN (monotone R) := λ n x, True.
Instance monotone_valid : Valid (monotone R) := λ x, True.

Program Instance monotone_op : Op (monotone R) := λ x y, x ++ y.
Instance monotone_pcore : PCore (monotone R) := Some.

Instance monotone_comm : Comm (≡) (@op (monotone R) _).
Proof.
  intros x y n a; rewrite /Below.
  setoid_rewrite elem_of_app; split=> Ha; firstorder.
Unshelve. Fail idtac. Admitted.
Instance monotone_assoc : Assoc (≡) (@op (monotone R) _).
Proof.
  intros x y z n a; rewrite /Below /=.
  repeat setoid_rewrite elem_of_app; split=> Ha; firstorder.
Unshelve. Fail idtac. Admitted.
Lemma monotone_idemp (x : monotone R) : x ⋅ x ≡ x.
Proof.
  intros n a; rewrite /Below.
  setoid_rewrite elem_of_app; split=> Ha; firstorder.
Unshelve. Fail idtac. Admitted.

Instance monotone_validN_ne n :
  Proper (dist n ==> impl) (@validN (monotone R) _ n).
Proof. intros x y ?; rewrite /impl; auto. Qed.
Instance monotone_validN_proper n : Proper (equiv ==> iff) (@validN (monotone R) _ n).
Proof. move=> x y /equiv_dist H; auto. Qed.

Instance monotone_op_ne' x : NonExpansive (op x).
Proof.
  intros n y1 y2; rewrite /dist /monotone_dist /equiv /monotone_equiv /Below.
  rewrite /=; setoid_rewrite elem_of_app => Heq a.
  specialize (Heq a); destruct Heq as [Heq1 Heq2].
  split; intros [b [[Hb|Hb] HRb]]; eauto.
  - destruct Heq1 as [? [? ?]]; eauto.
  - destruct Heq2 as [? [? ?]]; eauto.
Unshelve. Fail idtac. Admitted.
Instance monotone_op_ne : NonExpansive2 (@op (monotone R) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
Instance monotone_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op (monotone R) _) := ne_proper_2 _.

Lemma monotone_included (x y : monotone R) : x ≼ y ↔ y ≡ x ⋅ y.
Proof.
  split; [|by intros ?; exists y].
  by intros [z Hz]; rewrite Hz assoc monotone_idemp.
Unshelve. Fail idtac. Admitted.

Definition monotone_cmra_mixin : CmraMixin (monotone R).
Proof.
  apply cmra_total_mixin; try apply _ || by eauto.
  - intros ?; apply monotone_idemp.
  - rewrite /equiv /monotone_equiv /dist /monotone_dist; eauto.
Unshelve. Fail idtac. Admitted.
Canonical Structure monotoneR : cmra := Cmra (monotone R) monotone_cmra_mixin.

Global Instance monotone_cmra_total : CmraTotal monotoneR.
Proof. rewrite /CmraTotal; eauto. Qed.
Global Instance monotone_core_id (x : monotone R) : CoreId x.
Proof. by constructor. Qed.

Global Instance monotone_cmra_discrete : CmraDiscrete monotoneR.
Proof.
  split; auto.
  intros ? ?.
  rewrite /dist /equiv /= /cmra_dist /cmra_equiv /=
          /monotone_dist /monotone_equiv /dist /monotone_dist; eauto.
Unshelve. Fail idtac. Admitted.

Instance monotone_empty : Unit (monotone R) := @nil A.
Lemma auth_ucmra_mixin : UcmraMixin (monotone R).
Proof. split; done. Qed.

Canonical Structure monotoneUR := Ucmra (monotone R) auth_ucmra_mixin.

Global Instance principal_ne
       `{HRne : !∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
  NonExpansive (principal R).
Proof. intros n a1 a2 Ha; split; rewrite /= !Below_principal !Ha; done. Qed.

Global Instance principal_proper
       {HRne : ∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
  Proper ((≡) ==> (≡)) (principal R) := ne_proper _.

Global Instance principal_discrete a : Discrete (principal R a).
Proof.
  intros y; rewrite /dist /ofe_dist /= /equiv /ofe_equiv /= /monotone_equiv;
    eauto.
Unshelve. Fail idtac. Admitted.

Lemma principal_injN_general n a b :
  principal R a ≡{n}≡ principal R b → R a a → R a b.
Proof.
  rewrite /principal /dist /monotone_dist => Hab Haa.
  - destruct (Hab a) as [Ha _]; edestruct Ha as [? [?%elem_of_list_singleton ?]];
    subst; eauto.
    eexists _; split; first apply elem_of_list_singleton; eauto.
Unshelve. Fail idtac. Admitted.

Lemma principal_inj_general a b :
  principal R a ≡ principal R b → R a a → R a b.
Proof. intros Hab; apply (principal_injN_general 0); eauto. Qed.

Global Instance principal_injN_general' `{!Reflexive R} n :
  Inj (λ a b, R a b ∧ R b a) (dist n) (principal R).
Proof.
  intros x y Hxy; split; eapply (principal_injN_general n); eauto.
Unshelve. Fail idtac. Admitted.

Global Instance principal_inj_general' `{!Reflexive R} :
  Inj (λ a b, R a b ∧ R b a) (≡) (principal R).
Proof.
  intros x y Hxy; specialize (Hxy 0); eapply principal_injN_general'; eauto.
Unshelve. Fail idtac. Admitted.

Global Instance principal_injN `{!Reflexive R} {Has : AntiSymm (≡) R} n :
  Inj (dist n) (dist n) (principal R).
Proof.
  intros x y [Hxy Hyx]%principal_injN_general'.
  erewrite (@anti_symm _ _ _ Has); eauto.
Unshelve. Fail idtac. Admitted.
Global Instance principal_inj `{!Reflexive R} `{!AntiSymm (≡) R} :
  Inj (≡) (≡) (principal R).
Proof. intros ???. apply equiv_dist=>n. by apply principal_injN, equiv_dist. Qed.

Lemma principal_R_opN_base `{!Transitive R} n x y :
  (∀ b, b ∈ y → ∃ c, c ∈ x ∧ R b c) → y ⋅ x ≡{n}≡ x.
Proof.
  intros HR; split; rewrite /op /monotone_op Below_app; [|by firstorder].
  intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done].
  exists d; split; [|transitivity c]; done.
Unshelve. Fail idtac. Admitted.

Lemma principal_R_opN `{!Transitive R} n a b :
  R a b → principal R a ⋅ principal R b ≡{n}≡ principal R b.
Proof.
  intros; apply principal_R_opN_base; intros c; rewrite /principal.
  setoid_rewrite elem_of_list_singleton => ->; eauto.
Unshelve. Fail idtac. Admitted.

Lemma principal_R_op `{!Transitive R} a b :
  R a b → principal R a ⋅ principal R b ≡ principal R b.
Proof. by intros ? ?; apply principal_R_opN. Qed.

Lemma principal_op_RN n a b x :
  R a a → principal R a ⋅ x ≡{n}≡ principal R b → R a b.
Proof.
  intros Ha HR.
  destruct (HR a) as [[z [HR1%elem_of_list_singleton HR2]] _];
    last by subst; eauto.
  rewrite /op /monotone_op /principal Below_app Below_principal; auto.
Unshelve. Fail idtac. Admitted.

Lemma principal_op_R a b x :
  R a a → principal R a ⋅ x ≡ principal R b → R a b.
Proof. intros ? ?; eapply (principal_op_RN 0); eauto. Qed.

Lemma principal_op_R' `{!Reflexive R} a b x :
  principal R a ⋅ x ≡ principal R b → R a b.
Proof. intros; eapply principal_op_R; eauto. Qed.

Lemma principal_includedN `{!PreOrder R} n a b :
  principal R a ≼{n} principal R b ↔ R a b.
Proof.
  split.
  - intros [z Hz]; eapply principal_op_RN; last by rewrite Hz; eauto.
    reflexivity.
  - intros ?; exists (principal R b); rewrite principal_R_opN; eauto.
Unshelve. Fail idtac. Admitted.

Lemma principal_included `{!PreOrder R} a b :
  principal R a ≼ principal R b ↔ R a b.
Proof.
  split.
  - intros [z Hz]; eapply principal_op_R; last by rewrite Hz; eauto.
    reflexivity.
  - intros ?; exists (principal R b); rewrite principal_R_op; eauto.
Unshelve. Fail idtac. Admitted.

Internalized properties
Lemma monotone_equivI `{!(∀ n : nat, Proper (dist n ==> dist n ==> iff) R)}
      `{!Reflexive R} `{!AntiSymm (≡) R} {M} a b :
  principal R a ≡ principal R b ⊣⊢ (a ≡ b : uPred M).
Proof.
  uPred.unseal. do 2 split.
  - intros Hx. exact: principal_injN.
  - intros Hx. exact: principal_ne.
Unshelve. Fail idtac. Admitted.

Lemma monotone_local_update_grow `{!Transitive R} a q na:
  R a na →
  (principal R a, q) ~l~> (principal R na, principal R na).
Proof.
  intros Hana Hanb.
  apply local_update_unital_discrete.
  intros z _ Habz.
  split; first done.
  intros n; specialize (Habz n).
  intros x; split.
  - intros (y & ->%elem_of_list_singleton & Hy2).
    by exists na; split; first constructor.
  - intros (y & [->|Hy1]%elem_of_cons & Hy2).
    + by exists na; split; first constructor.
    + exists na; split; first constructor.
      specialize (Habz x) as [_ [c [->%elem_of_list_singleton Hc2]]].
      { exists y; split; first (by apply elem_of_app; right); eauto. }
      etrans; eauto.
Unshelve. Fail idtac. Admitted.

Lemma monotone_local_update_get_frag `{!PreOrder R} a na:
  R na a →
  (principal R a, ε) ~l~> (principal R a, principal R na).
Proof.
  intros Hana.
  apply local_update_unital_discrete.
  intros z _.
  rewrite left_id.
  intros <-.
  split; first done.
  apply monotone_included.
  by apply principal_included.
Unshelve. Fail idtac. Admitted.

Lemma monotone_update `{!PreOrder R} a b c:
  R a b →
  R c b →
  ● principal R a ~~> ● principal R b ⋅ ◯ principal R c.
Proof.
  intros Hab Hcb.
  etrans.
  { apply auth_update_alloc; apply (monotone_local_update_grow _ _ b); done. }
  etrans; first apply cmra_update_op_l.
  apply auth_update_alloc.
  apply monotone_local_update_get_frag; done.
Unshelve. Fail idtac. Admitted.

End monotone.

Arguments monotoneC {_} _.
Arguments monotoneR {_} _.
Arguments monotoneUR {_} _.

Having an instance of this class for a relation R allows almost all lemmas provided in this module to be used. See type classes required by some of preceding the lemmas and instances in the to see how this works. The only lemma that requires extra conditions on R is the injectivity of principal which requires antisymmetry.
Class ProperPreOrder {A : Type} `{Dist A} (R : relation A) := {
  ProperPreOrder_preorder :: PreOrder R;
  ProperPreOrder_ne :: ∀ n, Proper ((dist n) ==> (dist n) ==> iff) R
}.