Library iris.base_logic.upred

From stdpp Require Import finite.
From iris.bi Require Import notation.
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ _) ⇒ etrans; [eassumption|] : core.
Local Hint Extern 1 (_ _) ⇒ etrans; [|eassumption] : core.
Local Hint Extern 10 (_ _) ⇒ lia : core.

The basic definition of the uPred type, its metric and functor laws. You probably do not want to import this file. Instead, import base_logic.base_logic; that will also give you all the primitive and many derived laws for the logic.


Record uPred (M : ucmraT) : Type := UPred {
  uPred_holds :> nat M Prop;

  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1 x1 ≼{n1} x2 n2 n1 uPred_holds n2 x2
}.
Bind Scope bi_scope with uPred.
Arguments uPred_holds {_} _%I _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3 := {}.

Section cofe.
  Context {M : ucmraT}.

  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
    { uPred_in_equiv : n x, ✓{n} x P n x Q n x }.
  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
    { uPred_in_dist : n' x, n' n ✓{n'} x P n' x Q n' x }.
  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
  Definition uPred_ofe_mixin : OfeMixin (uPred M).
  Proof.
    split.
    - intros P Q; split.
      + by intros HPQ n; spliti x ??; apply HPQ.
      + intros HPQ; splitn x ?; apply HPQ with n; auto.
    - intros n; split.
      + by intros P; splitx i.
      + by intros P Q HPQ; splitx i ??; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; spliti x ??.
        by trans (Q i x);[apply HP|apply HQ].
    - intros n P Q HPQ; spliti x ??; apply HPQ; auto.
  Qed.
  Canonical Structure uPredO : ofeT := OfeT (uPred M) uPred_ofe_mixin.

  Program Definition uPred_compl : Compl uPredO := λ c,
    {| uPred_holds n x := n', n' n ✓{n'}x c n' n' x |}.
  Next Obligation.
    move⇒ /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono.
    eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
    eapply cmra_includedN_le=>//; lia. done.
  Qed.
  Global Program Instance uPred_cofe : Cofe uPredO := {| compl := uPred_compl |}.
  Next Obligation.
    intros n c; spliti x Hin Hv.
    etrans; [|by symmetry; apply (chain_cauchy c i n)]. splitH; [by apply H|].
    repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
  Qed.
End cofe.
Arguments uPredO : clear implicits.

Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
  intros x1 x2 Hx; split⇒ ?; eapply uPred_mono; eauto; by rewrite Hx.
Qed.
Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.

Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
  P ≡{n2}≡ Q n2 n1 ✓{n2} x Q n1 x P n2 x.
Proof.
  intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
Qed.

Lemma uPred_alt {M : ucmraT} (P: nat M Prop) :
  ( n1 n2 x1 x2, P n1 x1 x1 ≼{n1} x2 n2 n1 P n2 x2)
  ( ( x n1 n2, n2 n1 P n1 x P n2 x)
   ( n x1 x2, x1 ≡{n}≡ x2 m, m n P m x1 P m x2)
   ( n x1 x2, x1 ≼{n} x2 m, m n P m x1 P m x2)
  ).
Proof.
  assert ( n1 n2 (x1 x2 : M), n2 n1 x1 ≡{n1}≡ x2 x1 ≼{n2} x2).
  { intros ????? H. eapply cmra_includedN_le; last done. by rewrite H. }
  
  split.
  - intros Hupred. repeat split; eauto using cmra_includedN_le.
  - intros (Hdown & _ & Hmono) **. eapply Hmono; [done..|]. eapply Hdown; done.
Qed.

functor
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
  `{!CmraMorphism f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.

Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
  `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
  intros x1 x2 Hx; splitn' y ??.
  split; apply Hx; auto using cmra_morphism_validN.
Qed.
Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P P.
Proof. by splitn x ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
    `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
  uPred_map (g f) P uPred_map f (uPred_map g P).
Proof. by splitn x Hx. Qed.
Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
      `{!CmraMorphism f} `{!CmraMorphism g}:
  ( x, f x g x) x, uPred_map f x uPred_map g x.
Proof. intros Hf P; splitn x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
Definition uPredO_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
  uPredO M1 -n> uPredO M2 := OfeMor (uPred_map f : uPredO M1 uPredO M2).
Lemma uPredO_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
    `{!CmraMorphism f, !CmraMorphism g} n :
  f ≡{n}≡ g uPredO_map f ≡{n}≡ uPredO_map g.
Proof.
  by intros Hfg P; splitn' y ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.

Program Definition uPredOF (F : urFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := uPredO (urFunctor_car F B A);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredO_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
  intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
  apply uPredO_map_ne, urFunctor_ne; split; by apply HPQ.
Qed.
Next Obligation.
  intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
  apply uPred_map_exty. by rewrite urFunctor_id.
Qed.
Next Obligation.
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' P; simpl. rewrite -uPred_map_compose.
  apply uPred_map_exty; apply urFunctor_compose.
Qed.

Instance uPredOF_contractive F :
  urFunctorContractive F oFunctorContractive (uPredOF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredO_map_ne, urFunctor_contractive.
  destruct n; split; by apply HPQ.
Qed.

logical entailement
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails : n x, ✓{n} x P n x Q n x }.
Hint Resolve uPred_mono : uPred_def.

logical connectives
Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
  {| uPred_holds n x := φ |}.
Solve Obligations with done.
Definition uPred_pure_aux : seal (@uPred_pure_def). by eexists. Qed.
Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
Definition uPred_pure_eq :
  @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).

Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_and_aux : seal (@uPred_and_def). by eexists. Qed.
Definition uPred_and {M} := uPred_and_aux.(unseal) M.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).

Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x Q n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed.
Definition uPred_or {M} := uPred_or_aux.(unseal) M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).

Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := n' x',
       x x' n' n ✓{n'} x' P n' x' Q n' x' |}.
Next Obligation.
  intros M P Q n1 n1' x1 x1' HPQ [x2 Hx1'] Hn1 n2 x3 [x4 Hx3] ?; simpl in ×.
  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
  eapply HPQ; auto. (x2 x4); by rewrite assoc.
Qed.
Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. Qed.
Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
Definition uPred_impl_eq :
  @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).

Program Definition uPred_forall_def {M A} (Ψ : A uPred M) : uPred M :=
  {| uPred_holds n x := a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_forall_aux : seal (@uPred_forall_def). by eexists. Qed.
Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
Definition uPred_forall_eq :
  @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).

Program Definition uPred_exist_def {M A} (Ψ : A uPred M) : uPred M :=
  {| uPred_holds n x := a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 with uPred_def.
Definition uPred_exist_aux : seal (@uPred_exist_def). by eexists. Qed.
Definition uPred_exist {M A} := uPred_exist_aux.(unseal) M A.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).

Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
  {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). by eexists. Qed.
Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
Definition uPred_internal_eq_eq:
  @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).

Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := x1 x2, x ≡{n}≡ x1 x2 P n x1 Q n x2 |}.
Next Obligation.
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
   x1, (x2 z); split_and?; eauto using uPred_mono, cmra_includedN_l.
  eapply dist_le, Hn. by rewrite Hy Hx assoc.
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed.
Definition uPred_sep {M} := uPred_sep_aux.(unseal) M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).

Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := n' x',
       n' n ✓{n'} (x x') P n' x' Q n' (x x') |}.
Next Obligation.
  intros M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in ×.
  eapply uPred_mono with n3 (x1 x3);
    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. Qed.
Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
Definition uPred_wand_eq :
  @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).

Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
Definition uPred_plainly_eq :
  @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).

Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (core x) |}.
Next Obligation.
  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed.
Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
Definition uPred_persistently_eq :
  @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).

Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 True | S n' P n' x end |}.
Next Obligation.
  intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
Qed.
Definition uPred_later_aux : seal (@uPred_later_def). by eexists. Qed.
Definition uPred_later {M} := uPred_later_aux.(unseal) M.
Definition uPred_later_eq :
  @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).

Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
  {| uPred_holds n x := a ≼{n} x |}.
Next Obligation.
  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn. eapply cmra_includedN_le=>//.
   (a' x2). by rewrite Hx(assoc op) Hx1.
Qed.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed.
Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
Definition uPred_ownM_eq :
  @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).

Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
  {| uPred_holds n x := ✓{n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). by eexists. Qed.
Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
Definition uPred_cmra_valid_eq :
  @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).

Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
  {| uPred_holds n x := k yf,
      k n ✓{k} (x yf) x', ✓{k} (x' yf) Q k x' |}.
Next Obligation.
  intros M Q n1 n2 x1 x2 HQ [x3 Hx] Hn k yf Hk.
  rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy.
  destruct (HQ k (x3 yf)) as (x'&?&?); [auto|by rewrite assoc|].
   (x' x3); split; first by rewrite -assoc.
  eauto using uPred_mono, cmra_includedN_l.
Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M.
Definition uPred_bupd_eq :
  @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).

Global uPred-specific Notation
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.

Primitive logical rules. These are not directly usable later because they do not refer to the BI connectives.
Module uPred_primitive.
Definition unseal_eqs :=
  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
  uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
  uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
  uPred_cmra_valid_eq, @uPred_bupd_eq).
Ltac unseal :=
  rewrite !unseal_eqs /=.

Section primitive.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails : core.

Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope.

Notation "'True'" := (uPred_pure True) : bi_scope.
Notation "'False'" := (uPred_pure False) : bi_scope.
Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope.
Infix "∧" := uPred_and : bi_scope.
Infix "∨" := uPred_or : bi_scope.
Infix "→" := uPred_impl : bi_scope.
Notation "∀ x .. y , P" :=
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
Notation "∃ x .. y , P" :=
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
Infix "∗" := uPred_sep : bi_scope.
Infix "-∗" := uPred_wand : bi_scope.
Notation "□ P" := (uPred_persistently P) : bi_scope.
Notation "■ P" := (uPred_plainly P) : bi_scope.
Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
Notation "▷ P" := (uPred_later P) : bi_scope.
Notation "|==> P" := (uPred_bupd P) : bi_scope.

Entailment
Lemma entails_po : PreOrder (⊢).
Proof.
  split.
  - by intros P; splitx i.
  - by intros P Q Q' HP HQ; splitx i ??; apply HQ, HP.
Qed.
Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
Proof. intros P Q HPQ HQP; splitx n; by split; [apply HPQ|apply HQP]. Qed.
Lemma equiv_spec P Q : (P ⊣⊢ Q) (P Q) (Q P).
Proof.
  split.
  - intros HPQ; split; splitx i; apply HPQ.
  - intros [??]. exact: entails_anti_sym.
Qed.
Lemma entails_lim (cP cQ : chain (uPredO M)) :
  ( n, cP n cQ n) compl cP compl cQ.
Proof.
  intros Hlim; splitn m ? HP.
  eapply uPred_holds_ne, Hlim, HP; rewrite ?conv_compl; eauto.
Qed.

Non-expansiveness and setoid morphisms
Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M).
Proof. intros φ1 φ2 Hφ. by unseal; split⇒ -[|m] ?; try apply Hφ. Qed.

Lemma and_ne : NonExpansive2 (@uPred_and M).
Proof.
  intros n P P' HP Q Q' HQ; unseal; splitx n' ??.
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.

Lemma or_ne : NonExpansive2 (@uPred_or M).
Proof.
  intros n P P' HP Q Q' HQ; splitx n' ??.
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.

Lemma impl_ne :
  NonExpansive2 (@uPred_impl M).
Proof.
  intros n P P' HP Q Q' HQ; splitx n' ??.
  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
Qed.

Lemma sep_ne : NonExpansive2 (@uPred_sep M).
Proof.
  intros n P P' HP Q Q' HQ; splitn' x ??.
  unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
     x1, x2; split_and!; try (apply HP || apply HQ);
    eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.

Lemma wand_ne :
  NonExpansive2 (@uPred_wand M).
Proof.
  intros n P P' HP Q Q' HQ; splitn' x ??; unseal; split; intros HPQ x' n'' ???;
    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.

Lemma internal_eq_ne (A : ofeT) :
  NonExpansive2 (@uPred_internal_eq M A).
Proof.
  intros n x x' Hx y y' Hy; splitn' z; unseal; split; intros; simpl in ×.
  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.

Lemma forall_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
Proof.
  by intros Ψ1 Ψ2 ; unseal; splitn' x; split; intros HP a; apply .
Qed.

Lemma exist_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Proof.
  intros Ψ1 Ψ2 .
  unseal; splitn' x ??; split; intros [a ?]; a; by apply .
Qed.

Lemma later_contractive : Contractive (@uPred_later M).
Proof.
  unseal; intros [|n] P Q HPQ; split⇒ -[|n'] x ?? //=; try lia.
  apply HPQ; eauto using cmra_validN_S.
Qed.

Lemma plainly_ne : NonExpansive (@uPred_plainly M).
Proof.
  intros n P1 P2 HP.
  unseal; splitn' x; split; apply HP; eauto using @ucmra_unit_validN.
Qed.

Lemma persistently_ne : NonExpansive (@uPred_persistently M).
Proof.
  intros n P1 P2 HP.
  unseal; splitn' x; split; apply HP; eauto using @cmra_core_validN.
Qed.

Lemma ownM_ne : NonExpansive (@uPred_ownM M).
Proof.
  intros n a b Ha.
  unseal; splitn' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.

Lemma cmra_valid_ne {A : cmraT} :
  NonExpansive (@uPred_cmra_valid M A).
Proof.
  intros n a b Ha; unseal; splitn' x ? /=.
  by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.

Lemma bupd_ne : NonExpansive (@uPred_bupd M).
Proof.
  intros n P Q HPQ.
  unseal; splitn' x; split; intros HP k yf ??;
    destruct (HP k yf) as (x'&?&?); auto;
     x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
Qed.

Introduction and elimination rules
Lemma pure_intro φ P : φ P φ.
Proof. by intros ?; unseal; split. Qed.
Lemma pure_elim' φ P : (φ True P) φ P.
Proof. unseal; intros HP; splitn x ??. by apply HP. Qed.
Lemma pure_forall_2 {A} (φ : A Prop) : ( x : A, φ x) x : A, φ x.
Proof. by unseal. Qed.

Lemma and_elim_l P Q : P Q P.
Proof. by unseal; splitn x ? [??]. Qed.
Lemma and_elim_r P Q : P Q Q.
Proof. by unseal; splitn x ? [??]. Qed.
Lemma and_intro P Q R : (P Q) (P R) P Q R.
Proof. intros HQ HR; unseal; splitn x ??; by split; [apply HQ|apply HR]. Qed.

Lemma or_intro_l P Q : P P Q.
Proof. unseal; splitn x ??; left; auto. Qed.
Lemma or_intro_r P Q : Q P Q.
Proof. unseal; splitn x ??; right; auto. Qed.
Lemma or_elim P Q R : (P R) (Q R) P Q R.
Proof. intros HP HQ; unseal; splitn x ? [?|?]. by apply HP. by apply HQ. Qed.

Lemma impl_intro_r P Q R : (P Q R) P Q R.
Proof.
  unseal; intros HQ; splitn x ?? n' x' ????. apply HQ;
    naive_solver eauto using uPred_mono, cmra_included_includedN.
Qed.
Lemma impl_elim_l' P Q R : (P Q R) P Q R.
Proof. unseal; intros HP ; splitn x ? [??]; apply HP with n x; auto. Qed.

Lemma forall_intro {A} P (Ψ : A uPred M): ( a, P Ψ a) P a, Ψ a.
Proof. unseal; intros HPΨ; splitn x ?? a; by apply HPΨ. Qed.
Lemma forall_elim {A} {Ψ : A uPred M} a : ( a, Ψ a) Ψ a.
Proof. unseal; splitn x ? HP; apply HP. Qed.

Lemma exist_intro {A} {Ψ : A uPred M} a : Ψ a a, Ψ a.
Proof. unseal; splitn x ??; by a. Qed.
Lemma exist_elim {A} (Φ : A uPred M) Q : ( a, Φ a Q) ( a, Φ a) Q.
Proof. unseal; intros HΦΨ; splitn x ? [a ?]; by apply HΦΨ with a. Qed.

BI connectives
Lemma sep_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
Proof.
  intros HQ HQ'; unseal.
  split; intros n' x ? (x1&x2&?&?&?); x1,x2; ofe_subst x;
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
Qed.
Lemma True_sep_1 P : P True P.
Proof.
  unseal; split; intros n x ??. (core x), x. by rewrite cmra_core_l.
Qed.
Lemma True_sep_2 P : True P P.
Proof.
  unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
    eauto using uPred_mono, cmra_includedN_r.
Qed.
Lemma sep_comm' P Q : P Q Q P.
Proof.
  unseal; split; intros n x ? (x1&x2&?&?&?); x2, x1; by rewrite (comm op).
Qed.
Lemma sep_assoc' P Q R : (P Q) R P (Q R).
Proof.
  unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
   y1, (y2 x2); split_and?; auto.
  + by rewrite (assoc op) -Hy -Hx.
  + by y2, x2.
Qed.
Lemma wand_intro_r P Q R : (P Q R) P Q -∗ R.
Proof.
  unsealHPQR; splitn x ?? n' x' ???; apply HPQR; auto.
   x, x'; split_and?; auto.
  eapply uPred_mono with n x; eauto using cmra_validN_op_l.
Qed.
Lemma wand_elim_l' P Q R : (P Q -∗ R) P Q R.
Proof.
  unsealHPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
  eapply HPQR; eauto using cmra_validN_op_l.
Qed.

Persistently
Lemma persistently_mono P Q : (P Q) P Q.
Proof. intros HP; unseal; splitn x ? /=. by apply HP, cmra_core_validN. Qed.
Lemma persistently_elim P : P P.
Proof.
  unseal; splitn x ? /=.
  eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
Qed.
Lemma persistently_idemp_2 P : P P.
Proof. unseal; splitn x ?? /=. by rewrite cmra_core_idemp. Qed.

Lemma persistently_forall_2 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof. by unseal. Qed.
Lemma persistently_exist_1 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof. by unseal. Qed.

Lemma persistently_and_sep_l_1 P Q : P Q P Q.
Proof.
  unseal; splitn x ? [??]; (core x), x; simpl in ×.
  by rewrite cmra_core_l.
Qed.

Plainly
Lemma plainly_mono P Q : (P Q) P Q.
Proof. intros HP; unseal; splitn x ? /=. apply HP, ucmra_unit_validN. Qed.
Lemma plainly_elim_persistently P : P P.
Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
Lemma plainly_idemp_2 P : P P.
Proof. unseal; splitn x ?? //. Qed.

Lemma plainly_forall_2 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof. by unseal. Qed.
Lemma plainly_exist_1 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof. by unseal. Qed.

Lemma prop_ext_2 P Q : ((P -∗ Q) (Q -∗ P)) P Q.
Proof.
  unseal; splitn x ? /= HPQ. splitn' x' ??.
    move: HPQ⇒ [] /(_ n' x'); rewrite !left_id⇒ ?.
    move⇒ /(_ n' x'); rewrite !left_id⇒ ?. naive_solver.
Qed.

Lemma persistently_impl_plainly P Q : ( P Q) ( P Q).
Proof.
  unseal; split⇒ /= n x ? HPQ n' x' ????.
  eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
  apply (HPQ n' x); eauto using cmra_validN_le.
Qed.

Lemma plainly_impl_plainly P Q : ( P Q) (■ P Q).
Proof.
  unseal; split⇒ /= n x ? HPQ n' x' ????.
  eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
  apply (HPQ n' x); eauto using cmra_validN_le.
Qed.

Later
Lemma later_mono P Q : (P Q) P Q.
Proof.
  unsealHP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
Qed.
Lemma later_intro P : P P.
Proof.
  unseal; split⇒ -[|n] /= x ? HP; first done.
  apply uPred_mono with (S n) x; eauto using cmra_validN_S.
Qed.
Lemma later_forall_2 {A} (Φ : A uPred M) : ( a, Φ a) a, Φ a.
Proof. unseal; by split⇒ -[|n] x. Qed.
Lemma later_exist_false {A} (Φ : A uPred M) :
  ( a, Φ a) False ( a, Φ a).
Proof. unseal; split⇒ -[|[|n]] x /=; eauto. Qed.
Lemma later_sep_1 P Q : (P Q) P Q.
Proof.
  unseal; splitn x ?.
  destruct n as [|n]; simpl.
  { by x, (core x); rewrite cmra_core_r. }
  intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
    as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in ×.
   y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
Qed.
Lemma later_sep_2 P Q : P Q (P Q).
Proof.
  unseal; splitn x ?.
  destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
   x1, x2; eauto using dist_S.
Qed.

Lemma later_false_em P : P False ( False P).
Proof.
  unseal; split⇒ -[|n] x ? /= HP; [by left|right].
  intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
Qed.

Lemma later_persistently_1 P : P P.
Proof. by unseal. Qed.
Lemma later_persistently_2 P : P P.
Proof. by unseal. Qed.
Lemma later_plainly_1 P : P P.
Proof. by unseal. Qed.
Lemma later_plainly_2 P : P P.
Proof. by unseal. Qed.

Internal equality
Lemma internal_eq_refl {A : ofeT} P (a : A) : P (a a).
Proof. unseal; by splitn x ??; simpl. Qed.
Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A uPred M) :
  NonExpansive Ψ a b Ψ a Ψ b.
Proof. intros . unseal; splitn x ?? n' x' ??? Ha. by apply with n a. Qed.

Lemma fun_ext {A} {B : A ofeT} (g1 g2 : discrete_fun B) :
  ( i, g1 i g2 i) g1 g2.
Proof. by unseal. Qed.
Lemma sig_eq {A : ofeT} (P : A Prop) (x y : sigO P) :
  proj1_sig x proj1_sig y x y.
Proof. by unseal. Qed.

Lemma later_eq_1 {A : ofeT} (x y : A) : Next x Next y (x y).
Proof. by unseal. Qed.
Lemma later_eq_2 {A : ofeT} (x y : A) : (x y) Next x Next y.
Proof. by unseal. Qed.

Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a a b a b.
Proof.
  unseal⇒ ?. splitn x ?. by apply (discrete_iff n).
Qed.

Basic update modality
Lemma bupd_intro P : P |==> P.
Proof.
  unseal. splitn x ? HP k yf ?; x; split; first done.
  apply uPred_mono with n x; eauto using cmra_validN_op_l.
Qed.
Lemma bupd_mono P Q : (P Q) (|==> P) |==> Q.
Proof.
  unseal. intros HPQ; splitn x ? HP k yf ??.
  destruct (HP k yf) as (x'&?&?); eauto.
   x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
Qed.
Lemma bupd_trans P : (|==> |==> P) |==> P.
Proof. unseal; split; naive_solver. Qed.
Lemma bupd_frame_r P R : (|==> P) R |==> P R.
Proof.
  unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
  destruct (HP k (x2 yf)) as (x'&?&?); eauto.
  { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
   (x' x2); split; first by rewrite -assoc.
   x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
Qed.
Lemma bupd_plainly P : (|==> P) P.
Proof.
  unseal; splitn x Hnx /= Hng.
  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
  eapply uPred_mono; eauto using ucmra_unit_leastN.
Qed.

Own
Lemma ownM_op (a1 a2 : M) :
  uPred_ownM (a1 a2) ⊣⊢ uPred_ownM a1 uPred_ownM a2.
Proof.
  unseal; splitn x ?; split.
  - intros [z ?]; a1, (a2 z); split; [by rewrite (assoc op)|].
    split. by (core a1); rewrite cmra_core_r. by z.
  - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); (z1 z2).
    by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
      -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
Lemma persistently_ownM_core (a : M) : uPred_ownM a uPred_ownM (core a).
Proof.
  splitn x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
Qed.
Lemma ownM_unit P : P (uPred_ownM ε).
Proof. unseal; splitn x ??; by x; rewrite left_id. Qed.
Lemma later_ownM a : uPred_ownM a b, uPred_ownM b (a b).
Proof.
  unseal; split⇒ -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
  destruct Hax as [y ?].
  destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
   a'. rewrite Hx. eauto using cmra_includedN_l.
Qed.

Lemma bupd_ownM_updateP x (Φ : M Prop) :
  x ~~>: Φ uPred_ownM x |==> y, Φ y uPred_ownM y.
Proof.
  unsealHup; splitn x2 ? [x3 Hx] k yf ??.
  destruct (Hup k (Some (x3 yf))) as (y&?&?); simpl in ×.
  { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
   (y x3); split; first by rewrite -assoc.
   y; eauto using cmra_includedN_l.
Qed.

Valid
Lemma ownM_valid (a : M) : uPred_ownM a a.
Proof.
  unseal; splitn x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
Qed.
Lemma cmra_valid_intro {A : cmraT} P (a : A) : a P ( a).
Proof. unseal⇒ ?; splitn x ? _ /=; by apply cmra_valid_validN. Qed.
Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a a False.
Proof. unsealHa; splitn x ??; apply Ha, cmra_validN_le with n; auto. Qed.
Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : a a.
Proof. by unseal. Qed.
Lemma cmra_valid_weaken {A : cmraT} (a b : A) : (a b) a.
Proof. unseal; splitn x _; apply cmra_validN_op_l. Qed.

Lemma prod_validI {A B : cmraT} (x : A × B) : x ⊣⊢ x.1 x.2.
Proof. by unseal. Qed.
Lemma option_validI {A : cmraT} (mx : option A) :
   mx ⊣⊢ match mx with Some x x | NoneTrue : uPred M end.
Proof. unseal. by destruct mx. Qed.

Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : a ⊣⊢ a.
Proof. unseal; splitn x _. by rewrite /= -cmra_discrete_valid_iff. Qed.

Lemma discrete_fun_validI {A} {B : A ucmraT} (g : discrete_fun B) : g ⊣⊢ i, g i.
Proof. by unseal. Qed.

Consistency/soundness statement The lemmas pure_soundness and internal_eq_soundness should become an instance of siProp soundness in the future.
Lemma pure_soundness φ : (True φ ) φ.
Proof. unseal⇒ -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.

Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True x y) x y.
Proof.
  unseal⇒ -[H]. apply equiv_distn.
  by apply (H n ε); eauto using ucmra_unit_validN.
Qed.

Lemma later_soundness P : (True P) (True P).
Proof.
  unseal⇒ -[HP]; splitn x Hx _.
  apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
  by apply (HP (S n)); eauto using ucmra_unit_validN.
Qed.
End primitive.
End uPred_primitive.