Union of non-empty things is non-empty.

cmra_restrictions.v

From iris.algebra Require Export ofe monoid cmra.
From iris.prelude Require Import options.
Locate pmap_omap.
Section restrict_validity.
  Definition restrictV (A : Type) (P : nat → A → Prop) := A.
  Local Instance restrictV_validN A P : ValidN (restrictV A P) := P.
  Local Instance restrictV_valid A P : Valid (restrictV A P) := λ a, ∀ n, P n a.

  Definition restrictV_cmra {A : cmra} PvalidN
  (* the new validity restricts the old one *)
  (H1 : ∀ n a, PvalidN n a → ✓{n} a)
  (* the new validity is compatible with equivalence *)
  (H2 : ∀ n : nat, Proper (dist n ==> impl) (PvalidN n))
  (* the new validity is down-closed on the step-index *)
  (H3 : ∀ n a, PvalidN (S n) a → PvalidN n a)
  (* the new validity is down-closed on the resource *)
  (H4 : ∀ n a b, PvalidN n (a ⋅ b) → PvalidN n a) :
  CmraMixin (restrictV A PvalidN).
  Proof.
    split.
    1,2,6,7,8,9,10: apply A.
    - apply H2.
    - intros x. done.
    - apply H3.
    - apply H4.
    - intros n x y1 y2 H%H1. by apply A.
  Qed.
End restrict_validity.

Section sig_cmra.

  (* In order for this CMRA to be well-defined, the core (if defined) must satisfy P again. *)
  (* In other words, P is closed under pcore. *)
  Definition PCoreRestrictable `{PCore A} (P : A → Prop) := ∀ a, from_option P True (pcore a).
  Arguments PCoreRestrictable A {_} P.
  Existing Class PCoreRestrictable.

  (* tricky dependent matches, which avoid the need for P to be ProofIrrel. *)
  Program Definition sig_pcore_match `{PCoreRestrictable A P} :=
    λ (a : sig P) (r: option A), match r as rr return pcore (`a) = rr → option (sig P) 
          with Some x => λ HH, Some (x ↾ _) | None => λ _, None end.
  Next Obligation.
    intros A H P HP1 [a Ha] pc x Hx.
    specialize (HP1 a). rewrite Hx in HP1. apply HP1.
  Qed.
  Local Instance sig_pcore `{PCoreRestrictable A P} : PCore (sig P) :=
    λ a, sig_pcore_match a _ eq_refl.

  (* tricky reasoning with dependent matches *)
  Lemma sig_pcore_match_Some `{PCoreRestrictable A P} (a b : sig P) x HH :
    sig_pcore_match a x HH = Some b → x = Some (`b).
  Proof. rewrite /sig_pcore_match. destruct x; last done. by intros [= <-]. Qed.
  Lemma sig_pcore_match_Some_eq `{PCoreRestrictable A P} (a : sig P) x HH :
    sig_pcore_match a x HH = sig_pcore_match a _ eq_refl.
  Proof. by destruct HH. Qed.
  Lemma sig_pcore_Some `{PCoreRestrictable A P} (a b : sig P) :
    pcore a = Some b → pcore (`a) = Some (`b).
  Proof.
    intros HH. rewrite /pcore /= /sig_pcore in HH.
    apply sig_pcore_match_Some in HH. done.
  Qed.
  Lemma sig_pcore_has_proof `{PCoreRestrictable A P} (a : sig P) {b} :
    pcore (`a) = Some b → ∃ prf, pcore a = Some (b ↾ prf).
  Proof.
    intros HH. rewrite /= /pcore /sig_pcore /=.
    rewrite -(sig_pcore_match_Some_eq a (Some b) HH). simpl.
    by eexists.
  Qed.

  (* Similarly, in order to be well-defined, P must be closed under op. *)
  Definition OpRestrictable `{Op A} (P : A → Prop) := ∀ a b, P (a ⋅ b).
  Arguments OpRestrictable A {_} P.
  Existing Class OpRestrictable.
  Local Program Instance sig_op `{OpRestrictable A P} : Op (sig P) :=
    λ a b, (`a ⋅ `b) ↾ _.
  Next Obligation. intros A H P HP1 ??. apply HP1. Qed.
  Lemma sig_op_def `{OpRestrictable A P} (a b : sig P) : proj1_sig (a ⋅ b) = (`a) ⋅ (`b).
  Proof. simpl. done. Qed.

  Local Instance sig_valid `{Valid A} (P : A → Prop) : Valid (sig P) := λ a, ✓ (`a).
  Local Instance sig_validN `{ValidN A} (P : A → Prop) : ValidN (sig P) := λ n a, ✓{n} (`a).

  (* Finally, we also require that the [cmra_restrict] law produces results in P. *)
  Definition RestrictedExtend (A:ofe) (P : A → Prop) `{Op A} `{!OpRestrictable A P} `{ValidN A} :=
    ∀ n (x y1 y2 : sig P), ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
      { z1 : A & { z2 : A | proj1_sig x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ `y1 ∧ z2 ≡{n}≡ `y2 ∧ P z1 ∧ P z2 }}.

  Definition sig_cmra {A : cmra} (P : A → Prop)
    (HH1 : PCoreRestrictable A P)
    (HH2 : OpRestrictable A P)
    (HH3 : RestrictedExtend A P) :
    CmraMixin (sig P).
  Proof.
    split.
    - intros [x Hx] n [y1 Hy1] [y2 Hy2]. by eapply (@cmra_op_ne A).
    - intros n [x Hx] [y Hy] [cx Hcx] Heq Hcore%sig_pcore_Some.
      simpl in Hcore.
      pose proof (cmra_pcore_ne n x y cx Heq Hcore) as (cy & Hcy1 & Hcy2).
      edestruct (sig_pcore_has_proof (y ↾ Hy) Hcy1) as [prf Hprf].
      eexists. split; first done. apply Hcy2.
    - intros ? [] []. eapply (@cmra_validN_ne A).
    - intros []. eapply (@cmra_valid_validN A).
    - intros ? []. eapply (@cmra_validN_S A).
    - intros [] [] []. eapply (@cmra_assoc A).
    - intros [] []. eapply (@cmra_comm A).
    - intros [] [] H%sig_pcore_Some. eapply (@cmra_pcore_l A). done.
    - intros [x Hx] [cx Hcx] H%sig_pcore_Some. simpl in H.
      pose proof (cmra_pcore_idemp x cx H) as HH.
      assert (∃ cx', Some cx' = pcore cx) as [cx' Hcx'].
      { destruct (pcore cx); first by eexists. exfalso. inversion HH. }
      odestruct (sig_pcore_has_proof (cx ↾ Hcx)) as [prf Hprf]; first done.
      rewrite Hprf. f_equiv. rewrite -Hcx' in HH. inversion HH; simplify_eq. done.
    - intros [x Hx] [y Hy] [cx Hcx] Hxy H%sig_pcore_Some. simpl in H.
      destruct Hxy as [[z Hz] HHz]. rewrite sig_equiv_def sig_op_def /= in HHz.
      destruct (cmra_pcore_mono x y cx) as (cy & Hcy & HHcy).
      { by exists z. } { done. }
      odestruct (sig_pcore_has_proof (y ↾ Hy)) as [prf Hprf]; first done.
      eexists; split; first done.
      exists (cy ↾ prf). rewrite sig_equiv_def sig_op_def /=. destruct HHcy as (cz & Hcz).
      rewrite {2} Hcz (cmra_assoc cx) -cmra_pcore_dup //.
    - intros ? [] []. eapply (@cmra_validN_op_l A).
    - intros n [x Hx] [y1 Hy1] [y2 Hy2] Hxv Hequiv.
      destruct (HH3 n _ _ _ Hxv Hequiv) as (z1 & z2 & Heq1 & Heq2 & Heq3 & Hz1 & Hz2).
      exists (z1 ↾ Hz1), (z2 ↾ Hz2). split.
      + rewrite sig_equiv_def //.
      + rewrite sig_dist_def //.
  Qed.

  (* [RestrictedExtend] holds when P is compatible with ≡{0}≡, which is often the case,
     e.g. if the RA is discrete and Leibniz. *)
  Lemma RestrictedExtend_from_Proper (A:cmra) (P : A → Prop) `{!OpRestrictable A P} :
    Proper (dist 0 ==> iff) P → RestrictedExtend A P.
  Proof.
    intros Hproper n [x Hx] [y1 Hy1] [y2 Hy2] Hxv Hequiv.
    destruct (cmra_extend n x y1 y2 Hxv Hequiv) as (z1 & z2 & Hxz & Hz1n & Hz2n).
    exists z1, z2. do 3 (split; first done).
    split. all: eapply Hproper; [eapply dist_le;[eassumption|lia]|done].
  Qed.

End sig_cmra.

Section nocore_cmra.
  (* when you want to delete the core *)
  Definition no_core (A:Type) := A.
  Local Program Instance no_core_pcore A : PCore (no_core A) := λ _, None.

  Definition no_core_cmra {A : cmra} :
    CmraMixin (no_core A).
  Proof.
    split.
    - apply _.
    - intros ????? [=].
    - apply _.
    - apply (@cmra_valid_validN A).
    - apply (@cmra_validN_S A).
    - apply (@cmra_assoc A).
    - apply (@cmra_comm A).
    - intros ?? [=].
    - intros ?? [=].
    - intros ???? [=].
    - apply (@cmra_validN_op_l A).
    - apply (@cmra_extend A).
  Qed.

  (* this is useful when the core is not included in your predicate *)
  Lemma no_core_PCoreRestrictable A (P : no_core A → Prop) : PCoreRestrictable P.
  Proof. done. Qed.

End nocore_cmra.

nonempty.v

From stdpp Require Import gmap base relations prelude tactics options.
From Coq.ssr Require Export ssreflect.

Definition nonzero (n : nat) := match n with 0 => False | _ => True end.
Lemma nonzero_unique n (H1 H2 : nonzero n) : H1 = H2.
Proof.
  destruct n; first done.
  destruct H1, H2. done.
Qed.
Lemma nonzero_def n : nonzero n ↔ n ≠ 0.
Proof. by destruct n. Qed.
Definition nonempty (p : gmap nat nat) := nonzero (size p).
Lemma nonempty_unique p (H1 H2 : nonempty p) : H1 = H2.
Proof. apply nonzero_unique. Qed.
Lemma nonempty_def p : nonempty p ↔ p ≠ ∅.
Proof. rewrite /nonempty nonzero_def map_size_non_empty_iff. done. Qed.

Lemma union_nonempty p1 p2 (H1 : nonempty p1) (H2 : nonempty p2) : nonempty (p1 ∪ p2).
Proof.
  rewrite !nonempty_def in H1,H2|-*.
  eapply map_choose in H1 as (k & v & Hkv).
  intros Hempty.
  assert ((p1 ∪ p2) !! k = None) as [Hn1 Hn2]%lookup_union_None.
  { rewrite Hempty lookup_empty //. }
  congruence.
Qed.