Library iris.algebra.upred

From iris.algebra Require Export cmra.
Local Hint Extern 1 (_ ≼ _) ⇒ etrans; [eassumption|].
Local Hint Extern 1 (_ ≼ _) ⇒ etrans; [|eassumption].
Local Hint Extern 10 (_ ≤ _) ⇒ omega.

Record uPred (M : ucmraT) : Type := IProp {
  uPred_holds :> nat → M → M → Prop;
  uPred_mono n x1 y1 x2 y2:
    uPred_holds n x1 y1 → x1 ≼{n} x2 → y1 ≡{n}≡ y2 → uPred_holds n x2 y2;
  uPred_closed n1 n2 x y :
    uPred_holds n1 x y → n2 ≤ n1 → ✓{n2} x → ✓{n2} y → uPred_holds n2 x y
}.
Arguments uPred_holds {_} _ _ _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.

Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _ _.

Section cofe.
  Context {M : ucmraT}.

  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
    { uPred_in_equiv : ∀ n x y, ✓{n} x → ✓{n} y → P n x y ↔ Q n x y }.
  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
    { uPred_in_dist : ∀ n' x y, n' ≤ n → ✓{n'} x → ✓{n'} y → P n' x y ↔ Q n' x y}.
  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
  Program Instance uPred_compl : Compl (uPred M) := λ c,
    {| uPred_holds n x y := c n n x y |}.
  Next Obligation. naive_solver eauto using uPred_mono. Qed.
  Next Obligation.
    intros c n1 n2 x y ????; simpl in ×.
    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
    - 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 y ???.
        by trans (Q i x y);[apply HP|apply HQ].
    - intros n P Q HPQ; split⇒ i x ??; apply HPQ; auto.
    - intros n c; split⇒i x ??; symmetry; apply (chain_cauchy c i n); auto.
  Qed.
  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> dist n ==> iff) (P n).
Proof. intros x1 x2 Hx y1 y2 Hy; 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 y1 y2 Hy; apply uPred_ne; apply equiv_dist. Qed.

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

Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x y := P n (f x) (f y)|}.
Next Obligation.
  intros M1 M2 f ? P n y1 y2 x1 x2 ? Hx Hy. rewrite /=.
  rewrite -Hy. naive_solver eauto using uPred_mono, cmra_monotoneN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.

Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
  intros x1 x2 Hx; split⇒ n' y ??.
  split; apply Hx; auto using validN_preserving.
Qed.
Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split⇒ n x ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
    `{!CMRAMonotone f, !CMRAMonotone 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 : ucmraT} (f g : M1 -n> M2)
      `{!CMRAMonotone f} `{!CMRAMonotone g}:
  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split⇒ n x y Hx Hy /=; by rewrite /uPred_holds /= ?Hf. Qed.
Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
    `{!CMRAMonotone f, !CMRAMonotone g} n :
  f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
Proof.
  by intros Hfg P; split⇒ n' x y ???;
    rewrite /uPred_holds /= ?(dist_le _ _ _ _(Hfg x)) //= ?(dist_le _ _ _ _(Hfg y)); last lia.
Qed.

Program Definition uPredCF (F : urFunctor) : cFunctor := {|
  cFunctor_car A B := uPredC (urFunctor_car F B A);
  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
  intros F A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_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_ext⇒y. 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_ext⇒y; apply urFunctor_compose.
Qed.

Instance uPredCF_contractive F :
  urFunctorContractive F → cFunctorContractive (uPredCF F).
Proof.
  intros ? A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_map_ne, urFunctor_contractive⇒ i ?; split; by apply HPQ.
Qed.

Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails : ∀ n x y, ✓{n} x → ✓{n} y → P n x y → Q n x y}.
Hint Extern 0 (uPred_entails _ _) ⇒ reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).

Hint Resolve uPred_mono uPred_closed : uPred_def.

Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
  {| uPred_holds n x y := φ|}.
Solve Obligations with (intros; cofe_subst; done).

Definition uPred_pure_aux : { x | x = @uPred_pure_def}. by eexists. Qed.
Definition uPred_pure {M} := proj1_sig uPred_pure_aux M.
Definition uPred_pure_eq :
  @uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux.

Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True).

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

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

Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x y := ∀ n' x',
       x ≼ x' → n' ≤ n → ✓{n'} x' → ✓{n'} y → P n' x' y → Q n' x' y |}.
Next Obligation.
  intros M P Q n1 x1 x1' y1 y1' HPQ [x2 Hx1'] Hx2' n2 x3 [x4 Hx3] ?; simpl in ×.
  rewrite Hx3 (dist_le _ _ _ _ Hx1') // -(dist_le _ _ _ _ Hx2'); auto. intros ???.
  eapply HPQ; auto. ∃ (x2 ⋅ x4); by rewrite assoc.
Qed.
Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
Definition uPred_impl_eq :
  @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.

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

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

Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
  {| uPred_holds n x y := a1 ≡{n}≡ a2|}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.

Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x y := ∃ x1 x2 y1 y2, x ≡{n}≡ x1 ⋅ x2 ∧ y ≡{n}≡ y1 ⋅ y2
                                       ∧ P n x1 y1 ∧ Q n x2 y2 |}.
Next Obligation.
  intros M P Q n x1 y1 x2 y2 (x1'&x2'&y1'&y2'&Hx&Hy&?&?) [z Hz] ?.
  ∃ x1', (x2' ⋅ z), y1', y2'.
  split_and?; eauto using uPred_mono, cmra_includedN_l.
  - by rewrite Hz Hx assoc.
  - by rewrite -Hy.
Qed.
Next Obligation.
  intros M P Q n1 n2 x y (x1&x2&y1&y2&Hx&Hy&?&?) Hlt.
  rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
  rewrite {1}(dist_le _ _ _ _ Hy) // =>?.
  ∃ x1, x2, y1, y2; cofe_subst; split_and!;
  eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
Qed.
Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.

Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x y := ∀ n' x' y',
       n' ≤ n → ✓{n'} (x ⋅ x') → ✓{n'} (y ⋅ y') → P n' x' y' → Q n' (x ⋅ x') (y ⋅ y') |}.
Next Obligation.
  intros M P Q n1 x1 y1 x2 y2 HPQ Hx Hy n2 x3 y3 ????; simpl in ×.
  rewrite -(dist_le _ _ _ _ Hy) //.
  apply uPred_mono with (x1 ⋅ x3) (y1 ⋅ y3); first apply HPQ;
    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
  by rewrite (dist_le _ _ _ _ Hy).
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
Definition uPred_wand_eq :
  @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.

Program Definition uPred_relevant_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x y:= P n (core x) (core y) ∧ y ≡{n}≡ core y |}.
Next Obligation.
  intros M P n x1 x2 y1 y2 (?&?) Hx Hy. rewrite -Hy.
  naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation.
  intros M P n1 n2 x y (?&Hc) ???.
  naive_solver eauto using uPred_closed, @cmra_core_mono, @cmra_core_validN, dist_le.
Qed.
Definition uPred_relevant_aux : { x | x = @uPred_relevant_def }. by eexists. Qed.
Definition uPred_relevant {M} := proj1_sig uPred_relevant_aux M.
Definition uPred_relevant_eq :
  @uPred_relevant = @uPred_relevant_def := proj2_sig uPred_relevant_aux.

Program Definition uPred_affine_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x y:= P n x y ∧ y ≡{n}≡ ∅ |}.
Next Obligation.
  intros M P n x1 y1 x2 y2 (?&Hempty) Hx Hy.
  rewrite -Hy. naive_solver eauto 2 with uPred_def.
Qed.
Next Obligation.
  intros M P n1 n2 x y (?&?) ???. naive_solver eauto 2 using uPred_closed, dist_le.
Qed.
Definition uPred_affine_aux : { x | x = @uPred_affine_def }. by eexists. Qed.
Definition uPred_affine {M} := proj1_sig uPred_affine_aux M.
Definition uPred_affine_eq :
  @uPred_affine = @uPred_affine_def := proj2_sig uPred_affine_aux.

Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x y := match n return _ with 0 ⇒ True | S n' ⇒ P n' x y end |}.
Next Obligation.
  intros M P [|n] ??; eauto using uPred_mono, cmra_includedN_S,(dist_le (A:=M)).
Qed.
Next Obligation.
  intros M P [|n1] [|n2] x1 x2 y1 y2; eauto using uPred_closed,cmra_validN_S; try lia.
Qed.
Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
Definition uPred_later {M} := proj1_sig uPred_later_aux M.
Definition uPred_later_eq :
  @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.

Program Definition uPred_ownM_def {M: ucmraT} (a : M) : uPred M :=
  {| uPred_holds n x y := a ≼{n} x|}.
Next Obligation.
  intros M a n x1 y1 x2 y2 [a' Hx1] [x2' ->] Hy;
    ∃ (a' ⋅ x2'). by rewrite (assoc op) Hx1.
Qed.
Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
Definition uPred_ownM_eq :
  @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.

Program Definition uPred_ownMl_def {M: ucmraT} (a : M) : uPred M :=
  {| uPred_holds n x y := a ≡{n}≡ y|}.
Next Obligation.
  intros M a n x1 y1 x2 y2 Hequiv Hx Hy.
  rewrite Hequiv //=.
Qed.
Next Obligation.
  intros M a n1 n2 x1 x2 Hequiv Hle ?.
  rewrite -(dist_le _ _ _ _ Hequiv) //=.
Qed.
Definition uPred_ownMl_aux : { x | x = @uPred_ownMl_def }. by eexists. Qed.
Definition uPred_ownMl {M} := proj1_sig uPred_ownMl_aux M.
Definition uPred_ownMl_eq :
  @uPred_ownMl = @uPred_ownMl_def := proj2_sig uPred_ownMl_aux.

Program Definition uPred_valid_def {M : ucmraT} {A : cmraT} (a : A) : uPred M :=
  {| uPred_holds n x y := ✓{n} a|}.
Solve Obligations with (intros; cofe_subst; naive_solver eauto 2 using cmra_validN_le, dist_le).
Definition uPred_valid_aux : { x | x = @uPred_valid_def }. by eexists. Qed.
Definition uPred_valid {M A} := proj1_sig uPred_valid_aux M A.
Definition uPred_valid_eq :
  @uPred_valid = @uPred_valid_def := proj2_sig uPred_valid_aux.

Program Definition uPred_stopped_def {M: ucmraT} : uPred M :=
  {| uPred_holds n x y := ∀ n', n' ≤ n → nf (stepN n') y|}.
Next Obligation.
  rewrite /nf /red; intros M n x1 x2 y1 y2 Hns Heq1 Heq2; simpl.
  intros n' Hle (y&Hs').
  eapply Hns; eauto. ∃ y. by rewrite (dist_le _ _ _ _ Heq2).
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_stopped_aux : { x | x = @uPred_stopped_def }. by eexists. Qed.
Definition uPred_stopped {M} := proj1_sig uPred_stopped_aux M.
Definition uPred_stopped_eq :
  @uPred_stopped = @uPred_stopped_def := proj2_sig uPred_stopped_aux.

Program Definition uPred_emp_def {M: ucmraT} : uPred M :=
  {| uPred_holds n x y := y ≡{n}≡ ∅ |}.
Solve Obligations with (intros; cofe_subst; naive_solver eauto 2 using cmra_validN_le, dist_le).
Definition uPred_emp_aux : { x | x = @uPred_emp_def }. by eexists. Qed.
Definition uPred_emp {M} := proj1_sig uPred_emp_aux M.
Definition uPred_emp_eq :
  @uPred_emp = @uPred_emp_def := proj2_sig uPred_emp_aux.

Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
  (at level 99, Q at level 200, right associativity) : C_scope.
Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
  (at level 95, no associativity) : C_scope.
Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
Notation "■ φ" := (uPred_pure φ%C%type)
  (at level 20, right associativity) : uPred_scope.
Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
Notation "x ⊥ y" := (uPred_pure (x%C%type ⊥ y%C%type)) : uPred_scope.
Notation "'False'" := (uPred_pure False) : uPred_scope.
Notation "'True'" := (uPred_pure True) : uPred_scope.
Notation "'Emp'" := (uPred_emp) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Infix "∨" := uPred_or : uPred_scope.
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
Notation "P -★ Q" := (uPred_wand P Q)
  (at level 99, Q at level 200, right associativity) : uPred_scope.
Notation "∀ x .. y , P" :=
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Notation "∃ x .. y , P" :=
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
Notation "□ P" := (uPred_relevant P)
  (at level 20, right associativity) : uPred_scope.
Notation "⧆ P" := (uPred_affine P)
  (at level 20, right associativity) : uPred_scope.
Notation "⧈ P" := (uPred_affine (uPred_relevant P))
  (at level 20, right associativity) : uPred_scope.
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Infix "≡" := (uPred_eq) : uPred_scope.
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.

Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
Instance: Params (@uPred_iff) 1.
Infix "↔" := uPred_iff : uPred_scope.

Definition uPred_relevant_if {M} (p : bool) (P : uPred M) : uPred M :=
  (if p then □ P else P)%I.
Instance: Params (@uPred_relevant_if) 2.
Arguments uPred_relevant_if _ !_ _/.
Notation "□? p P" := (uPred_relevant_if p P)
  (at level 20, p at level 0, P at level 20, format "□? p P").

Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
  Nat.iter n uPred_later P.
Instance: Params (@uPred_laterN) 2.
Notation "▷^ n P" := (uPred_laterN n P)
  (at level 20, n at level 9, right associativity,
   format "▷^ n P") : uPred_scope.

Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
Arguments timelessP {_} _ {_}.

Class ATimelessP {M: ucmraT} (P : uPred M)
  := atimelessP : ⧆▷ P ⊢ (⧆P ∨ ▷ False).
Arguments atimelessP {_} _ {_}.

Class RelevantP {M: ucmraT} (P : uPred M) := relevantP : P ⊢ □ P.
Arguments relevantP {_} _ {_}.

Class AffineP {M: ucmraT} (P : uPred M) := affineP : P ⊢ ⧆ P.
Arguments affineP {_} _ {_}.

Class UnlimitedP {M} (P : uPred M) := {
  unlimited_relevant :> RelevantP P;
  unlimited_affine :> AffineP P
}.

Module uPred.
Definition unseal :=
  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_relevant_eq, uPred_affine_eq,
  uPred_later_eq, uPred_ownM_eq, uPred_ownMl_eq, uPred_valid_eq, uPred_emp_eq, uPred_stopped_eq).
Ltac unseal := rewrite !unseal /=.

Section uPred_logic.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). Arguments uPred_holds {_} !_ _ _ _ /.
Hint Immediate uPred_in_entails.

Global Instance: PreOrder (@uPred_entails M).
Proof.
  split.
  × by intros P; split⇒ x i.
  × by intros P Q Q' HP HQ; split⇒ x y i ???; apply HQ, HP.
Qed.
Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
Proof. intros P Q HPQ HQP; split⇒ x n; by split; [apply HPQ|apply HQP]. Qed.
Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
Proof.
  split; [|by intros [??]; apply (anti_symm (⊢))].
  intros HPQ; split; split⇒ x i; apply HPQ.
Qed.
Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
Proof. apply equiv_spec. Qed.
Global Instance entails_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation (uPred M)).
Proof.
  move ⇒ P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Qed.
Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
Proof. by intros →. Qed.
Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
Proof. by intros ? <-. Qed.

Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M).
Proof. intros φ1 φ2 Hφ. by unseal; split⇒ -[|n] ?; try apply Hφ. Qed.
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Proof.
  intros P P' HP Q Q' HQ; unseal; split⇒ x n' ????.
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.
Global Instance and_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_and M) := ne_proper_2 _.
Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Proof.
  intros P P' HP Q Q' HQ; split⇒ x n' ??.
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.
Global Instance or_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_or M) := ne_proper_2 _.
Global Instance impl_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Proof.
  intros P P' HP Q Q' HQ; split⇒ n' x y ???;
  by unseal; split; intros HPQ; intros n'' x' ?????;
  apply HQ, HPQ, HP; auto.
Qed.
Global Instance impl_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_impl M) := ne_proper_2 _.
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Proof.
  intros P P' HP Q Q' HQ; split⇒ n' x y ???.
  unseal; split; intros (x1&x2&y1&y2&?&?&?&?); cofe_subst x; cofe_subst y;
    ∃ x1, x2, y1, y2; split_and!; try (apply HP || apply HQ);
    eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Global Instance sep_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_sep M) := ne_proper_2 _.
Global Instance wand_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Proof.
  intros P P' HP Q Q' HQ; split⇒ n' x y ???; unseal; split; intros HPQ n'' x' y' ????;
    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
Global Instance wand_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_wand M) := ne_proper_2 _.
Global Instance eq_ne (A : cofeT) n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Proof.
  intros x x' Hx y y' Hy; split⇒ n' 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.
Global Instance eq_proper (A : cofeT) :
  Proper ((≡) ==> (≡) ==> (⊣⊢)) (@uPred_eq M A) := ne_proper_2 _.
Global Instance forall_ne A 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.
Global Instance forall_proper A :
  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_forall M A).
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split⇒ n' x; split; intros HP a; apply HΨ.
Qed.
Global Instance exist_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Proof.
  intros Ψ1 Ψ2 HΨ.
  unseal; split⇒ n' x ??; split; intros [a ?]; ∃ a; by apply HΨ.
Qed.
Global Instance exist_proper A :
  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_exist M A).
Proof.
  intros Ψ1 Ψ2 HΨ.
  unseal; split⇒ n' x ?; split; intros [a ?]; ∃ a; by apply HΨ.
Qed.
Global Instance later_contractive : Contractive (@uPred_later M).
Proof.
  intros n P Q HPQ; unseal; split⇒ -[|n'] x y ???; simpl; [done|].
  apply (HPQ n'); eauto using cmra_validN_S.
Qed.
Global Instance later_proper' :
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
Global Instance relevant_ne n : Proper (dist n ==> dist n) (@uPred_relevant M).
Proof.
  intros P1 P2 HP.
  unseal; split⇒ n' x y; split;
  (intros (?&?); split; first apply HP; eauto using @cmra_core_validN).
Qed.
Global Instance relevant_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_relevant M) := ne_proper _.
Global Instance affine_ne n : Proper (dist n ==> dist n) (@uPred_affine M).
Proof.
  intros P1 P2 HP.
  unseal; split⇒ n' x y ???.
  split; intros (?&?); split; auto; apply HP; eauto.
Qed.
Global Instance affine_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_affine M) := ne_proper _.
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
Proof.
  intros a b Ha.
  unseal; split⇒ n' x y ?? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
Global Instance ownMl_ne n : Proper (dist n ==> dist n) (@uPred_ownMl M).
Proof.
  intros a b Ha.
  unseal; split⇒ n' x y ?? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance ownMl_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownMl M) := ne_proper _.
Global Instance valid_ne {A : cmraT} n :
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
  intros a b Ha; unseal; split⇒ n' x y ?? /=.
  by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance valid_proper {A : cmraT} :
  Proper ((≡) ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _.

Lemma pure_intro φ P : φ → P ⊢ ■ φ.
Proof. by intros ?; unseal; split. Qed.
Lemma pure_elim φ Q R : (Q ⊢ ■ φ) → (φ → Q ⊢ R) → Q ⊢ R.
Proof.
  unseal; intros HQP HQR; split⇒ n x y ?? HQ; apply HQR; eauto.
  eapply HQP; last apply HQ; eauto.
Qed.
Lemma and_elim_l P Q : P ∧ Q ⊢ P.
Proof. by unseal; split⇒ n x y ?? [??]. Qed.
Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
Proof. by unseal; split⇒ n x y ?? [??]. Qed.
Lemma and_intro P 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_l P Q : P ⊢ P ∨ Q.
Proof. unseal; split⇒ n x y ???; left; auto. Qed.
Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
Proof. unseal; split⇒ n x y ???; right; auto. Qed.
Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
Proof. intros HP HQ; unseal; split⇒ n x y ?? [?|?]. by apply HP. by apply HQ. Qed.
Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
Proof.
  unseal; intros HQ; split⇒ n x y ??? n' x' ?????.
  apply HQ; try naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
Qed.
Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
Proof. by unseal; intros HP HP'; split⇒ n x y ???; apply HP with n x, HP'. Qed.
Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
Proof. unseal; intros HPΨ; split⇒ n x y ??? a; by apply HPΨ. Qed.
Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
Proof. unseal; split⇒ n x y ?? HP; apply HP. Qed.
Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
Proof. unseal; split⇒ n x y ???; by ∃ a. Qed.
Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
Proof. unseal; intros HΦΨ; split⇒ n x y ?? [a ?]; by apply HΦΨ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) : True ⊢ (a ≡ a).
Proof. unseal; split⇒ n x y ???; simpl. naive_solver. Qed.
Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
  {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
Proof.
  unseal; intros Hab Ha; split⇒ n x y ???.
  apply HΨ with n a; auto.
  - symmetry. unfold uPred_eq_def in Hab.
    eapply Hab; last eauto; auto.
  - eauto.
Qed.
Lemma eq_equiv {A : cofeT} (a b : A) : (True ⊢ a ≡ b) → a ≡ b.
Proof.
  unseal⇒ Hab; apply equiv_dist; intros n.
  apply Hab with ∅ ∅; last done;
  apply cmra_valid_validN, ucmra_unit_valid.
Qed.
Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P
  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
Proof.
  unseal; intros Hab Ha; split⇒ n x y ???. apply HΨ with n a; auto.
  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n) x y).
  - by apply Ha.
Qed.

Lemma affine_equiv P: ⧆P ⊣⊢ (P ∧ Emp).
Proof.
  unseal; apply (anti_symm (⊢)); split⇒ n x y ??; naive_solver.
Qed.

Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.

Lemma False_elim P : False ⊢ P.
Proof. by apply (pure_elim False). Qed.
Lemma True_intro P : P ⊢ True.
Proof. by apply pure_intro. Qed.
Lemma and_elim_l' P Q R : (P ⊢ R) → P ∧ Q ⊢ R.
Proof. by rewrite and_elim_l. Qed.
Lemma and_elim_r' P Q R : (Q ⊢ R) → P ∧ Q ⊢ R.
Proof. by rewrite and_elim_r. Qed.
Lemma or_intro_l' P Q R : (P ⊢ Q) → P ⊢ Q ∨ R.
Proof. intros ->; apply or_intro_l. Qed.
Lemma or_intro_r' P Q R : (P ⊢ R) → P ⊢ Q ∨ R.
Proof. intros ->; apply or_intro_r. Qed.
Lemma exist_intro' {A} P (Ψ : A → uPred M) a : (P ⊢ Ψ a) → P ⊢ ∃ a, Ψ a.
Proof. intros ->; apply exist_intro. Qed.
Lemma forall_elim' {A} P (Ψ : A → uPred M) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
Proof. move⇒ HP a. by rewrite HP forall_elim. Qed.

Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.

Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R.
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
Lemma impl_elim_l P Q : (P → Q) ∧ P ⊢ Q.
Proof. apply impl_elim with P; auto. Qed.
Lemma impl_elim_r P Q : P ∧ (P → Q) ⊢ Q.
Proof. apply impl_elim with P; auto. Qed.
Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
Proof. intros; apply impl_elim with Q; auto. Qed.
Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R.
Proof. intros; apply impl_elim with P; auto. Qed.
Lemma impl_entails P Q : (True ⊢ P → Q) → P ⊢ Q.
Proof. intros HPQ; apply impl_elim with (P)%I; auto. rewrite -HPQ; auto. Qed.
Lemma entails_impl P Q : (P ⊢ Q) → True ⊢ P → Q.
Proof. auto using impl_intro_l. Qed.

Lemma iff_refl Q P : Q ⊢ P ↔ P.
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
Lemma iff_equiv P Q : (True ⊢ P ↔ Q) → (P ⊣⊢ Q).
Proof.
  intros HPQ; apply (anti_symm (⊢));
    apply impl_entails; rewrite HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : (P ⊣⊢ Q) → True ⊢ P ↔ Q.
Proof. intros ->; apply iff_refl. Qed.

Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
Proof. intros; apply pure_elim with φ1; eauto using pure_intro. Qed.
Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ■ φ1 ⊣⊢ ■ φ2.
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
Proof. auto. Qed.
Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.
Proof. by intros; apply and_mono. Qed.
Lemma and_mono_r P P' Q' : (P' ⊢ Q') → P ∧ P' ⊢ P ∧ Q'.
Proof. by apply and_mono. Qed.
Lemma or_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∨ P' ⊢ Q ∨ Q'.
Proof. auto. Qed.
Lemma or_mono_l P P' Q : (P ⊢ Q) → P ∨ P' ⊢ Q ∨ P'.
Proof. by intros; apply or_mono. Qed.
Lemma or_mono_r P P' Q' : (P' ⊢ Q') → P ∨ P' ⊢ P ∨ Q'.
Proof. by apply or_mono. Qed.
Lemma impl_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P → P') ⊢ Q → Q'.
Proof.
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
  apply impl_elim with P; eauto.
Qed.
Lemma forall_mono {A} (Φ Ψ : A → uPred M) :
  (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ ∀ a, Ψ a.
Proof.
  intros HP. apply forall_intro⇒ a; rewrite -(HP a); apply forall_elim.
Qed.
Lemma exist_mono {A} (Φ Ψ : A → uPred M) :
  (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ ∃ a, Ψ a.
Proof. intros HΦ. apply exist_elim⇒ a; rewrite (HΦ a); apply exist_intro. Qed.
Lemma affine_mono P Q: (P ⊢ Q) → ⧆P ⊢ ⧆Q.
Proof. by intros HP; rewrite ?affine_equiv; apply and_mono_l. Qed.
Global Instance pure_mono' : Proper (impl ==> (⊢)) (@uPred_pure M).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Global Instance and_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance and_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance or_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance or_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
  Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_exist M A).
Proof. intros P1 P2; apply exist_mono. Qed.
Global Instance affine_mono' : Proper ((⊢) ==> (⊢)) (@uPred_affine M).
Proof. intros P1 P2; apply affine_mono. Qed.

Global Instance and_idem : IdemP (⊣⊢) (@uPred_and M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance or_idem : IdemP (⊣⊢) (@uPred_or M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance and_comm : Comm (⊣⊢) (@uPred_and M).
Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
Global Instance True_and : LeftId (⊣⊢) True%I (@uPred_and M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance and_True : RightId (⊣⊢) True%I (@uPred_and M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance False_and : LeftAbsorb (⊣⊢) False%I (@uPred_and M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance and_False : RightAbsorb (⊣⊢) False%I (@uPred_and M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance True_or : LeftAbsorb (⊣⊢) True%I (@uPred_or M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance or_True : RightAbsorb (⊣⊢) True%I (@uPred_or M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance False_or : LeftId (⊣⊢) False%I (@uPred_or M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance or_False : RightId (⊣⊢) False%I (@uPred_or M).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
Global Instance and_assoc : Assoc (⊣⊢) (@uPred_and M).
Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
Global Instance or_comm : Comm (⊣⊢) (@uPred_or M).
Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
Global Instance or_assoc : Assoc (⊣⊢) (@uPred_or M).
Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
Global Instance True_impl : LeftId (⊣⊢) True%I (@uPred_impl M).
Proof.
  intros P; apply (anti_symm (⊢)).
  - by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
Qed.

Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
Proof.
  apply (anti_symm (⊢)); first auto.
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
Qed.
Lemma or_and_r P Q R : P ∧ Q ∨ R ⊣⊢ (P ∨ R) ∧ (Q ∨ R).
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
Lemma and_or_l P Q R : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R.
Proof.
  apply (anti_symm (⊢)); last auto.
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
Qed.
Lemma and_or_r P Q R : (P ∨ Q) ∧ R ⊣⊢ P ∧ R ∨ Q ∧ R.
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
Lemma and_exist_l {A} P (Ψ : A → uPred M) : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a.
Proof.
  apply (anti_symm (⊢)).
  - apply impl_elim_r'. apply exist_elim⇒a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim⇒a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.
Lemma and_exist_r {A} P (Φ: A → uPred M) : (∃ a, Φ a) ∧ P ⊣⊢ ∃ a, Φ a ∧ P.
Proof.
  rewrite -(comm _ P) and_exist_l. apply exist_proper⇒a. by rewrite comm.
Qed.

Lemma impl_curry P Q R : ((P ∧ Q) → R)%I ⊣⊢ (P → Q → R)%I.
Proof.
  apply (anti_symm (⊢)).
  - apply impl_intro_r.
    apply impl_intro_r.
    rewrite -assoc.
    apply impl_elim_l.
  - apply impl_intro_r.
    by rewrite assoc impl_elim_l impl_elim_l.
Qed.

Lemma pure_intro_l φ Q R : φ → (■ φ ∧ Q ⊢ R) → Q ⊢ R.
Proof. intros ? <-; auto using pure_intro. Qed.
Lemma pure_intro_r φ Q R : φ → (Q ∧ ■ φ ⊢ R) → Q ⊢ R.
Proof. intros ? <-; auto using pure_intro. Qed.
Lemma pure_intro_impl φ Q R : φ → (Q ⊢ ■ φ → R) → Q ⊢ R.
Proof. intros ? →. eauto using pure_intro_l, impl_elim_r. Qed.
Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ■ φ ∧ Q ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ■ φ ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_equiv (φ : Prop) : φ → ■ φ ⊣⊢ True.
Proof. intros; apply (anti_symm _); auto using pure_intro. Qed.

Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ a ≡ a.
Proof. rewrite (True_intro P). apply eq_refl. Qed.
Hint Resolve eq_refl'.
Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
Proof. by intros →. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
Lemma eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
Proof.
  apply (eq_rewrite P Q (λ Q, P ↔ Q))%I; first solve_proper; auto using iff_refl.
Qed.

Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ★ P' ⊢ Q ★ Q'.
Proof.
  intros HQ HQ'; unseal.
  split; intros n' x y ?? (x1&x2&y1&y2&?&?&?&?); ∃ x1,x2,y1,y2; cofe_subst x; cofe_subst y.
    split_and!; eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
Qed.
Global Instance Emp_sep : LeftId (⊣⊢) Emp%I (@uPred_sep M).
Proof.
  intros P; unseal; split⇒ n x y Hvalid Hvalidy; split.
  - intros (x1&x2&y1&y2&?&?&?&?); cofe_subst.
    rewrite left_id in Hvalidy *; eauto using uPred_mono, cmra_includedN_r.
  - intros ?; ∃ (core x), x, ∅, y; rewrite cmra_core_l left_id.
    split_and!; eauto. simpl; reflexivity.
Qed.
Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
Proof.
  intros P Q; unseal; split⇒ n x y ??; split;
    intros (x1&x2&y1&y2&?&?&?&?); ∃ x2, x1, y2, y1;
  by rewrite (comm op x2) (comm op y2).
Qed.
Global Instance sep_assoc : Assoc (⊣⊢) (@uPred_sep M).
Proof.
  intros P Q R; unseal; split⇒ n x y ??; split.
  - intros (x1&x2&y1&y2&Hx&Hy&?&z1&z2&w1&w2&Hz&Hw&?&?); ∃ (x1 ⋅ z1), z2, (y1 ⋅ w1), w2;
    split_and?; auto.
    + by rewrite -(assoc op) -Hz -Hx.
    + by rewrite -(assoc op) -Hw -Hy.
    + by ∃ x1, z1, y1, w1.
  - intros (x1&x2&y1&y2&Hx&Hy&(z1&z2&w1&w2&Hz&Hw&?&?)&?).
    ∃ z1, (z2 ⋅ x2), w1, (w2 ⋅ y2); split_and?; auto.
    + by rewrite (assoc op) -Hz -Hx.
    + by rewrite (assoc op) -Hw -Hy.
    + by ∃ z2, x2, w2, y2.
Qed.
Lemma wand_intro_r P Q R : (P ★ Q ⊢ R) → P ⊢ Q -★ R.
Proof.
  unseal⇒ HPQR; split⇒ n x y ??? n' x' y' ????. apply HPQR; auto.
  ∃ x, x', y, y'; split_and?; auto.
  eapply uPred_closed with n; eauto using cmra_validN_op_l.
Qed.
Lemma wand_intro_affine_r P Q R : (⧆P ★ Q ⊢ R) → ⧆P ⊢ ⧆(Q -★ R).
Proof.
  unseal⇒ HPQR. split⇒ n x y ?? Haffine; split; auto.
  intros n' x' y' ????. apply HPQR; auto.
  ∃ x, x', y, y'; split_and?; auto.
  eapply uPred_closed with n; eauto using cmra_validN_op_l.
  destruct Haffine; auto.
Qed.
Lemma wand_elim_l' P Q R : (P ⊢ Q -★ R) → P ★ Q ⊢ R.
  unseal ⇒HPQR. split; intros n x y ?? (?&?&?&?&?&?&?&?). cofe_subst.
  eapply HPQR; eauto using cmra_validN_op_l.
Qed.

Hint Resolve sep_mono.
Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ★ P' ⊢ Q ★ P'.
Proof. by intros; apply sep_mono. Qed.
Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ★ P' ⊢ P ★ Q'.
Proof. by apply sep_mono. Qed.
Global Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Global Instance sep_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -★ P') ⊢ Q -★ Q'.
Proof.
  intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
Qed.
Global Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.

Lemma emp_True: Emp ⊣⊢ ⧆True.
Proof. rewrite affine_equiv left_id. auto. Qed.
Global Instance sep_Emp : RightId (⊣⊢) Emp%I (@uPred_sep M).
Proof. by intros P; rewrite comm left_id. Qed.
Lemma sep_elim_l P Q : P ★ ⧆Q ⊢ P.
Proof. by rewrite (True_intro Q) -emp_True right_id. Qed.
Lemma sep_elim_r P Q : ⧆P ★ Q ⊢ Q.
Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed.
Lemma sep_elim_l' P Q R : (P ⊢ R) → P ★ ⧆Q ⊢ R.
Proof. intros ->; apply sep_elim_l. Qed.
Lemma sep_elim_r' P Q R : (Q ⊢ R) → ⧆P ★ Q ⊢ R.
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
Lemma sep_intro_Emp_l P Q R : (Emp ⊢ P) → (R ⊢ Q) → (R ⊢ P ★ Q).
Proof. by intros; rewrite -(left_id Emp%I uPred_sep R); apply sep_mono. Qed.
Lemma sep_intro_Emp_r P Q R : (R ⊢ P) → (Emp ⊢ Q) → (R ⊢ P ★ Q).
Proof. by intros; rewrite -(right_id Emp%I uPred_sep R); apply sep_mono. Qed.
Lemma sep_elim_Emp_l P Q R : (Emp ⊢ P) → (P ★ R ⊢ Q) → R ⊢ Q.
Proof. by intros HP; rewrite -HP left_id. Qed.
Lemma sep_elim_Emp_r P Q R : (Emp ⊢ P) → (R ★ P ⊢ Q) → R ⊢ Q.
Proof. by intros HP; rewrite -HP right_id. Qed.
Lemma sep_elim_l_equiv P Q {A: cofeT} (a b: A): (P ⊢ a ≡ b) → (P ★ Q ⊢ a ≡ b).
Proof.
  unseal. intros HPre. split. intros n x y ?? (x1&x2&y1&y2&Hx&Hy&HP&HQ).
  simpl. eapply HPre with x1 y1; eauto.
  - eapply cmra_validN_op_l with x2. rewrite -Hx; auto.
  - eapply cmra_validN_op_l with y2. rewrite -Hy; auto.
Qed.
Lemma sep_elim_l_valid P Q {A: cmraT} (a: A): (P ⊢ ✓ a) → (P ★ Q ⊢ ✓ a).
Proof.
  unseal. intros HPre. split. intros n x y ?? (x1&x2&y1&y2&Hx&Hy&HP&HQ).
  simpl. eapply HPre with x1 y1; eauto.
  - eapply cmra_validN_op_l with x2. rewrite -Hx; auto.
  - eapply cmra_validN_op_l with y2. rewrite -Hy; auto.
Qed.
Lemma sep_elim_l_ownM P Q (a: M): (P ⊢ uPred_ownM a) → (P ★ Q ⊢ uPred_ownM a).
Proof.
  unseal. intros HPre. split. intros n x y ?? (x1&x2&y1&y2&Hx&Hy&HP&HQ).
  simpl. destruct HPre as [HPre']. etransitivity; first (eapply (HPre' n x1 y1); eauto).
  - eapply cmra_validN_op_l with x2. rewrite -Hx; auto.
  - eapply cmra_validN_op_l with y2. rewrite -Hy; auto.
  - eexists; eauto.
Qed.
Lemma wand_intro_l P Q R : (Q ★ P ⊢ R) → P ⊢ Q -★ R.
Proof. rewrite comm; apply wand_intro_r. Qed.
Lemma wand_intro_affine_l P Q R : (Q ★ ⧆P ⊢ R) → ⧆P ⊢ ⧆(Q -★ R).
Proof. rewrite comm; apply wand_intro_affine_r. Qed.
Lemma wand_elim_l P Q : (P -★ Q) ★ P ⊢ Q.
Proof. by apply wand_elim_l'. Qed.
Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q.
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
Lemma wand_elim_r' P Q R : (Q ⊢ P -★ R) → P ★ Q ⊢ R.
Proof. intros ->; apply wand_elim_r. Qed.
Lemma wand_apply_l P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
Proof. intros → → <-; apply wand_elim_l. Qed.
Lemma wand_apply_r P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
Proof. intros → → <-; apply wand_elim_r. Qed.
Lemma wand_apply_l' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
Proof. intros → <-; apply wand_elim_l. Qed.
Lemma wand_apply_r' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
Proof. intros → <-; apply wand_elim_r. Qed.
Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.
Proof.
  apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
  apply sep_mono_r, wand_elim_r.
Qed.
Lemma wand_iff_emp P : Emp ⊢ ((P -★ P) ∧ (P -★ P))%I.
Proof. by apply and_intro; apply wand_intro_l; rewrite ?right_id. Qed.
Lemma equiv_wand_iff P Q : P ⊣⊢ Q → Emp ⊢ ((P -★ Q) ∧ (Q -★ P)).
Proof. intros →. apply wand_iff_emp. Qed.

Lemma wand_diag P : ⧆(P -★ P) ⊣⊢ Emp.
Proof.
  apply (anti_symm _); auto.
  - rewrite emp_True. apply affine_mono; auto.
  - rewrite affine_equiv. apply and_intro; auto.
    apply wand_intro_l. by rewrite right_id.
Qed.
Lemma wand_Emp P : (Emp -★ P) ⊣⊢ P.
Proof.
  apply (anti_symm _).
  - eapply sep_elim_Emp_l; first reflexivity. by rewrite wand_elim_r.
  - apply wand_intro_l. rewrite left_id. auto.
Qed.
Lemma wand_entails P Q : (Emp ⊢ P -★ Q) → P ⊢ Q.
Proof.
  intros HPQ. eapply sep_elim_Emp_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
Lemma entails_wand P Q : (P ⊢ Q) → Emp ⊢ P -★ Q.
Proof. by intros; eapply wand_intro_l; rewrite right_id. Qed.
Lemma wand_curry P Q R : (P -★ Q -★ R) ⊣⊢ (P ★ Q -★ R).
Proof.
  apply (anti_symm _).
  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
Qed.

Lemma sep_and P Q : ⧆P ★ ⧆Q ⊢ ⧆(P ∧ Q).
Proof.
  unseal. split. intros n x y ?? (x1&x2&y1&y2&Hx&Hy&(HP&Hy1)&(HQ&Hy2)).
  rewrite Hy1 Hy2 left_id in Hy HP HQ ×.
  intros Hy HP HQ. rewrite Hy Hx.
  simpl; split_and!; auto;
  eapply uPred_mono; eauto using cmra_includedN_r, cmra_includedN_l.
Qed.
Lemma pure_elim_spare φ Q Q' R : (Q ⊢ ⧆■ φ ★ Q') → (φ → (Q ⊢ R)) → Q ⊢ R.
Proof.
  unseal; intros HQP HQR. split⇒ n x ??? HQ; apply HQR; eauto.
  edestruct HQP as (HQP').
  edestruct HQP' as (?&?&?&?&?); try eapply HQ; eauto.
  naive_solver.
Qed.
Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ⧆■ φ ★ Q ⊢ R.
Proof.
  intros. eapply (pure_elim_spare φ _ Q); auto.
Qed.
Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ★ ⧆■ φ ⊢ R.
Proof. intros; eapply (pure_elim_spare φ _ Q); eauto. rewrite comm; eauto. Qed.

Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto.
       unseal; split; naive_solver.
Qed.
Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto.
       unseal; split; naive_solver.
Qed.

Lemma sep_and_l P Q R : P ★ (Q ∧ R) ⊢ (P ★ Q) ∧ (P ★ R).
Proof. auto. Qed.
Lemma sep_and_r P Q R : (P ∧ Q) ★ R ⊢ (P ★ R) ∧ (Q ★ R).
Proof. auto. Qed.
Lemma sep_or_l P Q R : P ★ (Q ∨ R) ⊣⊢ (P ★ Q) ∨ (P ★ R).
Proof.
  apply (anti_symm (⊢)); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
Lemma sep_or_r P Q R : (P ∨ Q) ★ R ⊣⊢ (P ★ R) ∨ (Q ★ R).
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ★ (∃ a, Ψ a) ⊣⊢ ∃ a, P ★ Ψ a.
Proof.
  intros; apply (anti_symm (⊢)).
  - apply wand_elim_r', exist_elim⇒a. apply wand_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim⇒ a; apply sep_mono; auto using exist_intro.
Qed.
Lemma sep_exist_r {A} (Φ: A → uPred M) Q: (∃ a, Φ a) ★ Q ⊣⊢ ∃ a, Φ a ★ Q.
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
Lemma sep_forall_l {A} P (Ψ : A → uPred M) : P ★ (∀ a, Ψ a) ⊢ ∀ a, P ★ Ψ a.
Proof. by apply forall_intro⇒ a; rewrite forall_elim. Qed.
Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ★ Q ⊢ ∀ a, Φ a ★ Q.
Proof. by apply forall_intro⇒ a; rewrite forall_elim. Qed.
Lemma sep_affine_1 P Q: (⧆P ★ ⧆Q) ⊢ ⧆(P ★ Q).
Proof.
  unseal. constructor. intros n x y ?? (x1&x2&y1&y2&Hx&Hy&(?&Hy2)&(?&Hy1)).
    split.
    × ∃ x1, x2, y1, y2. split_and!; auto.
    × by rewrite Hy Hy1 Hy2 right_id.
Qed.

Lemma affine_elim P : ⧆P ⊢ P.
Proof. by rewrite affine_equiv and_elim_l. Qed.
Lemma affine_affine0 P : ⧆⧆P ⊣⊢ ⧆P.
Proof.
  rewrite ?affine_equiv. apply (anti_symm (⊢)); auto.
Qed.
Lemma sep_affine_2 P Q: (⧆P ★ ⧆Q) ⊣⊢ ⧆(⧆P ★ ⧆Q).
Proof.
  apply (anti_symm (⊢)).
  - rewrite -{1}(affine_affine0 P) -{1}(affine_affine0 Q) sep_affine_1 //=.
  - rewrite ?affine_equiv. auto.
Qed.
Lemma sep_affine_3 P Q: (⧆P ★ ⧆Q) ⊣⊢ ⧆(⧆P ★ Q).
Proof.
  apply (anti_symm (⊢)).
  - rewrite -{1}(affine_affine0 P) -{1}(affine_affine0 Q) sep_affine_1 (affine_elim Q) //=.
  - unseal; constructor.
    intros n x y ?? ((x1&x2&y1&y2&Hx&Hy&(?&Hy1)&HQ)&Hempty).
    assert (y2 ≡{n}≡ ∅) as Hy2.
    { rewrite -Hempty Hy Hy1 left_id //=. }
    ∃ x1, x2, y1, y2. split_and!; auto.
    × split; auto.
    × split; auto.
Qed.

Lemma relevant_pure φ : (□ ⧆■ φ) ⊣⊢ (⧆■φ).
Proof.
  unseal. split⇒ n x y ??. simpl; split.
  - intros ((?&?)&?). split; auto. etransitivity; eauto.
  - intros (?&Hempty). split_and!; auto;
    rewrite Hempty persistent_core //=.
Qed.
Lemma relevant_elim P : □ P ⊢ P.
Proof.
  unseal; split⇒ n x y ?? /=.
  intros (HP&Hy). rewrite Hy.
  eapply uPred_mono; eauto using @cmra_included_core, cmra_included_includedN.
Qed.
Lemma relevant_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
Proof.
  unseal⇒ HPQ.
  split⇒ n x y ?? [? ?].
  split; auto. apply HPQ; simpl; auto using @cmra_core_validN. by rewrite ?cmra_core_idemp.
Qed.
Lemma relevant_and P Q : (□ (P ∧ Q)) ⊣⊢ (□ P ∧ □ Q).
Proof. unseal; split⇒n x y ??; naive_solver. Qed.
Lemma relevant_or P Q : (□ (P ∨ Q)) ⊣⊢ (□ P ∨ □ Q).
Proof. unseal; split⇒n x y ??; naive_solver. Qed.
Lemma relevant_forall `{Inhabited A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
Proof.
  unseal; split⇒n x y ??.
  split; simpl; try naive_solver.
  intros HP. split; first naive_solver.
  edestruct (HP inhabitant); eauto.
Qed.
Lemma relevant_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
Proof.
  unseal; split⇒n x y ??; try naive_solver.
Qed.
Lemma relevant_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ★ Q).
Proof.
  unseal; split⇒ n x y ?? [??].
  split; auto.
  ∃ (core x), (core x), (core y), (core y); rewrite -?cmra_core_dup; auto.
Qed.
Lemma relevant_and_sep_l_1' P Q : (□ P ∧ Q) ⊢ (□ P ★ Q).
Proof.
  unseal; split⇒ n x y ?? [[??]?]; ∃ (core x), x, (core y), y; simpl in ×.
  by rewrite ?cmra_core_l ?cmra_core_idemp.
Qed.
Lemma relevant_relevant_later P : (□ ▷ P) ⊣⊢ (□ ▷ □ P).
Proof. unseal. split=>-[|n] x y ??; auto.
       simpl. rewrite ?cmra_core_idemp. naive_solver.
Qed.
Lemma relevant_later_1 P : (□ ▷ P) ⊢ (▷ □ P).
Proof. rewrite relevant_relevant_later. rewrite relevant_elim //=. Qed.
Lemma relevant_relevant_later_contra P Q: □ (▷ □ P -★ Q) ⊢ □ (□ ▷ P -★ Q).
Proof.
  apply relevant_intro'. apply wand_intro_l.
  rewrite relevant_later_1.
  rewrite {1}(relevant_elim (_ -★ _)).
  apply wand_elim_r.
Qed.
Lemma relevant_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
Proof. unseal. intro HPQ. econstructor; intros n x y ?? [? ?].
       split; auto. eapply HPQ; eauto using @cmra_core_validN.
Qed.
Lemma relevant_eq {A:cofeT} (a b : A) : (□ ⧆(a ≡ b)) ⊣⊢ ⧆(a ≡ b).
Proof.
  unseal; apply (anti_symm (⊢)); auto; split.
  - intros n x y ?? ((Hequiv&Hempty)&Hcore).
    split; auto. etransitivity; eauto.
  - intros n x y ?? (Hequiv&Hempty).
    split; rewrite ?Hempty ?persistent_core; naive_solver.
Qed.

Hint Resolve relevant_mono.

Global Instance relevant_mono' : Proper ((⊢) ==> (⊢)) (@uPred_relevant M).
Proof. intros P Q; apply relevant_mono. Qed.
Global Instance relevant_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@uPred_relevant M).
Proof. intros P Q; apply relevant_mono. Qed.
Lemma relevant_impl P Q : □ (P → Q) ⊢ (□ P → □ Q).
Proof.
  apply impl_intro_l; rewrite -relevant_and.
  apply relevant_mono, impl_elim with P; auto.
Qed.
Lemma relevant_affine_and_sep P Q : (□ (⧆P ∧ ⧆Q)) ⊣⊢ (□ (⧆P ★ ⧆Q)).
Proof.
  apply (anti_symm (⊢)).
  - rewrite relevant_and_sep_1; auto.
  - unseal. split; intros n x y ?? ((x1&x2&y1&y2&Hx&Hy&(?&Hy1)&(?&Hy2))&?).
    simpl. rewrite Hy Hy1 Hy2 right_id; split_and!; auto.
    × rewrite -Hy1 Hx.
      eapply uPred_mono; eauto using cmra_included_l, cmra_included_includedN.
    × rewrite -Hy2 Hx.
      eapply uPred_mono; eauto using cmra_included_r, cmra_included_includedN.
    × rewrite Hy1 Hy2 right_id in Hy *; etransitivity; eauto.
Qed.
Lemma relevant_sep P Q : (□ P ★ □ Q) ⊢ (□(P ★ Q)).
Proof.
  unseal; split. intros n x y ?? (x1&x2&y1&y2&Hx&Hy&(HP&Hcore1)&(HQ&Hcore2)).
  split.
  - destruct (cmra_core_monoN n x1 (x1 ⋅ x2)) as (x1'&Hx1'); eauto using cmra_includedN_l.
    destruct (cmra_core_monoN n x2 (x1 ⋅ x2)) as (x2'&Hx2'); eauto using cmra_includedN_r.
    ∃ (core x1 ⋅ x1'), (core x2 ⋅ x2'), (core y1), (core y2).
    rewrite -Hx1' -Hx2'.
    rewrite ?Hx ?Hy {1}Hcore1 {1}Hcore2.
    rewrite -?cmra_core_dup ?cmra_core_distrib -?Hy //=.
    split_and!; auto.
    × rewrite ?Hx1'.
      eapply uPred_mono; eauto using cmra_included_l, cmra_included_r;
      rewrite -Hx1'. apply cmra_core_monoN, cmra_includedN_l.
    × rewrite ?Hx2';
      eapply uPred_mono; eauto using cmra_included_l, cmra_included_r;
      rewrite -Hx2'. apply cmra_core_monoN, cmra_includedN_r.
  - rewrite Hy Hcore1 Hcore2 cmra_core_distrib; auto.
    rewrite -Hy; auto.
Qed.
Lemma relevant_sep_dup'_1 P : (□ P) ⊢ (□ P ★ □ P).
Proof.
  unseal. split; intros n x y ?? (HP&?).
  ∃ x, (core x), y, (core y); split; auto.
  × rewrite cmra_core_r; auto.
  × split_and!; auto.
    ** by rewrite cmra_core_r.
    ** simpl in *; rewrite ?cmra_core_idemp; auto.
    ** simpl. rewrite ?cmra_core_idemp; auto.
Qed.
Lemma relevant_affine_sep P Q : (□ (⧆P ★ ⧆Q) ⊣⊢ (□⧆P ★ □⧆Q)).
Proof.
  apply (anti_symm (⊢)).
  - rewrite -relevant_affine_and_sep. rewrite relevant_sep_dup'_1.
    apply sep_mono; auto.
  - rewrite relevant_sep. auto.
Qed.
Lemma relevant_wand_1 P Q: □ (P -★ Q) ⊢ (□P -★ □Q).
Proof.
  apply wand_intro_r.
  rewrite relevant_sep.
  rewrite wand_elim_l. auto.
Qed.
Lemma relevant_wand_impl_1 P Q : (□ (P -★ Q)) ⊢ (□ (P → Q)).
Proof.
  unseal; split; intros n x y ?? (HPre&?).
  split; auto. intros n' ? Hincluded ????.
  specialize (HPre n' x' (core (core y))).
  rewrite ?cmra_core_r in HPre *; intros HPre.
  destruct Hincluded as (x''&Hin).
  eapply uPred_mono; first eapply HPre; eauto.
  × rewrite Hin assoc -cmra_core_dup -Hin //=.
  × rewrite cmra_core_idemp; auto.
  × rewrite Hin assoc -cmra_core_dup //=.
Qed.
Lemma relevant_entails_l' P Q : (P ⊢ □ Q) → P ⊢ (□ Q ★ P).
Proof.
  unseal. intros HPQ. split. intros n x ? HP.
  destruct HPQ as [HPQ'].
  simpl. ∃ (core x), x, (core y), y.
  split_and!; auto.
  × rewrite cmra_core_l. auto.
  × rewrite cmra_core_l. auto.
  × rewrite ?cmra_core_idemp. eapply HPQ'; eauto.
  × by rewrite cmra_core_idemp.
Qed.
Lemma relevant_entails_r' P Q : (P ⊢ □ Q) → P ⊢ (P ★ □ Q).
Proof. intros; rewrite comm. apply relevant_entails_l'; auto. Qed.


Hint Resolve or_elim or_intro_l' or_intro_r'.

Lemma affine_relevant P : ⧆□ P ⊢ □⧆P.
Proof.
  unseal; auto; econstructor; intros n x y ?? ((?&Hcore)&Heqy); auto.
  split; auto. split; auto.
  by rewrite Heqy persistent_core.
Qed.
Lemma affine_and P Q : (⧆(P ∧ Q)) ⊣⊢ (⧆P ∧ ⧆Q).
Proof. unseal; split⇒n x y ??; naive_solver. Qed.
Lemma affine_and_l P Q : (⧆P ∧ Q) ⊣⊢ (⧆P ∧ ⧆Q).
Proof. unseal; split⇒n x y ??; naive_solver. Qed.
Lemma affine_and_r P Q : (P ∧ ⧆Q) ⊣⊢ (⧆P ∧ ⧆Q).
Proof. unseal; split⇒n x y ??; naive_solver. Qed.
Lemma affine_or P Q : (⧆(P ∨ Q)) ⊣⊢ (⧆P ∨ ⧆Q).
Proof. unseal; split⇒n x y ??; naive_solver. Qed.
Lemma affine_forall `{Inhabited A} (Ψ : A → uPred M) : (⧆ ∀ a, Ψ a) ⊣⊢ (∀ a, ⧆ Ψ a).
Proof.
  unseal; split⇒n x y ??.
  split; simpl; try naive_solver.
  intros HP. split; first naive_solver.
  edestruct (HP inhabitant); eauto.
Qed.
Lemma affine_exist {A} (Ψ : A → uPred M) : (⧆ ∃ a, Ψ a) ⊣⊢ (∃ a, ⧆ Ψ a).
Proof.
  unseal; split⇒n x y ??; try naive_solver.
Qed.
Lemma affine_affine_later P : (⧆ ▷ P) ⊣⊢ (⧆ ▷ ⧆P).
Proof. unseal. split=>-[|n] x y ??; auto.
       simpl. split; intros; naive_solver eauto 2 using dist_le.
Qed.
Lemma affine_later_1 P : (⧆ ▷ P) ⊢ (▷ ⧆ P).
Proof. rewrite affine_affine_later. rewrite affine_elim //=. Qed.
Lemma affine_later_distrib P Q: (⧆▷ (⧆P ★ ⧆Q) ⊢ (⧆▷ P ★ ⧆▷ Q)).
Proof.
  unseal. split=>-[|n] x y ?? [HL ?]; auto; simpl.
  - ∃ x, ∅, ∅, ∅.
    split_and!; rewrite ?right_id; auto.
  - destruct HL as (x1&x2&y1&y2&?&?&(?&Hay1)&(?&Hay2)).
    destruct (cmra_extend n x x1 x2)
      as ([x1' x2']&Hx'&Hx1'&Hx2'); eauto using cmra_validN_S; simpl in ×.
    destruct (cmra_extend (S n) y ∅ ∅)
      as ([y1' y2']&Hy'&Hy1'&Hy2'); eauto using cmra_validN_S; simpl in ×.
      { rewrite ?right_id; eauto using dist_le. }
    ∃ x1', x2', y1', y2'; split_and!; auto.
    × by rewrite Hx1' (dist_le _ _ _ _ Hy1') //= -?Hay1; last lia.
    × by rewrite Hx2' (dist_le _ _ _ _ Hy2') //= -?Hay2; last lia.
Qed.
Lemma relevant_affine P : □⧆P ⊣⊢ ⧆□ P.
Proof.
  apply (anti_symm (⊢)).
  - unseal; auto; econstructor; intros n x y ?? ((?&Hcore)&Heqy); auto.
    split.
    × split; auto.
    × by rewrite Heqy Hcore.
  - unseal; auto; econstructor; intros n x y ?? ((?&Hcore)&Heqy); auto.
    split; auto. split; auto. rewrite -Heqy; auto.
Qed.

Lemma affine_relevant_later P: ⧆▷□P ⊣⊢ ⧆□▷ P.
Proof.
  apply (anti_symm (⊢)).
  - unseal; auto; econstructor; intros n x y ??.
    intros (HP&Haff). split; auto.
    rewrite Haff in HP ×. destruct n as [|n']; simpl; rewrite ?persistent_core; auto.
    intros (HP&_). split; auto.
  - apply affine_mono, relevant_later_1.
Qed.

Lemma unlimited_elim P : ⧈ P ⊢ P.
Proof.
  by rewrite affine_elim relevant_elim.
Qed.
Lemma unlimited_intro' P Q : (⧈ P ⊢ Q) → ⧈ P ⊢ ⧈ Q.
Proof.
  unseal⇒ HPQ.
  split⇒ n x y ?? HP.
  assert (y ≡{n}≡ ∅) as Hequiv.
  { naive_solver. }
  split; [split |]; auto.
  - rewrite Hequiv persistent_core. eapply HPQ; simpl; auto using @cmra_core_validN.
    × apply cmra_valid_validN, ucmra_unit_valid.
    × by rewrite Hequiv //= ?persistent_core in HP ×.
  - by rewrite Hequiv persistent_core.
Qed.
Lemma unlimited_and P Q : (⧈(P ∧ Q)) ⊣⊢ (⧈ P ∧ ⧈ Q).
Proof. by rewrite relevant_and affine_and. Qed.
Lemma unlimited_or P Q : (⧈ (P ∨ Q)) ⊣⊢ (⧈ P ∨ ⧈ Q).
Proof. by rewrite relevant_or affine_or. Qed.
Lemma unlimited_forall `{Inhabited A} (Ψ : A → uPred M) : (⧈ ∀ a, Ψ a) ⊣⊢ (∀ a, ⧈ Ψ a).
Proof. by rewrite relevant_forall affine_forall. Qed.
Lemma unlimited_exist {A} (Ψ : A → uPred M) : (⧈ ∃ a, Ψ a) ⊣⊢ (∃ a, ⧈ Ψ a).
Proof. by rewrite relevant_exist affine_exist. Qed.
Lemma unlimited_and_sep_1 P Q : ⧈ (P ∧ Q) ⊢ ⧈ (P ★ Q).
Proof.
  unseal; split⇒ n x y ?? [[[HP HQ] Hcore] Hempty].
  rewrite Hempty.
  split; [| auto].
  split; [| by rewrite persistent_core].
  ∃ (core x), (core x), ∅, ∅.
  rewrite -Hcore Hempty in HP HQ ×.
  rewrite -cmra_core_dup ?right_id persistent_core; auto.
Qed.
Lemma unlimited_and_sep_l_1 P Q : (⧈ P ∧ Q) ⊢ (⧈P ★ Q).
Proof.
  unseal; split⇒ n x y ?? [[[HP Hcore] Hempty] HQ]; ∃ (core x), x, ∅, ∅; simpl in ×.
  rewrite cmra_core_l cmra_core_idemp right_id persistent_core.
  by rewrite Hempty persistent_core in HP HQ ×.
Qed.
Lemma unlimited_unlimited_later P : (⧈ ▷ P) ⊣⊢ (⧈ ▷ ⧈ P).
Proof.
  rewrite -(relevant_affine P) -(relevant_relevant_later).
  rewrite -(relevant_affine (▷ ⧆ P)) -(affine_affine_later P).
  by rewrite relevant_affine.
Qed.

Lemma unlimited_mono P Q : (P ⊢ Q) → ⧈ P ⊢ ⧈ Q.
Proof. intros. apply unlimited_intro'. by rewrite unlimited_elim. Qed.
Hint Resolve unlimited_mono.
Lemma unlimited_impl P Q : ⧈(P → Q) ⊢ (⧈ P → ⧈ Q).
Proof.
  apply impl_intro_l; rewrite -unlimited_and.
  apply unlimited_mono, impl_elim with P; auto.
Qed.
Lemma unlimited_sep_dup' P : (⧈P) ⊣⊢ (⧈P ★ ⧈P).
Proof.
  apply (anti_symm (⊢)); auto.
  unseal. split⇒n x y ?? [[HP ?] Hempty].
  simpl in ×. ∃ x, (core x), ∅, ∅. rewrite cmra_core_r right_id ?persistent.
  by rewrite Hempty ?persistent_core in HP ×.
Qed.

Global Instance relevant_if_ne n p : Proper (dist n ==> dist n) (@uPred_relevant_if M p).
Proof. solve_proper. Qed.
Global Instance relevant_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_relevant_if M p).
Proof. solve_proper. Qed.
Global Instance relevant_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_relevant_if M p).
Proof. solve_proper. Qed.

Lemma relevant_if_elim p P : □?p P ⊢ P.
Proof. destruct p; simpl; auto using relevant_elim. Qed.
Lemma always_elim_if p P : □ P ⊢ □?p P.
Proof. destruct p; simpl; auto using relevant_elim. Qed.
Lemma relevant_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
Proof. destruct p; simpl; auto using relevant_and. Qed.
Lemma relevant_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
Proof. destruct p; simpl; auto using relevant_or. Qed.
Lemma relevant_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
Proof. destruct p; simpl; auto using relevant_exist. Qed.

Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
Proof.
  unseal⇒ HP; split=>-[|n] x y ???; [done|apply HP; eauto using cmra_validN_S].
Qed.
Lemma later_intro P : P ⊢ ▷ P.
Proof.
  unseal; split⇒ -[|n] x y ???; simpl in *; [done|].
  apply uPred_closed with (S n); eauto using cmra_validN_S.
Qed.
Lemma löb P : (▷ P → P) ⊢ P.
Proof.
  unseal; split⇒ n x y ?? HP; induction n as [|n IH]; [by apply HP|].
  apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
Qed.
Lemma wand_löb P : □(▷ P -★ P) ⊢ □P.
Proof.
  unseal; split⇒ n x y ?? HP; induction n as [|n IH].
  - destruct HP as (HP&Hcore). specialize (HP 0 ∅ ∅). rewrite ?right_id in HP ×. simpl; auto.
    intros HP'. rewrite Hcore. rewrite ?cmra_core_idemp.
    split; auto.
    eapply uPred_closed with 0; first apply HP';
    eauto using @cmra_core_validN, cmra_included_includedN, cmra_included_core.
  - destruct HP as (HP&Hcore).
    simpl. split; auto. simpl in HP.
    generalize (HP (S n) (core x) (core y)). rewrite -?cmra_core_dup. simpl. intros HP'.
    apply HP'; eauto using cmra_core_validN.
    apply IH; eauto using cmra_validN_S.
    split; eauto using dist_le.
    simpl. intros n' x' y' ???. eapply HP; eauto.
Qed.

Lemma relevant_löb_1 P : □(□▷ P -★ □P) ⊢ □P.
Proof.
  unseal; split⇒ n x y ?? HP; induction n as [|n IH].
  - destruct HP as (HP&Hcore); split; auto.
    edestruct HP as (HP'&Heq); eauto using @cmra_core_validN.
    × erewrite cmra_core_l; auto.
    × erewrite cmra_core_l; auto.
    × simpl. auto.
    × rewrite -Heq in HP' ×.
      rewrite ?cmra_core_l {1}Hcore. auto.
  - destruct HP as (HP&Hcore). rewrite Hcore.
    eapply uPred_closed with (S n); eauto using cmra_validN_S, @cmra_core_validN.
    edestruct HP as (HP'&Heq); eauto.
    × erewrite cmra_core_l; auto.
    × erewrite cmra_core_l; auto.
    × simpl. split; auto.
      eapply IH; eauto using cmra_validN_S.
      split; eauto using dist_S.
      eapply uPred_closed with (S n); eauto using cmra_validN_S, @cmra_core_validN.
    × split.
      ** rewrite ?cmra_core_l ?cmra_core_idemp in HP' ×. eauto.
      ** rewrite cmra_core_idemp; trivial.
Qed.
Lemma unlimited_löb_1 P : ⧆□(⧆□▷ P -★ ⧆□P) ⊢ □P.
Proof.
  unseal; split⇒ n x y ?? HP; induction n as [|n IH].
  - destruct HP as ((HP&Hcore)&Haff); split; auto.
    simpl in HP.
    edestruct (HP 0 x ∅) as (HP'&Heq); eauto using cmra_core_validN.
    × erewrite cmra_core_l; auto.
    × rewrite right_id. apply cmra_core_validN; eauto.
    × simpl. split; rewrite ?persistent_core; auto.
    × rewrite -Heq in HP' ×.
      rewrite ?cmra_core_l ?right_id ?cmra_core_idemp {1}Hcore.
      rewrite cmra_core_idemp -cmra_core_dup cmra_core_idemp.
      intros (?&?); auto.
  - destruct HP as ((HP&Hcore)&Haff). rewrite Hcore.
    eapply uPred_closed with (S n); eauto using cmra_validN_S, @cmra_core_validN.
    edestruct HP as (HP'&?); eauto.
    × erewrite cmra_core_l; auto.
    × erewrite cmra_core_l; auto.
    × simpl. split; auto.
      split; auto.
      eapply IH; eauto using cmra_validN_S.
      split; eauto using dist_S.
      split; eauto using dist_S.
      eapply uPred_closed with (S n); eauto using cmra_validN_S, @cmra_core_validN.
    × split.
      ** rewrite ?cmra_core_l ?cmra_core_idemp in HP' ×. simpl. intros (?&?); eauto.
      ** rewrite cmra_core_idemp; trivial.
Qed.
Lemma relevant_löb_2 P : □(□▷ P → □P) ⊢ □P.
Proof.
  unseal; split⇒ n x y ?? HP; induction n as [|n IH].
  - destruct HP as (HP&Hcore); split; auto.
    edestruct HP as (HP'&?); eauto using @cmra_core_validN.
    × split; simpl; auto.
      by rewrite cmra_core_idemp.
    × by rewrite ?cmra_core_idemp in HP' ×.
  - edestruct HP as (HP'&Hcore).
    simpl; split; auto.
    rewrite -(cmra_core_idemp x).
    rewrite -(cmra_core_idemp y).
    apply HP'; eauto using @cmra_core_validN.
    split; last (by rewrite cmra_core_idemp).

    rewrite ?cmra_core_idemp. apply IH; eauto using cmra_validN_S.
    split; last (by eauto using dist_le).
    eapply uPred_closed with (S n); eauto using cmra_validN_S, @cmra_core_validN.
Qed.
Lemma relevant_löb_3 P : □(▷ P → P) ⊢ □P.
Proof.
  apply relevant_mono. apply löb.
Qed.
Lemma later_and P Q : (▷ (P ∧ Q)) ⊣⊢ (▷ P ∧ ▷ Q).
Proof. unseal; split⇒ -[|n] x y; by split. Qed.
Lemma later_or P Q : (▷ (P ∨ Q)) ⊣⊢ (▷ P ∨ ▷ Q).
Proof. unseal; split⇒ -[|n] x y; simpl; tauto. Qed.
Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
Proof. unseal; by split⇒ -[|n] x y. Qed.
Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ (▷ ∃ a, Φ a).
Proof. unseal; by split⇒ -[|[|n]] x y. Qed.
Lemma later_exist_2 `{Inhabited A} (Φ : A → uPred M) :
  (▷ ∃ a, Φ a)%I ⊢ (∃ a, ▷ Φ a)%I.
Proof. unseal; split⇒ -[|[|n]] x y; done || by ∃ inhabitant. Qed.
Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ ▷ P ★ ▷ Q.
Proof.
  unseal; split⇒ n x z ??; split.
  - destruct n as [|n]; simpl.
    { by ∃ x, (core x), z, (core z); rewrite ?cmra_core_r. }
    intros (x1&x2&z1&z2&Hx&Hz&?&?);
      destruct (cmra_extend n x x1 x2) as ([y1 y2]&Hx'&Hy1&Hy2);
      eauto using cmra_validN_S; simpl in ×.
      destruct (cmra_extend n z z1 z2) as ([q1 q2]&Hz'&Hq1&Hq2);
      eauto using cmra_validN_S; simpl in ×.
    ∃ y1, y2, q1, q2; split_and!; [by rewrite Hx'| by rewrite Hz'
                                        | by rewrite Hy1 Hq1 | by rewrite Hy2 Hq2].
  - destruct n as [|n]; simpl; [done|intros (x1&x2&z1&z2&Hx&Hz&?&?)].
    ∃ x1, x2, z1, z2; split_and!; eauto using dist_S.
Qed.
Lemma later_sep_affine_l P Q : (▷ (⧆P ★ Q)) ⊣⊢ (⧆▷ P ★ ▷ Q).
Proof.
  unseal; split⇒ n x z ??; split.
  - destruct n as [|n]; simpl.
    { by intros; ∃ x, (core x), ∅, z; rewrite ?cmra_core_r ?left_id. }
    intros (x1&x2&z1&z2&Hx&Hz&(?&Haff)&?);
      destruct (cmra_extend n x x1 x2) as ([y1 y2]&Hx'&Hy1&Hy2);
      eauto using cmra_validN_S; simpl in ×.
      destruct (cmra_extend n z z1 z2) as ([q1 q2]&Hz'&Hq1&Hq2);
      eauto using cmra_validN_S; simpl in ×.
    ∃ y1, y2, ∅, (q1 ⋅ q2); split_and!.
    × by rewrite Hx'.
    × by rewrite left_id Hz'.
    × by rewrite -Haff Hy1.
    × done.
    × by rewrite Hq1 Hq2 Hy2 Haff ?left_id.
  - destruct n as [|n]; simpl; [done|intros (x1&x2&z1&z2&Hx&Hz&(?&?)&?)].
    ∃ x1, x2, z1, z2; split_and!; eauto using dist_S.
Qed.

Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
Proof. by intros →. Qed.
Hint Resolve later_mono later_proper.
Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Lemma later_True : ▷ True ⊣⊢ True.
Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q.
Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed.
Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
  ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. Qed.
Lemma later_wand P Q : ▷ (P -★ Q) ⊢ ▷ P -★ ▷ Q.
Proof. apply wand_intro_r;rewrite -later_sep; eauto using wand_elim_l. Qed.
Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
Lemma later_sep_affine_r P Q : (▷ (P ★ ⧆Q)) ⊣⊢ (▷ P ★ ⧆▷ Q).
Proof. by rewrite comm later_sep_affine_l comm. Qed.

Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
Proof. induction m; simpl. by intros ???. solve_proper. Qed.
Global Instance laterN_proper m :
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _.

Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
Proof. done. Qed.
Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
Proof. induction n; simpl; auto. Qed.
Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
Proof. induction n1; simpl; auto. Qed.
Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.

Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
Proof. induction n; simpl; auto. Qed.
Lemma laterN_intro n P : P ⊢ ▷^n P.
Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
Lemma laterN_exist_1 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ (▷^n ∃ a, Φ a).
Proof. induction n as [|n IH]; simpl; rewrite ?later_exist_1; auto. Qed.
Lemma laterN_exist_2 `{Inhabited A} n (Φ : A → uPred M) :
  (▷^n ∃ a, Φ a) ⊢ ∃ a, ▷^n Φ a.
Proof. induction n as [|n IH]; simpl; rewrite -?later_exist_2; auto. Qed.
Lemma laterN_sep n P Q : ▷^n (P ★ Q) ⊣⊢ ▷^n P ★ ▷^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.

Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@uPred_laterN M n).
Proof. intros P Q; apply laterN_mono. Qed.
Global Instance laterN_flip_mono' n :
  Proper (flip (⊢) ==> flip (⊢)) (@uPred_laterN M n).
Proof. intros P Q; apply laterN_mono. Qed.
Lemma laterN_True n : ▷^n True ⊣⊢ True.
Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed.
Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
Proof.
  apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
Qed.
Lemma laterN_exist n `{Inhabited A} (Φ : A → uPred M) :
  ▷^n (∃ a, Φ a) ⊣⊢ (∃ a, ▷^n Φ a).
Proof. apply: anti_symm; eauto using laterN_exist_2, laterN_exist_1. Qed.
Lemma laterN_wand n P Q : ▷^n (P -★ Q) ⊢ ▷^n P -★ ▷^n Q.
Proof.
  apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
Qed.
Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.

Lemma ownM_op (a1 a2 : M) :
  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2.
Proof.
  unseal; split⇒ n x y ??; split.
  - intros [z ?]; ∃ a1, (a2 ⋅ z), y, (core y);
    split_and!; [by rewrite (assoc op)| by rewrite cmra_core_r | |].
    × by ∃ (core a1); rewrite cmra_core_r.
    × by ∃ z.
  - intros (y1&y2&q1&q2&Hx&Hy&[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 ownM_op' (a1 a2 : M) :
  uPred_ownM (a1 ⋅ a2) ⊣⊢ (uPred_ownM a1 ★ ⧆ uPred_ownM a2).
Proof.
  unseal; split⇒ n x y ??; split.
  - intros [z ?]; ∃ a1, (a2 ⋅ z), y, ∅ ;
    split_and!; [by rewrite (assoc op)| by rewrite right_id | |].
    × by ∃ (core a1); rewrite cmra_core_r.
    × split; auto. by ∃ z.
  - intros (y1&y2&q1&q2&Hx&Hy&[z1 Hy1]&([z2 Hy2]&Hq2)); ∃ (z1 ⋅ z2).
    by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
      -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
Lemma ownM_op'' (a1 a2 : M) :
  ⧆ uPred_ownM (a1 ⋅ a2) ⊣⊢ (⧆ uPred_ownM a1 ★ ⧆ uPred_ownM a2).
Proof.
  unseal; split⇒ n x y ??; split.
  - intros [[z ?] Heqy]. ∃ a1, (a2 ⋅ z), y, ∅ ;
    split_and!; [by rewrite (assoc op)| by rewrite right_id | |].
    × rewrite Heqy; split; auto. ∃ (core a1); rewrite cmra_core_r //=.
    × split; auto. by ∃ z.
  - intros (y1&y2&q1&q2&Hx&Hy&([z1 Hy1]&Hq1)&([z2 Hy2]&Hq2)).
    split.
    × ∃ (z1 ⋅ z2).
        by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
           -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
    × rewrite Hy Hq1 Hq2 right_id //=.
Qed.
Lemma unlimited_ownM_core (a : M) : (⧈ uPred_ownM (core a)) ⊣⊢ ⧆ uPred_ownM (core a).
Proof.
  split⇒ n x y; split.
  - unseal. intros (([a' Hx]&?)&?); simpl. split; auto.
    ∃ (a' ⋅ x). by rewrite assoc -Hx cmra_core_l.
  - unseal; intros ([a' Hx]&->); simpl. rewrite -(cmra_core_idemp a) Hx.
    split_and!; try (rewrite ?persistent_core; auto; done).
    apply cmra_core_monoN, cmra_includedN_l.
Qed.
Lemma unlimited_ownM (a : M) : Persistent a → (⧈ uPred_ownM a) ⊣⊢ ⧆ uPred_ownM a.
Proof. intros. by rewrite -(persistent_core a) unlimited_ownM_core. Qed.
Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
Proof. unseal; split⇒ n x ??. by ∃ x; simpl. Qed.
Lemma ownM_something' : Emp ⊢ ⧆∃ a, uPred_ownM a.
Proof. unseal; split⇒ n x ??. by split; auto; ∃ x; simpl. Qed.
Lemma ownM_empty : True ⊢ uPred_ownM ∅.
Proof. unseal; split⇒ n x ??; by ∃ x; rewrite left_id. Qed.
Lemma ownM_empty' : Emp ⊢ ⧆uPred_ownM ∅.
Proof. unseal; split⇒ n x ??; by split; auto; ∃ x; rewrite left_id. Qed.

Lemma ownMl_op (a1 a2 : M) :
  uPred_ownMl (a1 ⋅ a2) ⊣⊢ (uPred_ownMl a1 ★ uPred_ownMl a2).
Proof.
  unseal; split⇒ n x y ??; split.
  - intros ?. ∃ x, (core x), a1, a2;
    split_and!; simpl; auto.
    by rewrite cmra_core_r.
  - intros (y1&y2&q1&q2&Hx&Hy&Hy1&Hy2).
    simpl in ×. by rewrite Hy Hy1 Hy2.
Qed.
Lemma relevant_ownMl_core (a : M) : (□ uPred_ownMl (core a)) ⊣⊢ uPred_ownMl (core a).
Proof.
  split⇒ n x y; split.
  - unseal. intros (Hx&?); simpl. simpl in Hx. rewrite Hx. auto.
  - unseal=>//=. intros Heq. rewrite -?Heq -(cmra_core_idemp a) Heq.
    by rewrite persistent_core.
Qed.
Lemma relevant_ownMl (a : M) : Persistent a → (□ uPred_ownMl a) ⊣⊢ uPred_ownMl a.
Proof. intros. by rewrite -(persistent_core a) relevant_ownMl_core. Qed.
Lemma ownMl_something : True ⊢ ∃ a, uPred_ownMl a.
Proof. unseal; split⇒ n x y ???. by ∃ y; simpl. Qed.
Lemma ownMl_empty : Emp ⊣⊢ uPred_ownMl ∅.
Proof. unseal; split⇒ n x y ??. simpl. split; auto. Qed.

Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof.
  unseal; split⇒ n x y Hv ? [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
Qed.
Lemma ownMl_valid (a : M) : uPred_ownMl a ⊢ (uPred_ownMl a ★ ⧆✓ a).
Proof.
  unseal; split⇒ n x y Hv //= ? Heq.
  ∃ x, (core x), y, ∅. rewrite ?cmra_core_r ?right_id. split_and!; auto; by cofe_subst.
Qed.
Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊢ ✓ a.
Proof. unseal⇒ ?; split⇒ n x y ? ? _ /=; by apply cmra_valid_validN. Qed.
Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
Proof. unseal⇒ Ha; split⇒ n x y ???; apply Ha, cmra_validN_le with n; auto. Qed.
Lemma relevant_valid {A : cmraT} (a : A) : □ ⧆ (✓ a) ⊣⊢ ⧆ (✓ a).
Proof.
  unseal. split⇒ n x y ??. simpl; split.
  - intros ((?&?)&?). split; auto. etransitivity; eauto.
  - intros (?&Hempty). split_and!; auto; rewrite Hempty persistent_core //=.
Qed.
Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split⇒ n x y _ ?; apply cmra_validN_op_l. Qed.

Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed.
Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op'. eauto. Qed.

Lemma prod_equivI {A B : cofeT} (x y : A × B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
Proof. by unseal. Qed.
Lemma prod_validI {A B : cmraT} (x : A × B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
Proof. by unseal. Qed.

Lemma later_equivI {A : cofeT} (x y : later A) :
  x ≡ y ⊣⊢ ▷ (later_car x ≡ later_car y).
Proof. by unseal. Qed.

Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : ✓ a ⊣⊢ (■ ✓ a).
Proof. unseal; split⇒ n x y _ _. by rewrite /= -cmra_discrete_valid_iff. Qed.
Lemma timeless_eq {A : cofeT} (a b : A) : Timeless a → a ≡ b ⊣⊢ ■ (a ≡ b).
Proof.
  unseal⇒ ?. apply (anti_symm (⊢)); split⇒ n x y ??; by apply (timeless_iff n).
Qed.

Lemma option_equivI {A : cofeT} (mx my : option A) :
  mx ≡ my ⊣⊢ match mx, my with
             | Some x, Some y ⇒ x ≡ y | None, None ⇒ True | _, _ ⇒ False
             end.
Proof.
  uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
Qed.
Lemma option_validI {A : cmraT} (mx : option A) :
  ✓ mx ⊣⊢ match mx with Some x ⇒ ✓ x | None ⇒ True end.
Proof. uPred.unseal. by destruct mx. Qed.

Lemma timelessP_spec P : TimelessP P ↔ ∀ n x y, ✓{n} x → ✓{n} y → P 0 x y → P n x y.
Proof.
  split.
  - intros HP n x y ???; induction n as [|n]; auto.
    move: HP; rewrite /TimelessP; unseal⇒ /uPred_in_entails /(_ (S n) x y).
    by destruct 1; auto using cmra_validN_S.
  - move⇒ HP; rewrite /TimelessP; unseal; split⇒ -[|n] x y /=; auto; left.
    apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.

Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%I.
Proof. by apply timelessP_spec; unseal ⇒ -[|n] x. Qed.
Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
   TimelessP (✓ a : uPred M)%I.
Proof.
  apply timelessP_spec; unseal⇒ n x y /=. by rewrite -!cmra_discrete_valid_iff.
Qed.
Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
Proof.
  intros; rewrite /TimelessP later_or (timelessP _) (timelessP Q); eauto 10.
Qed.
Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
Proof.
  rewrite !timelessP_spec; unseal⇒ HP [|n] x y ?? HPQ [|n'] x' ?????; auto.
  apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le.
Qed.
Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
Proof.
  intros; rewrite /TimelessP later_sep (timelessP P) (timelessP Q).
  apply wand_elim_l', or_elim; apply wand_intro_r; auto;
  first (apply wand_elim_r', or_elim; apply wand_intro_r; auto;
         first rewrite ?(comm _ Q); auto).
  × etransitivity; [|eapply or_intro_r]; unseal.
    split⇒n x y ?? HP. destruct n; simpl in *; auto.
    naive_solver.
  × etransitivity; [|eapply or_intro_r]; unseal.
    split⇒n x y ?? HP. destruct n; simpl in *; auto.
    naive_solver.
Qed.
Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
  rewrite !timelessP_spec; unseal⇒ HP [|n] x y ?? HPQ [|n'] x' y' ????; auto.
  apply HP, HPQ, uPred_closed with (S n');
    eauto 3 using cmra_validN_le, cmra_validN_op_r.
Qed.
Global Instance forall_timeless {A} (Ψ : A → uPred M) :
  (∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
Proof. by setoid_rewrite timelessP_spec; unseal⇒ HΨ n x y ??? a; apply HΨ. Qed.
Global Instance exist_timeless {A} (Ψ : A → uPred M) :
  (∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
Proof.
  by setoid_rewrite timelessP_spec; unseal⇒ HΨ [|n] x y ??;
    [|intros [a ?]; ∃ a; apply HΨ].
Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
  Timeless a → TimelessP (a ≡ b : uPred M)%I.
Proof.
  intro; apply timelessP_spec; unseal⇒ n x y ???; by apply equiv_dist, timeless.
Qed.
Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
Proof.
  intro; apply timelessP_spec; unseal⇒ n x y ???; apply cmra_included_includedN,
    cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.


Lemma atimelessP_spec P : ATimelessP P ↔ ∀ n x, ✓{n} x → P 0 x ∅ → P n x ∅.
Proof.
  split.
  - intros HP n x ??; induction n as [|n]; auto.
    move: HP; rewrite /ATimelessP; unseal⇒ /uPred_in_entails /(_ (S n) x ∅).
    destruct 1 as [ HlP | HlF]; auto using cmra_validN_S, ucmra_unit_validN.
    × split; auto. eapply IHn; auto using cmra_validN_S.
    × destruct HlP as (HP&?Haff). auto.
    × simpl in ×. exfalso; auto.
  - move⇒ HP; rewrite /ATimelessP; unseal; split⇒ -[|n] x y /=; auto.
    intros ?? (HP'&Haff). left.
    split; auto. rewrite Haff.
    apply HP, uPred_closed with n; eauto using cmra_validN_le, ucmra_unit_validN.
    rewrite -(dist_le _ _ _ _ Haff); auto.
Qed.


Lemma timeless_atimeless P: TimelessP P → ATimelessP P.
Proof.
  rewrite /TimelessP /ATimelessP. intros →. rewrite ?affine_or.
  apply or_mono; eauto using affine_elim.
Qed.

Global Instance const_atimeless φ : ATimelessP (■ φ : uPred M)%I.
Proof. apply timeless_atimeless; apply _. Qed.
Global Instance valid_atimeless {A : cmraT} `{CMRADiscrete A} (a : A) :
   ATimelessP (✓ a : uPred M)%I.
Proof. apply timeless_atimeless; apply _. Qed.
Global Instance and_atimeless P Q: ATimelessP P → ATimelessP Q → ATimelessP (P ∧ Q).
Proof. rewrite /ATimelessP later_and ?affine_and or_and_r; apply and_mono. Qed.
Global Instance or_atimeless P Q : ATimelessP P → ATimelessP Q → ATimelessP (P ∨ Q).
Proof.
  intros; rewrite /ATimelessP later_or ?affine_or (atimelessP _) (atimelessP Q); eauto 10.
Qed.
Global Instance impl_atimeless P Q : ATimelessP Q → ATimelessP (P → Q).
Proof.
  rewrite !atimelessP_spec; unseal⇒ HP [|n] x ? HPQ [|n'] x' ?????; auto.
  apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le.
Qed.
Global Instance sep_atimeless_1 P Q: TimelessP P → TimelessP Q → ATimelessP (P ★ Q).
Proof.
  intros; apply timeless_atimeless; apply _.
Qed.
Global Instance sep_atimeless_2 P Q:
  AffineP P → AffineP Q → ATimelessP P → ATimelessP Q → ATimelessP (P ★ Q).
Proof.
  intros; rewrite /ATimelessP.
  rewrite {1}(affineP P).
  rewrite {1}(affineP Q).
  rewrite affine_later_distrib.
  rewrite (atimelessP P) (atimelessP Q).
  rewrite sep_or_l. rewrite sep_or_r.
  apply or_elim.
  - apply or_elim.
    × apply or_intro_l'. apply sep_affine_1.
    × apply or_intro_r'. apply sep_elim_l.
  - apply or_intro_r'. rewrite sep_or_r.
    apply or_elim; first apply sep_elim_r.
    unseal. split⇒ -[|n] x y ?? Hfalse /=; auto.
    destruct Hfalse as (?&?&?&?&?&?&?&?). auto.
Qed.
Global Instance wand_atimeless P Q : AffineP P → ATimelessP Q → ATimelessP (P -★ Q).
Proof.
  rewrite !atimelessP_spec.
  unseal⇒ HA HP [|n] x ? HPQ [|n'] x' y' ??? HP'; auto.
  apply affineP in HP'; eauto using cmra_validN_op_r.
  revert HP'. unseal.
  intros (HP'&Haff).
  rewrite Haff ?right_id.
  apply HP; auto.
  specialize (HPQ 0 x' ∅). rewrite ?left_id in HPQ *=> HPQ.
  eapply HPQ;
    eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
  apply uPred_closed with (S n');
    eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
  rewrite -Haff. eauto.
Qed.
Global Instance forall_atimeless {A} (Ψ : A → uPred M) :
  (∀ x, ATimelessP (Ψ x)) → ATimelessP (∀ x, Ψ x).
Proof. by setoid_rewrite atimelessP_spec; unseal⇒ HΨ n x ?? a; apply HΨ. Qed.
Global Instance exist_atimeless {A} (Ψ : A → uPred M) :
  (∀ x, ATimelessP (Ψ x)) → ATimelessP (∃ x, Ψ x).
Proof.
  by setoid_rewrite atimelessP_spec; unseal⇒ HΨ [|n] x ?;
    [|intros [a ?]; ∃ a; apply HΨ].
Qed.
Global Instance relevant_atimeless P : ATimelessP P → ATimelessP (□ P).
Proof.
  intros ?; rewrite /ATimelessP.
  rewrite affine_relevant_later.
  rewrite -relevant_affine atimelessP relevant_or relevant_affine.
  apply or_mono; auto using relevant_elim.
Qed.
Global Instance affine_atimeless P : ATimelessP P → ATimelessP (⧆ P).
Proof.
  rewrite /ATimelessP. intros HP.
  by rewrite -affine_affine_later HP affine_affine0.
Qed.
Global Instance eq_atimeless {A : cofeT} (a b : A) :
  Timeless a → ATimelessP (a ≡ b : uPred M)%I.
Proof. intros. apply timeless_atimeless; apply _. Qed.
Global Instance ownM_atimeless (a : M) : Timeless a → ATimelessP (uPred_ownM a).
Proof. intros. apply timeless_atimeless; apply _. Qed.

Global Instance emp_relevant: RelevantP (Emp: uPred M)%I.
Proof.
  rewrite /RelevantP. unseal. split⇒ n x y ??. simpl; intros →.
  rewrite persistent_core; auto.
Qed.
Global Instance pure_relevant φ : RelevantP (⧆■ φ : uPred M)%I.
Proof. by rewrite /RelevantP relevant_pure. Qed.
Global Instance relevant_relevant P : RelevantP (□ P).
Proof. by intros; apply relevant_intro'. Qed.
Global Instance relevant_affine' P : RelevantP P → RelevantP (⧆ P).
Proof. by intros; rewrite /RelevantP; rewrite relevant_affine;
       rewrite {1}(relevantP P).
Qed.
Global Instance and_relevant P Q :
  RelevantP P → RelevantP Q → RelevantP (P ∧ Q).
Proof. by intros; rewrite /RelevantP relevant_and; apply and_mono. Qed.
Global Instance or_relevant P Q :
  RelevantP P → RelevantP Q → RelevantP (P ∨ Q).
Proof. by intros; rewrite /RelevantP relevant_or; apply or_mono. Qed.
Global Instance sep_relevant P Q :
  RelevantP P → RelevantP Q → RelevantP (P ★ Q).
Proof.
  intros. rewrite /RelevantP {1}(relevantP P) {1}(relevantP Q).
  apply relevant_sep.
Qed.
Global Instance forall_relevant `{Inhabited A} (Ψ : A → uPred M) :
  (∀ x, RelevantP (Ψ x)) → RelevantP (∀ x, Ψ x).
Proof. by intros; rewrite /RelevantP relevant_forall; apply forall_mono. Qed.
Global Instance exist_relevant {A} (Ψ : A → uPred M) :
  (∀ x, RelevantP (Ψ x)) → RelevantP (∃ x, Ψ x).
Proof. by intros; rewrite /RelevantP relevant_exist; apply exist_mono. Qed.
Global Instance eq_relevant {A : cofeT} (a b : A) :
  RelevantP (⧆ (a ≡ b) : uPred M)%I.
Proof. by intros; rewrite /RelevantP relevant_eq. Qed.
Global Instance valid_relevant {A : cmraT} (a : A) :
  RelevantP (⧆✓ a : uPred M)%I.
Proof. by intros; rewrite /RelevantP relevant_valid. Qed.
Global Instance ownM_relevant : Persistent a → RelevantP (⧆(@uPred_ownM M a)).
Proof. intros; rewrite /RelevantP. rewrite relevant_affine unlimited_ownM //=. Qed.
Global Instance ownMl_relevant : Persistent a → RelevantP (@uPred_ownMl M a).
Proof. intros; rewrite /RelevantP. rewrite relevant_ownMl //=. Qed.
Global Instance default_relevant {A} P (Ψ : A → uPred M) (mx : option A) :
  RelevantP P → (∀ x, RelevantP (Ψ x)) → RelevantP (default P mx Ψ).
Proof. destruct mx; apply _. Qed.

Lemma relevant_relevant' P `{!RelevantP P} : (□ P) ⊣⊢ P.
Proof. apply (anti_symm (⊢)); auto using relevant_elim. Qed.
Lemma relevant_intro P Q `{!RelevantP P} : (P ⊢ Q) → P ⊢ □ Q.
Proof. rewrite -(relevant_relevant' P). apply relevant_intro'. Qed.
Lemma relevant_and_sep_l_1 P Q `{!RelevantP P} : (P ∧ Q) ⊢ (P ★ Q).
Proof. by rewrite -(relevant_relevant' P) relevant_and_sep_l_1'. Qed.
Lemma relevant_and_sep_r_1 P Q `{!RelevantP Q} : (P ∧ Q) ⊢ (P ★ Q).
Proof. rewrite -?(comm _ Q). apply relevant_and_sep_l_1; auto. Qed.
Lemma relevant_sep_dup P `{!RelevantP P} : P ⊢ (P ★ P).
Proof. by rewrite -(relevant_relevant' P) -relevant_sep_dup'_1. Qed.
Lemma relevant_entails_l P Q `{!RelevantP Q} : (P ⊢ Q) → P ⊢ (Q ★ P).
Proof. by rewrite -(relevant_relevant' Q); apply relevant_entails_l'. Qed.
Lemma relevant_entails_r P Q `{!RelevantP Q} : (P ⊢ Q) → P ⊢ (P ★ Q).
Proof. by rewrite -(relevant_relevant' Q); apply relevant_entails_r'. Qed.
Lemma relevant_sep' P Q `{!RelevantP P, !RelevantP Q} : (P ★ Q) ⊣⊢ (□(P ★ Q)).
Proof.
  apply (anti_symm (⊢)).
  - rewrite (relevant_relevant'). auto.
  - rewrite relevant_elim. auto.
Qed.

Global Instance affine_affine' P : AffineP (⧆ P).
Proof. rewrite /AffineP ?affine_equiv; auto. Qed.
Global Instance affine_relevant' P : AffineP P → AffineP (□ P).
Proof. intros. rewrite /AffineP. rewrite -relevant_affine. auto. Qed.
Global Instance emp_affine : AffineP (Emp: uPred M)%I.
Proof. by intros; rewrite /AffineP affine_equiv; auto. Qed.
Global Instance and_affine P Q :
  AffineP P → AffineP Q → AffineP (P ∧ Q).
Proof. by intros; rewrite /AffineP affine_and; apply and_mono. Qed.
Global Instance or_affine P Q :
  AffineP P → AffineP Q → AffineP (P ∨ Q).
Proof. by intros; rewrite /AffineP affine_or; apply or_mono. Qed.
Global Instance sep_affine P Q :
  AffineP P → AffineP Q → AffineP (P ★ Q).
Proof. by intros; rewrite /AffineP -sep_affine_1; apply sep_mono. Qed.
Global Instance forall_affine `{Inhabited A} (Ψ : A → uPred M) :
  (∀ x, AffineP (Ψ x)) → AffineP (∀ x, Ψ x).
Proof. rewrite /AffineP affine_forall. apply forall_mono. Qed.
Global Instance exist_affine {A} (Ψ : A → uPred M) :
  (∀ x, AffineP (Ψ x)) → AffineP (∃ x, Ψ x).
Proof. by intros; rewrite /AffineP affine_exist; apply exist_mono. Qed.
Global Instance default_affine {A} P (Ψ : A → uPred M) (mx : option A) :
  AffineP P → (∀ x, AffineP (Ψ x)) → AffineP (default P mx Ψ).
Proof. destruct mx; apply _. Qed.

Lemma affine_affine P `{!AffineP P} : (⧆ P) ⊣⊢ P.
Proof. apply (anti_symm (⊢)); auto using affine_elim. Qed.
Lemma affine_intro P Q `{!AffineP P} : (P ⊢ Q) → P ⊢ ⧆ Q.
Proof. rewrite -(affine_affine P). rewrite ?affine_equiv; auto. Qed.
Lemma sep_affine_distrib P Q `{!AffineP P, !AffineP Q}:
  (⧆ P ★ ⧆ Q) ⊣⊢ ⧆ (P ★ Q).
Proof. rewrite ?affine_affine. auto. Qed.
Lemma affine_later_distrib' P Q `{!AffineP P, !AffineP Q}: (⧆▷ (P ★ Q) ⊢ (⧆▷ P ★ ⧆▷ Q)).
Proof. by rewrite -{1}(affine_affine P) -{1}(affine_affine Q) affine_later_distrib. Qed.
Lemma affine_sep_elim_l' P Q R `{!AffineP Q}: (P ⊢ R) → P ★ Q ⊢ R.
Proof. rewrite -(affine_affine Q); auto. Qed.
Lemma affine_sep_elim_r' P Q R `{!AffineP P}: (Q ⊢ R) → P ★ Q ⊢ R.
Proof. rewrite -(affine_affine P); auto. Qed.

End uPred_logic.

Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint Resolve relevant_mono affine_elim : I.
Hint Resolve sep_elim_l' sep_elim_r' sep_mono affine_sep_elim_l' affine_sep_elim_r' : I.
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl eq_refl' : I.
End uPred.