(* iris/base_logic/upred.v *)
From iris.algebra Require Export cmra updates
From iris.algebra Require Export stepindex_finite
From iris.bi Require Import notation
From iris.si_logic Require Import siprop
From iris.prelude Require Import options

Local HintExtern 1 (_ ≼ _) => etrans; [eassumption|] : core.

Local HintExtern 1 (_ ≼ _) => etrans; [|eassumption] : core.

Local HintExtern 10 (_ ≤ _) => lia : core.

Record uPred(M : ucmra) : Type := UPred {
  uPred_holds : nat → M → Prop;
  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.

Local CoercionuPred_holds : uPred >-> Funclass.
Bind Scope bi_scope with uPred.

Global ArgumentsuPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred.

Global Instance: Params (@uPred_holds) 3 := {}.

Inductive uPred_equiv'(P Q : uPred M) : Prop :=
    { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.

Local InstanceuPred_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 }.

Local InstanceuPred_dist : Dist (uPred M) := uPred_dist'.

Definition uPred_ofe_mixin: OfeMixin (uPred M).
  Proof.
    apply ofe_mixin_finite.
    - intros P Q; split.
      + by intros HPQ n; split=> i x ??; apply HPQ.
      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
    - intros n; split.
      + by intros P; split=> x i.
      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; split=> i x ??.
        by trans (Q i x);[apply HP|apply HQ].
    - intros n P Q HPQ. split=> i x ??; apply HPQ; eauto with lia.
  Qed.
  Canonical Structure uPredO : ofe := Ofe (uPred M) uPred_ofe_mixin.

Program DefinitionuPred_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 ProgramInstance uPred_cofe : Cofe uPredO := cofe_finite uPred_compl _.
  Next Obligation.
    intros n c; split=>i x Hin Hv.
    etrans; [|by symmetry; apply (chain_cauchy c i n)].
    split=>H; [by apply H|].
    repeat intro. apply (chain_cauchy c _ i)=>//. by eapply uPred_mono.
  Qed.

Global ArgumentsuPredO : clear implicits.

Global InstanceuPred_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.

Global InstanceuPred_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 : ucmra} (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.

Program DefinitionuPred_map {M1 M2 : ucmra} (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.

Global InstanceuPred_map_ne {M1 M2 : ucmra} (f : M2 -n> M1)
  `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
  intros x1 x2 Hx; split=> n' y ??.
  split; apply Hx; auto using cmra_morphism_validN.
Qed.

Lemma uPred_map_id{M : ucmra} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split=> n x ?. Qed.

Lemma uPred_map_compose{M1 M2 M3 : ucmra} (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 split=> n x Hx. Qed.

Lemma uPred_map_ext{M1 M2 : ucmra} (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; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.

Definition uPredO_map{M1 M2 : ucmra} (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 : ucmra} (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; split=> n' y ??;
  rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)).
Qed.

Program DefinitionuPredOF (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_map_ne; split; by apply HPQ.
Qed.
Next Obligation.
  intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
  apply uPred_map_ext=>y. by rewrite urFunctor_map_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_ext=>y; apply urFunctor_map_compose.
Qed.

Global InstanceuPredOF_contractive F :
  urFunctorContractive F → oFunctorContractive (uPredOF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
  apply uPredO_map_ne, urFunctor_map_contractive.
  destruct HPQ as [HPQ]; split; intros ??; split; simpl; by eapply HPQ.
Qed.

Inductive uPred_entails{M} (P Q : uPred M) : Prop :=
  { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.

Global HintResolve uPred_mono : uPred_def.

Local ProgramDefinition uPred_si_pure_def {M} (Pi : siProp) : uPred M :=
  {| uPred_holds n x := siProp_holds Pi n |}.
Solve Obligations with naive_solver eauto using siProp_closed.

Local DefinitionuPred_si_pure_aux : seal (@uPred_si_pure_def).
Proof. by eexists. Qed.

Definition uPred_si_pure:= uPred_si_pure_aux.(unseal).

Global ArgumentsuPred_si_pure {M}.

Local DefinitionuPred_si_pure_unseal :
  @uPred_si_pure = @uPred_si_pure_def := uPred_si_pure_aux.(seal_eq).

Local ProgramDefinition uPred_si_emp_valid_def {M} (P : uPred M) : siProp :=
  {| siProp_holds n := P n ε |}.
Solve Obligations with naive_solver eauto with uPred_def.

Local DefinitionuPred_si_emp_valid_aux : seal (@uPred_si_emp_valid_def).
Proof. by eexists. Qed.

Definition uPred_si_emp_valid:= uPred_si_emp_valid_aux.(unseal).

Global ArgumentsuPred_si_emp_valid {M}.

Local DefinitionuPred_si_emp_valid_unseal :
  @uPred_si_emp_valid = @uPred_si_emp_valid_def := uPred_si_emp_valid_aux.(seal_eq).

Local ProgramDefinition 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.

Local DefinitionuPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.

Definition uPred_and:= uPred_and_aux.(unseal).

Global ArgumentsuPred_and {M}.

Local DefinitionuPred_and_unseal :
  @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).

Local ProgramDefinition 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.

Local DefinitionuPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.

Definition uPred_or:= uPred_or_aux.(unseal).

Global ArgumentsuPred_or {M}.

Local DefinitionuPred_or_unseal :
  @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).

Local ProgramDefinition 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. exists (x2 ⋅ x4); by rewrite assoc.
Qed.

Local DefinitionuPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.

Definition uPred_impl:= uPred_impl_aux.(unseal).

Global ArgumentsuPred_impl {M}.

Local DefinitionuPred_impl_unseal :
  @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).

Local ProgramDefinition 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.

Local DefinitionuPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.

Definition uPred_forall:= uPred_forall_aux.(unseal).

Global ArgumentsuPred_forall {M A}.

Local DefinitionuPred_forall_unseal :
  @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).

Local ProgramDefinition 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.

Local DefinitionuPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.

Definition uPred_exist:= uPred_exist_aux.(unseal).

Global ArgumentsuPred_exist {M A}.

Local DefinitionuPred_exist_unseal :
  @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).

Local ProgramDefinition 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.
  exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_includedN_l.
  rewrite Hy. eapply dist_le, Hn. by rewrite Hx assoc.
Qed.

Local DefinitionuPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.

Definition uPred_sep:= uPred_sep_aux.(unseal).

Global ArgumentsuPred_sep {M}.

Local DefinitionuPred_sep_unseal :
  @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).

Local ProgramDefinition 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.

Local DefinitionuPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.

Definition uPred_wand:= uPred_wand_aux.(unseal).

Global ArgumentsuPred_wand {M}.

Local DefinitionuPred_wand_unseal :
  @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).

Local ProgramDefinition uPred_persistently_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (core x) |}.
Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.

Local DefinitionuPred_persistently_aux : seal (@uPred_persistently_def).
Proof. by eexists. Qed.

Definition uPred_persistently:= uPred_persistently_aux.(unseal).

Global ArgumentsuPred_persistently {M}.

Local DefinitionuPred_persistently_unseal :
  @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).

Local ProgramDefinition 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.

Local DefinitionuPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.

Definition uPred_later:= uPred_later_aux.(unseal).

Global ArgumentsuPred_later {M}.

Local DefinitionuPred_later_unseal :
  @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).

Local ProgramDefinition uPred_ownM_def {M : ucmra} (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.
  exists (a' ⋅ x2). rewrite Hx. eapply dist_le, Hn. rewrite (assoc op) -Hx1 //.
Qed.

Local DefinitionuPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.

Definition uPred_ownM:= uPred_ownM_aux.(unseal).

Global ArgumentsuPred_ownM {M}.

Local DefinitionuPred_ownM_unseal :
  @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).

Local ProgramDefinition 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 Hk). intros Hxy.
  destruct (HQ k (x3 ⋅ yf)) as (x'&?&?); [auto|by rewrite assoc|].
  exists (x' ⋅ x3); split; first by rewrite -assoc.
  eauto using uPred_mono, cmra_includedN_l.
Qed.

Local DefinitionuPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.

Definition uPred_bupd:= uPred_bupd_aux.(unseal).

Global ArgumentsuPred_bupd {M}.

Local DefinitionuPred_bupd_unseal :
  @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).

Local DefinitionuPred_unseal :=
  (uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
  uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
  uPred_forall_unseal, uPred_exist_unseal,
  uPred_sep_unseal, uPred_wand_unseal,
  uPred_persistently_unseal, uPred_later_unseal, uPred_ownM_unseal,
  @uPred_bupd_unseal).

Ltac unseal:=
  rewrite !uPred_unseal /=.

Local ArgumentsuPred_holds {_} !_ _ _ /.

Local ArgumentssiProp_holds !_ _ /.

Local HintImmediate uPred_in_entails : core.

Lemma entails_po: PreOrder (⊢).
  Proof.
    split.
    - by intros P; split=> x i.
    - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
  Qed.

Lemma entails_anti_sym: AntiSymm (⊣⊢) (⊢).
  Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.

Lemma equiv_entailsP Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
  Proof.
    split.
    - intros HPQ; split; split=> x 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; split=> n m ? HP.
    eapply uPred_holds_ne, Hlim; [..|apply: HP]; rewrite ?conv_compl; eauto.
  Qed.

Lemma si_pure_ne: NonExpansive (@uPred_si_pure M).
  Proof. intros n Pi Pi' HPi. unseal; split; intros; by apply HPi. Qed.

Lemma si_emp_valid_ne: NonExpansive (@uPred_si_emp_valid M).
  Proof.
    intros n P P' HP.
    unseal; split; intros; apply HP; auto using ucmra_unit_validN.
  Qed.

Lemma and_ne: NonExpansive2 (@uPred_and M).
  Proof.
    intros n P P' HP Q Q' HQ; unseal; split=> x 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; split=> x 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; split=> x 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; split=> n' x ??.
    unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
      exists 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; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
      apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
  Qed.

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

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

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

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

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

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

Lemma si_pure_monoPi Qi : siProp_entails Pi Qi → <si_pure> Pi ⊢ <si_pure> Qi.
  Proof. intros HPQi. unseal; split=> n ??. apply HPQi. Qed.

Lemma si_emp_valid_monoP Q :
    (P ⊢ Q) → siProp_entails (<si_emp_valid> P) (<si_emp_valid> Q).
  Proof. intros HPQ. unseal; split=> n. apply HPQ, ucmra_unit_validN. Qed.

Lemma si_pure_impl_2Pi Qi :
    (<si_pure> Pi → <si_pure> Qi) ⊢ <si_pure> siProp_impl Pi Qi.
  Proof.
    unseal; siProp_primitive.unseal. split; simpl; eauto using cmra_validN_le.
  Qed.

Lemma si_pure_forall_2{A} (Φi : A → siProp) :
   (∀ x, <si_pure> Φi x) ⊢ <si_pure> siProp_forall Φi.
  Proof. by unseal; siProp_primitive.unseal. Qed.

Lemma si_pure_laterPi : <si_pure> siProp_later Pi ⊣⊢ ▷ <si_pure> Pi.
  Proof. by unseal; siProp_primitive.unseal. Qed.

Lemma si_emp_valid_later_1P :
    siProp_entails (<si_emp_valid> ▷ P) (siProp_later (<si_emp_valid> P)).
  Proof. by unseal; siProp_primitive.unseal. Qed.

Lemma si_emp_valid_exist_1{A} (Φ : A → uPred M) :
    siProp_entails (<si_emp_valid> ∃ x, Φ x)
                   (siProp_exist (λ x, <si_emp_valid> Φ x)).
  Proof. by unseal; siProp_primitive.unseal. Qed.

Lemma si_emp_valid_si_purePi :
    <si_emp_valid> (<si_pure> Pi : uPred M)%I ≡ Pi.
  Proof. by unseal. Qed.

Lemma si_pure_si_emp_validP :
    <si_pure> <si_emp_valid> P ⊢ □ P.
  Proof.
    unseal. split=> /= n x _ ?.
    eapply uPred_mono with n ε; eauto using ucmra_unit_leastN.
  Qed.

Lemma persistently_impl_si_purePi Q :
    (<si_pure> Pi → □ Q) ⊢ □ (<si_pure> Pi → 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 prop_ext_2P Q :
    siProp_entails (<si_emp_valid> ((P -∗ Q) ∧ (Q -∗ P)))
                   (siProp_internal_eq P Q).
  Proof.
    unseal; siProp_primitive.unseal.
    split=> n /=. setoid_rewrite (left_id ε op). split; naive_solver.
  Qed.

Lemma and_elim_lP Q : P ∧ Q ⊢ P.
  Proof. by unseal; split=> n x ? [??]. Qed.

Lemma and_elim_rP Q : P ∧ Q ⊢ Q.
  Proof. by unseal; split=> n x ? [??]. Qed.

Lemma and_introP Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
  Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.

Lemma or_intro_lP Q : P ⊢ P ∨ Q.
  Proof. unseal; split=> n x ??; left; auto. Qed.

Lemma or_intro_rP Q : Q ⊢ P ∨ Q.
  Proof. unseal; split=> n x ??; right; auto. Qed.

Lemma or_elimP Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
  Proof.
    intros HP HQ; unseal; split=> n x ? [?|?].
    - by apply HP.
    - by apply HQ.
  Qed.

Lemma impl_intro_rP Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
  Proof.
    unseal; intros HQ; split=> n 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 ; split=> n 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Ψ; split=> n x ?? a; by apply HPΨ. Qed.

Lemma forall_elim{A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
  Proof. unseal; split=> n x ? HP; apply HP. Qed.

Lemma exist_intro{A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
  Proof. unseal; split=> n x ??; by exists a. Qed.

Lemma exist_elim{A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
  Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.

Lemma sep_monoP P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
  Proof.
    intros HQ HQ'; unseal.
    split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
      eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
  Qed.

Lemma True_sep_1P : P ⊢ True ∗ P.
  Proof.
    unseal; siProp_primitive.unseal; split; intros n x ??.
    exists (core x), x. by rewrite cmra_core_l.
  Qed.

Lemma True_sep_2P : 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&?&?&?); exists 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&?&?)&?).
    exists y1, (y2 ⋅ x2); split_and?; auto.
    + by rewrite (assoc op) -Hy -Hx.
    + by exists y2, x2.
  Qed.

Lemma wand_intro_rP Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
  Proof.
    unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
    exists 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.
    unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
    eapply HPQR; eauto using cmra_validN_op_l.
  Qed.

Lemma persistently_monoP Q : (P ⊢ Q) → □ P ⊢ □ Q.
  Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.

Lemma persistently_elimP : □ P ⊢ P.
  Proof.
    unseal; split=> n x ? /=.
    eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
  Qed.

Lemma persistently_idemp_2P : □ P ⊢ □ □ P.
  Proof. unseal; split=> n 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_1P Q : □ P ∧ Q ⊢ P ∗ Q.
  Proof.
    unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
    by rewrite cmra_core_l.
  Qed.

Lemma later_monoP Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
  Proof.
    unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
  Qed.

Lemma later_introP : 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_1P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
  Proof.
    unseal; split=> n x ?.
    destruct n as [|n]; simpl.
    { by exists 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 *.
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
  Qed.

Lemma later_sep_2P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
  Proof.
    unseal; split=> n x ?.
    destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
    exists x1, x2; eauto using dist_S.
  Qed.

Lemma later_false_emP : ▷ P ⊢ ▷ False ∨ (▷ False → P).
  Proof.
    unseal; siProp_primitive.unseal; split=> -[|n] x ? /= HP; [by left|right].
    intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
  Qed.

Lemma later_persistently_1P : ▷ □ P ⊢ □ ▷ P.
  Proof. by unseal. Qed.

Lemma later_persistently_2P : □ ▷ P ⊢ ▷ □ P.
  Proof. by unseal. Qed.

Lemma bupd_introP : P ⊢ |==> P.
  Proof.
    unseal. split=> n x ? HP k yf ?; exists x; split; first done.
    apply uPred_mono with n x; eauto using cmra_validN_op_l.
  Qed.

Lemma bupd_monoP Q : (P ⊢ Q) → (|==> P) ⊢ |==> Q.
  Proof.
    unseal. intros HPQ; split=> n x ? HP k yf ??.
    destruct (HP k yf) as (x'&?&?); eauto.
    exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
  Qed.

Lemma bupd_transP : (|==> |==> P) ⊢ |==> P.
  Proof. unseal; split; naive_solver. Qed.

Lemma bupd_frame_rP 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). }
    exists (x' ⋅ x2); split; first by rewrite -assoc.
    exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
  Qed.

Lemma bupd_si_purePi : (|==> <si_pure> Pi) ⊢ <si_pure> Pi.
  Proof.
    unseal; split => n x Hnx /= Hng.
    destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
  Qed.

Lemma ownM_op(a1 a2 : M) :
    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
  Proof.
    unseal; split=> n x ?; split.
    - intros [z ?]; exists a1, (a2 ⋅ z); split; [by rewrite (assoc op)|].
      split.
      + by exists (core a1); rewrite cmra_core_r.
      + by exists z.
    - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (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.
    split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
  Qed.

Lemma ownM_unitP : P ⊢ (uPred_ownM ε).
  Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.

Lemma later_ownMa :
    ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ <si_pure> siProp_internal_eq a b.
  Proof.
    unseal; siProp_primitive.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.
    exists a'. rewrite Hx. eauto using cmra_includedN_l.
  Qed.

Lemma bupd_ownM_updatePx (Φ : M → Prop) :
    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
  Proof.
    unseal; siProp_primitive.unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
    destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *.
    { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
    exists (y ⋅ x3); split; first by rewrite -assoc.
    exists y; eauto using cmra_includedN_l.
  Qed.

Lemma ownM_forall{A} (f : A → M) :
    (∀ a, uPred_ownM (f a)) ⊢ ∃ z, uPred_ownM z ∧
      (∀ a, ∃ xf, <si_pure> siProp_internal_eq z (f a ⋅ xf)).
  Proof.
    unseal; siProp_primitive.unseal.
    split=> n y /= Hval Hf. exists y. split; [done|]. intros a.
    destruct (Hf a) as [xf ?]; eauto.
  Qed.

Lemma ownM_valid(a : M) : uPred_ownM a ⊢ <si_pure> siProp_cmra_valid a.
  Proof.
    unseal; siProp_primitive.unseal.
    split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
  Qed.