From iris.base_logic Require Import upred derived lib.fancy_updates
 primitive lib.wsat soundness.

Import uPred_primitive.
Import uPred.

Require Import iris.proofmode.tactics.
(* Some interesting lemmas! *)

Lemma core_unit {M : ucmraT} : core (∅ : M) ≡ ∅.
Proof. by rewrite /core /core' ucmra_pcore_unit. Qed.

Lemma except_0_sep' (M : ucmraT) (P Q : uPred M) : (◇ (P ★ Q))%I ⊢ (◇ P ★ ◇ Q)%I.
Proof. by rewrite except_0_sep. Qed.

 Lemma except_0_exist (M : ucmraT) A `{Inhabited A} (P : A → uPred M) :
  (◇ ∃ x, P x) ⊢ ∃ x, ◇ P x.
 Proof.
   rewrite /uPred_except_0; unseal; constructor => n x Hnx Hde.
   destruct n.
   - exists inhabitant; by left.
   - destruct Hde as [Hde|Hde]; first done. destruct Hde as [z Hde].
     by exists z; right.
 Qed.

 Lemma except_0_forall (M : ucmraT) A (P : A → uPred M) :
  (∀ x, ◇ P x) ⊢ (◇ ∀ x, P x).
 Proof.
   rewrite /uPred_except_0; unseal; constructor => n x Hnx Hde.
   destruct n; first by left.
   right=>z. specialize (Hde z); destruct Hde as [Hde|Hde]; done.
 Qed.

(* Naught modality *)
Program Definition uPred_naught_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n ∅ |}.
Next Obligation.
  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @ucmra_unit_validN. Qed.
Definition uPred_naught_aux : { x | x = @uPred_naught_def }. by eexists. Qed.
Definition uPred_naught {M} := proj1_sig uPred_naught_aux M.
Definition uPred_naught_eq :
  @uPred_naught = @uPred_naught_def := proj2_sig uPred_naught_aux.

(* Notation for naught: ⨳ (\smashtimes) *)
Notation "⨳ P" := (uPred_naught P)
  (at level 20, right associativity) : uPred_scope.

(* A plain fact is one that holds independent of resources. *)
Class PlainP {M} (P : uPred M) := plainP : P ⊢ ⨳ P.
Arguments plainP {_} _ {_}.

Section naught_properties.
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). (* Force implicit argument M *)
Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)

(* naught primitive properties *)


Global Instance naught_ne n : Proper (dist n ==> dist n) (@uPred_naught M).
Proof.
  intros P1 P2 HP.
  rewrite uPred_naught_eq; split=> n' x; split; apply HP;
   eauto using @ucmra_unit_validN.
Qed.
Global Instance naught_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_naught M) := ne_proper _.

Lemma true_entails_naught P : (True ⊢ P) → (True ⊢ ⨳ P).
Proof.
  unseal; rewrite uPred_naught_eq; intros HP. split=>n x Hx HT.
  apply HP; last done; apply ucmra_unit_validN.
Qed.

Lemma naught_irrel P n x y : (⨳ P)%I n x → (⨳ P)%I n y.
Proof. by rewrite uPred_naught_eq. Qed.

Lemma naught_keeps_premises P Q : (P ⊢ ⨳ Q) → P ⊢ P ★ ⨳ Q.
Proof.
  intros HPQ. split=> n x Hx HPx. unseal.
  exists x, (∅ : M); repeat split; trivial; first by rewrite right_id.
  apply HPQ in HPx; last trivial. eauto using naught_irrel.
Qed.

Lemma naught_mono P Q : (P ⊢ Q) → ⨳ P ⊢ ⨳ Q.
Proof.
  intros HP; rewrite uPred_naught_eq; split=> n x ? /=.
  apply HP, ucmra_unit_validN.
Qed.
Lemma naught_elim P : ⨳ P ⊢ P.
Proof.
  rewrite uPred_naught_eq; split=> n x ? ? /=.
  by eapply uPred_mono; last eapply cmra_included_includedN, @ucmra_unit_least.
Qed.
Lemma naught_idemp P : ⨳ P ⊢ ⨳ ⨳ P.
Proof. by rewrite uPred_naught_eq. Qed.

Lemma naught_pure_2 φ : ■ φ ⊢ ⨳ ■ φ.
Proof. by unseal; rewrite uPred_naught_eq. Qed.

Lemma naught_implies_always P : ⨳ P ⊢ □ P.
Proof.
  unseal; rewrite uPred_naught_eq. split=> n x Hx.
  cbv [uPred_naught_def uPred_always_def uPred_holds]=> HP.
  eapply uPred_mono; eauto; apply ucmra_unit_leastN.
Qed.

Lemma naught_always_1 P : □ ⨳ P ⊢ ⨳ □ P.
Proof.
  unseal; rewrite uPred_naught_eq; split=> n x ? /=.
  cbv [uPred_naught_def uPred_always_def uPred_holds].
  by rewrite core_unit.
Qed.

Lemma naught_always_2 P : ⨳ □ P ⊢ □ ⨳ P.
Proof.
  unseal; rewrite uPred_naught_eq; split=> n x ? /=.
  cbv [uPred_naught_def uPred_always_def uPred_holds].
  by rewrite core_unit.
Qed.

Lemma naught_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ⨳ Ψ a) ⊢ (⨳ ∀ a, Ψ a).
Proof. by unseal; rewrite uPred_naught_eq. Qed.
Lemma naught_exist_1 {A} (Ψ : A → uPred M) : (⨳ ∃ a, Ψ a) ⊢ (∃ a, ⨳ Ψ a).
Proof. by unseal; rewrite uPred_naught_eq. Qed.

Lemma naught_and_sep_1 P Q : ⨳ (P ∧ Q) ⊢ ⨳ (P ★ Q).
Proof.
  unseal; rewrite uPred_naught_eq; split=> n x ? [??].
  exists (∅ : M), (∅ : M); rewrite left_id; auto.
Qed.

Lemma naught_and_sep_l_1 P Q : ⨳ P ∧ Q ⊢ ⨳ P ★ Q.
Proof.
  unseal; rewrite uPred_naught_eq; split=> n x ? [??]; exists ∅, x; simpl in *.
  by rewrite left_id.
Qed.

Lemma naught_later P : ⨳ ▷ P ⊣⊢ ▷ ⨳ P.
Proof. by unseal; rewrite uPred_naught_eq. Qed.

Lemma naught_ownM : ⨳ uPred_ownM ∅ ⊣⊢ uPred_ownM ∅. (* perhaps quite useless!? *)
Proof.
  intros; apply (anti_symm _); first by apply:naught_elim.
  unseal; rewrite uPred_naught_eq; split=> n x ? ?.
  by cbv [uPred_naught_def uPred_ownM_def uPred_holds].
Qed.

Lemma naught_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ⨳ ✓ a.
Proof. by unseal; rewrite uPred_naught_eq. Qed.

Hint Resolve pure_intro.
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.

(* Naught derived *)
Hint Resolve naught_mono naught_elim.
Global Instance naught_mono' : Proper ((⊢) ==> (⊢)) (@uPred_naught M).
Proof. intros P Q; apply naught_mono. Qed.
Global Instance naught_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@uPred_naught M).
Proof. intros P Q; apply naught_mono. Qed.

Lemma naught_intro' P Q : (⨳ P ⊢ Q) → ⨳ P ⊢ ⨳ Q.
Proof. intros <-. apply naught_idemp. Qed.

Lemma naught_pure φ : ⨳ ■ φ ⊣⊢ ■ φ.
Proof. apply (anti_symm _); auto using naught_pure_2. Qed.
Lemma naught_forall {A} (Ψ : A → uPred M) : (⨳ ∀ a, Ψ a) ⊣⊢ (∀ a, ⨳ Ψ a).
Proof.
  apply (anti_symm _); auto using naught_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma naught_exist {A} (Ψ : A → uPred M) : (⨳ ∃ a, Ψ a) ⊣⊢ (∃ a, ⨳ Ψ a).
Proof.
  apply (anti_symm _); auto using naught_exist_1.
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma naught_and P Q : ⨳ (P ∧ Q) ⊣⊢ ⨳ P ∧ ⨳ Q.
Proof. rewrite !and_alt naught_forall. by apply forall_proper=> -[]. Qed.
Lemma naught_or P Q : ⨳ (P ∨ Q) ⊣⊢ ⨳ P ∨ ⨳ Q.
Proof. rewrite !or_alt naught_exist. by apply exist_proper=> -[]. Qed.
Lemma naught_impl P Q : ⨳ (P → Q) ⊢ ⨳ P → ⨳ Q.
Proof.
  apply impl_intro_l; rewrite -naught_and.
  apply naught_mono, impl_elim with P; auto.
Qed.
Lemma naught_internal_eq {A:cofeT} (a b : A) : ⨳ (a ≡ b) ⊣⊢ a ≡ b.
Proof.
  apply (anti_symm (⊢)); auto using naught_elim.
  apply (internal_eq_rewrite a b (λ b, ⨳ (a ≡ b))%I); auto.
  { intros n; solve_proper. }
  rewrite -(internal_eq_refl a) naught_pure; auto.
Qed.

Lemma naught_always P : ⨳ □ P ⊣⊢ □ ⨳ P.
Proof.
  apply (anti_symm _); auto using naught_always_1, naught_always_2.
Qed.

Lemma naught_and_sep P Q : ⨳ (P ∧ Q) ⊣⊢ ⨳ (P ★ Q).
Proof.
  apply (anti_symm (⊢)); last rewrite sep_and; auto using naught_and_sep_1.
Qed.
Lemma naught_and_sep_l' P Q : ⨳ P ∧ Q ⊣⊢ ⨳ P ★ Q.
Proof.
  apply (anti_symm (⊢)); last rewrite sep_and; auto using naught_and_sep_l_1.
Qed.
Lemma naught_and_sep_r' P Q : P ∧ ⨳ Q ⊣⊢ P ★ ⨳ Q.
Proof. by rewrite !(comm _ P) naught_and_sep_l'. Qed.
Lemma naught_sep P Q : ⨳ (P ★ Q) ⊣⊢ ⨳ P ★ ⨳ Q.
Proof. by rewrite -naught_and_sep -naught_and_sep_l' naught_and. Qed.
Lemma naught_sep_dup' P : ⨳ P ⊣⊢ ⨳ P ★ ⨳ P.
Proof. by rewrite -naught_sep -naught_and_sep (idemp _). Qed.

Lemma naught_wand P Q : ⨳ (P -★ Q) ⊢ ⨳ P -★ ⨳ Q.
Proof. by apply wand_intro_r; rewrite -naught_sep wand_elim_l. Qed.
Lemma naught_wand_impl P Q : ⨳ (P -★ Q) ⊣⊢ ⨳ (P → Q).
Proof.
  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
  apply naught_intro', impl_intro_r.
  by rewrite naught_and_sep_l' naught_elim wand_elim_l.
Qed.
Lemma naught_entails_l' P Q : (P ⊢ ⨳ Q) → P ⊢ ⨳ Q ★ P.
Proof. intros; rewrite -naught_and_sep_l'; auto. Qed.
Lemma naught_entails_r' P Q : (P ⊢ ⨳ Q) → P ⊢ P ★ ⨳ Q.
Proof. intros; rewrite -naught_and_sep_r'; auto. Qed.


Lemma except_0_naught P : ◇ ⨳ P ⊣⊢ ⨳ ◇ P.
Proof. by rewrite /uPred_except_0 naught_or naught_later naught_pure. Qed.

Lemma naught_cmra_valid {A : cmraT} (a : A) : ⨳ ✓ a ⊣⊢ ✓ a.
Proof.
  intros; apply (anti_symm _); first by apply:naught_elim.
  apply:naught_cmra_valid_1.
Qed.

(* Plainness *)
Global Instance pure_plain φ : PlainP (■ φ : uPred M)%I.
Proof. by rewrite /PlainP naught_pure. Qed.
Global Instance naught_plain P : PlainP (⨳ P).
Proof. by intros; apply naught_intro'. Qed.
Global Instance and_plain P Q :
  PlainP P → PlainP Q → PlainP (P ∧ Q).
Proof. by intros; rewrite /PlainP naught_and; apply and_mono. Qed.
Global Instance or_plain P Q :
  PlainP P → PlainP Q → PlainP (P ∨ Q).
Proof. by intros; rewrite /PlainP naught_or; apply or_mono. Qed.
Global Instance sep_plain P Q :
  PlainP P → PlainP Q → PlainP (P ★ Q).
Proof. by intros; rewrite /PlainP naught_sep; apply sep_mono. Qed.
Global Instance forall_plain {A} (Ψ : A → uPred M) :
  (∀ x, PlainP (Ψ x)) → PlainP (∀ x, Ψ x).
Proof. by intros; rewrite /PlainP naught_forall; apply forall_mono. Qed.
Global Instance exist_plain {A} (Ψ : A → uPred M) :
  (∀ x, PlainP (Ψ x)) → PlainP (∃ x, Ψ x).
Proof. by intros; rewrite /PlainP naught_exist; apply exist_mono. Qed.
Global Instance internal_eq_plain {A : cofeT} (a b : A) :
  PlainP (a ≡ b : uPred M)%I.
Proof. by intros; rewrite /PlainP naught_internal_eq. Qed.
Global Instance cmra_valid_plain {A : cmraT} (a : A) :
  PlainP (✓ a : uPred M)%I.
Proof. by intros; rewrite /PlainP naught_cmra_valid. Qed.
Global Instance later_plain P : PlainP P → PlainP (▷ P).
Proof. by intros; rewrite /PlainP naught_later; apply later_mono. Qed.
Global Instance ownM_plain : PlainP (@uPred_ownM M ∅). (* perhaps quite useless!? *)
Proof. intros. by rewrite /PlainP naught_ownM. Qed.
Global Instance from_option_plain {A} P (Ψ : A → uPred M) (mx : option A) :
  (∀ x, PlainP (Ψ x)) → PlainP P → PlainP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
Global Instance except_0_plain P : PlainP P → PlainP (◇ P).
Proof. intros; by rewrite /PlainP -except_0_naught except_0_mono. Qed.

(* Plainness implies persistence *)
Global Instance plain_persistent P : PlainP P → PersistentP P.
Proof.
 rewrite /PlainP /PersistentP => HP.
 by etrans; last apply naught_implies_always.
Qed.

(* Derived lemmas for plainness *)
Lemma naught_naught P `{!PlainP P} : ⨳ P ⊣⊢ P.
Proof. apply (anti_symm (⊢)); auto. Qed.
Lemma naught_intro P Q `{!PlainP P} : (P ⊢ Q) → P ⊢ ⨳ Q.
Proof. rewrite -(naught_naught P); apply naught_intro'. Qed.
Lemma naught_and_sep_l P Q `{!PlainP P} : P ∧ Q ⊣⊢ P ★ Q.
Proof. by rewrite -(naught_naught P) naught_and_sep_l'. Qed.
Lemma naught_and_sep_r P Q `{!PlainP Q} : P ∧ Q ⊣⊢ P ★ Q.
Proof. by rewrite -(naught_naught Q) naught_and_sep_r'. Qed.
Lemma naught_sep_dup P `{!PlainP P} : P ⊣⊢ P ★ P.
Proof. by rewrite -(naught_naught P) -naught_sep_dup'. Qed.
Lemma naught_entails_l P Q `{!PlainP Q} : (P ⊢ Q) → P ⊢ Q ★ P.
Proof. by rewrite -(naught_naught Q); apply naught_entails_l'. Qed.
Lemma naught_entails_r P Q `{!PlainP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
Proof. by rewrite -(naught_naught Q); apply naught_entails_r'. Qed.

(* important for proving properties in the model. *)
Lemma naught_irrel' P `{HPl: !PlainP P} n x y : ✓{n} x → ✓{n} y → P n x → P n y.
Proof.
 intros Hx Hy Hnx; apply HPl in Hnx; last done.
 apply naught_elim; first done. eapply naught_irrel; eauto.
Qed.

Lemma naught_keeps_premises' P Q `{HPl: !PlainP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
Proof.
  iIntros (HPQ) "HP".
  assert (HPQ': P ⊢ ⨳ Q) by (by iIntros "HP"; iApply HPl; iApply HPQ).
  iPoseProof (naught_keeps_premises _ _ HPQ' with "HP") as "HPQ".
  iDestruct "HPQ" as "[HP HQ]"; iSplitL "HP"; first trivial.
  by iApply naught_elim.
Qed.

Global Instance iter_Plain_Plain P `{Hpl: !PlainP P} n f :
  (∀ Q, PlainP Q -> PlainP (f Q)) →
  PlainP (Nat.iter n f P).
Proof.
  revert P Hpl. induction n => P Hpl; first done.
  rewrite Nat_iter_S_r; auto.
Qed.

End naught_properties.

Lemma bupd_extract_plain {M : ucmraT} (P Q : uPred M) `{!PlainP P} :
  (Q ⊢ P) → (|==> Q) ⊢ P.
Proof.
  intros HQP; unseal; split=> n x Hnx Hbp.
  destruct (Hbp n ∅ (le_n _)) as [z [Hz1 Hz2]]; first by rewrite right_id.
  revert Hz1; rewrite right_id=> Hz1.
  apply HQP in Hz2; trivial. eauto using naught_irrel', ucmra_unit_validN.
Qed.

(* future modality *)
Program Definition future_def `{invG Σ}
    (E : coPset) n (P : iProp Σ) : iProp Σ :=
  (Nat.iter n (λ Q, (|={E}=> ▷ Q)) (|={E}=> P))%I.
Definition future_aux : { x | x = @future_def }. by eexists. Qed.
Definition future := proj1_sig future_aux.
Definition future_eq : @future = @future_def := proj2_sig future_aux.
Arguments future {_ _} _ _ _%I.
Instance: Params (@fupd) 4.

Notation "|≫{ E }=[ n ]=> Q" := (future E n Q)
  (at level 99, E at level 50, Q at level 200,
   format "|≫{ E }=[ n ]=>  Q") : uPred_scope.
Notation "P ≫{ E }=[ n ]=★ Q" := (P -★ |≫{E}=[n]=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ≫{ E }=[ n ]=★  Q") : uPred_scope.
Notation "P ≫{ E }=[ n ]=★ Q" := (P ⊢ |≫{E}=[n]=> Q)
  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.

Lemma future_unfold `{invG Σ} (E : coPset) n (P : iProp Σ) :
  (|≫{E}=[n]=> P) ⊣⊢
  (match n with
   | O => |={E}=> P
   | S n => (Nat.iter (S n) (λ Q, (|={E}=> ▷ Q)) (|={E}=> P))
   end).
Proof.
  rewrite future_eq. destruct n; trivial.
Qed.

Lemma future_unfold_O `{invG Σ} (E : coPset) (P : iProp Σ) :
  (|≫{E}=[0]=> P) ⊣⊢ |={E}=> P.
Proof. by rewrite future_unfold. Qed.

Lemma future_unfold_S `{invG Σ} (E : coPset) n (P : iProp Σ) :
  (|≫{E}=[S n]=> P) ⊣⊢ (Nat.iter (S n) (λ Q, (|={E}=> ▷ Q)) (|={E}=> P)).
Proof. by rewrite future_unfold. Qed.

Section fupd_and_plain.
 Context `{invG Σ}.

 Lemma fupd_extract_plain {E1 E2} P Q `{!PlainP P} :
  (Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ★ P).
 Proof.
  intros HQP. rewrite fupd_eq /fupd_def; unseal.
  split => n x Hx Hfp k x' Hkn Hxx' Hwo.
  destruct (Hfp k x' Hkn Hxx' Hwo k ∅ (le_n _)) as [z [Hz1 Hz2]];
   first by rewrite right_id.
  assert (Hz1' : ✓{k} (z)) by (by revert Hz1; rewrite right_id).
  assert (HP : (◇ P)%I k ∅).
  { rewrite -uPred_sep_eq in Hz2. apply except_0_sep' in Hz2; last done.
    rewrite uPred_sep_eq in Hz2. destruct Hz2 as (z1 & z2 & Hz & _ & Hz2).
    rewrite -uPred_sep_eq in Hz2.
    assert (Hz2vl : ✓{k} z2) by (revert Hz1'; rewrite Hz;
      eauto using cmra_validN_op_l, cmra_validN_op_r).
    apply except_0_sep' in Hz2; last done.
   rewrite uPred_sep_eq in Hz2. destruct Hz2 as (w1 & w2 & Hw & _ & Hz2).
   assert (Hw2vl : ✓{k} w2) by (revert Hz2vl; rewrite Hw;
     eauto using cmra_validN_op_l, cmra_validN_op_r).
   eapply (naught_irrel' _ _ w2); auto using ucmra_unit_validN.
   by eapply (except_0_mono _ _ HQP). }
  intros m yf Hmk Hxx'yf. exists (x ⋅ x'); split; auto.
  destruct Hwo as (u1 & u2 & Hu & Hu1 & Hu2).
  rewrite -uPred_sep_eq; apply except_0_sep; first eauto using cmra_validN_le.
  rewrite uPred_sep_eq.
  exists u1, (x ⋅ u2); split;
   first by rewrite (comm _ u1) -assoc (dist_le _ _ _ _ Hu) // (comm _ u1).
  split.
  { assert (✓{m} u1) by
    (revert Hxx'; rewrite Hu=> Hxx';
      eapply cmra_validN_op_l, cmra_validN_op_r, cmra_validN_le; eauto).
    apply except_0_intro; last eapply uPred_closed; eauto. }
  assert (✓{m} (x ⋅ u2)) by
    (revert Hxx'; rewrite Hu=> Hxx';
      eapply cmra_validN_op_l; rewrite -assoc (comm _ u2);
      eapply cmra_validN_le; eauto).
  rewrite -uPred_sep_eq; apply except_0_sep; first done. rewrite uPred_sep_eq.
  exists u2, x; split; first by rewrite (comm _ u2).
  split.
  { assert (✓{m} u2) by eauto using cmra_validN_op_r.
    apply except_0_intro; last eapply uPred_closed; eauto. }
  rewrite -uPred_sep_eq. apply except_0_sep; first eauto using cmra_validN_op_l.
  rewrite uPred_sep_eq.
  exists x, (∅ : iResUR Σ); split; first by rewrite right_id.
  split.
  { apply except_0_intro; first eauto using cmra_validN_op_l.
    eapply uPred_closed; eauto; last eauto using cmra_validN_op_l. omega. }
  eapply uPred_closed; eauto using ucmra_unit_validN.
 Qed.

 Lemma later_fupd_plain {E} P `{Hpl: !PlainP P} :
   (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
 Proof.
  rewrite fupd_eq /fupd_def later_wand; unseal.
  split=> n x Hx Hfp k x' Hkn Hxx' Hwo.
  pose proof (Hwo) as Hwo'; apply later_intro in Hwo';
    last eauto using cmra_validN_op_r; rewrite uPred_later_eq in Hwo'.
  specialize (Hfp k x' Hkn Hxx' Hwo').
  assert (HP : (▷ ◇ P)%I k x).
  { eapply (naught_irrel' _ _ (x ⋅ x')); eauto using cmra_validN_op_l.
    eapply later_mono; last (rewrite uPred_later_eq; apply Hfp); trivial.
    rewrite -uPred_bupd_eq; apply bupd_extract_plain; first typeclasses eauto.
    apply except_0_mono; rewrite -uPred_sep_eq; by iIntros "(_&_&?)".
  }
  rewrite -uPred_bupd_eq; apply bupd_intro; trivial.
  rewrite -uPred_sep_eq -uPred_later_eq. rewrite -uPred_sep_eq in Hwo.
  apply except_0_intro; trivial.
  apply sep_assoc'; trivial.
  rewrite {1}uPred_sep_eq; eexists x', x.
  repeat split; trivial; by rewrite (comm _ x).
 Qed.

 Lemma step_Sn_fupd_mono {E} P Q n :
   (P ⊢ Q) →
   Nat.iter n (λ Q : iProp Σ, |={E}=> ▷ Q) P ⊢
   Nat.iter n (λ Q : iProp Σ, |={E}=> ▷ Q) Q.
 Proof.
  revert P Q; induction n=> P Q HPQ; first done.
  rewrite !Nat_iter_S_r; apply IHn. iIntros "HP".
  iMod "HP"; iModIntro; iNext; by iApply HPQ.
 Qed.

 Lemma future_plain_base {E} P `{Hpl: !PlainP P} n :
   (Nat.iter (S n) (λ Q, (|={E}=> ▷ Q)) (|={E}=> P)) ⊢
   |={E}=> Nat.iter (S n) (λ Q, ▷ ◇ Q) P.
 Proof.
  revert P Hpl. induction n=> P Hpl.
  - simpl. iIntros "HP"; iMod "HP"; by iApply later_fupd_plain.
  - rewrite !(Nat_iter_S_r (S n)). iIntros "Hfpn".
    iApply IHn. iApply step_Sn_fupd_mono; last trivial.
    iIntros "HP"; iMod "HP"; by iApply later_fupd_plain.
 Qed.

 Lemma later_n_mono {M} P Q n :
  (P ⊢ Q) → Nat.iter n (λ Q : uPred M, ▷ Q) P ⊢ Nat.iter n (λ Q, ▷ Q) Q.
 Proof.
   revert P Q; induction n=> P Q HPQ; first trivial.
   rewrite !Nat_iter_S_r. by apply IHn, later_mono.
 Qed.

 Lemma later_except_0_n {M} P n :
   Nat.iter (S n) (λ Q : uPred M, ▷ ◇ Q) P ⊢ Nat.iter (S n) (λ Q, ▷ Q) (◇ P)%I.
 Proof.
  revert P; induction n=> P; first trivial.
  rewrite !(Nat_iter_S_r (S n)). iIntros "Hfpn".
  iPoseProof (IHn with "Hfpn") as "Hfpn".
  iApply later_n_mono; last trivial.
  apply except_0_later.
 Qed.

  Lemma fupd_plain_forall_comm {E1 E2} (A :Type) (P : A → iProp Σ)
   `{Hpl: ∀ x, PlainP (P x)} :
  (∀ x : A, (|={E1,E2}=> P x))%I ⊢ |={E1}=> (∀ x : A, P x).
  Proof.
  rewrite fupd_eq /fupd_def; unseal.
  split=> n x Hx Hfp k x' Hkn Hxx' Hwo k' yf Hkk' Hxx'yf.
  exists (x ⋅ x'); split; first trivial.
  assert (Hk'xx' : ✓{k'} (x ⋅ x')) by eauto using cmra_validN_le.
  rewrite -uPred_sep_eq. rewrite -uPred_sep_eq in Hwo.
  eapply except_0_mono; first apply sep_assoc';
    last apply except_0_frame_l; trivial.
  rewrite {1}uPred_sep_eq; eexists x', x; repeat split; first by rewrite comm.
  eapply uPred_closed; eauto using cmra_validN_op_r.
  rewrite uPred_sep_eq in Hwo.
  rewrite -uPred_forall_eq; apply except_0_forall; eauto using cmra_validN_op_l.
  rewrite uPred_forall_eq => u.
  destruct (Hfp u k x' Hkn Hxx' Hwo k ∅ (le_n _)) as [z [Hz1 Hz2]];
    first by rewrite right_id.
  assert (✓{k} z) by (by revert Hz1; rewrite right_id).
  eapply (naught_irrel' _ _ z); eauto using cmra_validN_op_l, cmra_validN_le.
  eapply except_0_mono; last (eapply uPred_closed; first eapply Hz2);
    eauto using cmra_validN_le.
  rewrite -uPred_sep_eq; iIntros "(_ & _ & ?)"; iFrame.
 Qed.

 Lemma future_S {E} P n : (|≫{E}=[S n]=> P) ⊣⊢ |={E}=> ▷ (|≫{E}=[n]=> P).
 Proof. by rewrite !future_eq. Qed.

 Lemma future_mono {E} Q P n :
  (Q ⊢ P) → (|≫{E}=[n]=> Q) ⊢ (|≫{E}=[n]=> P).
  Proof.
    revert Q P; induction n => Q P HQP.
    - by rewrite !future_unfold_O; apply fupd_mono.
    - rewrite !future_S; auto using fupd_mono, later_mono.
  Qed.

 Lemma future_plain {E} P `{Hpl: !PlainP P} n :
   (|≫{E}=[n]=> P) ⊢ |={E}=> Nat.iter n (λ Q, ▷ Q) (◇ P).
 Proof.
   rewrite future_unfold; destruct n; iIntros "HP".
   - by iMod "HP"; iModIntro; iApply except_0_intro.
   - iPoseProof (future_plain_base with "HP") as "HP".
     iMod "HP"; iModIntro; by iApply later_except_0_n.
 Qed.

 Lemma future_plain'_base {E} Q P `{Hpl: !PlainP P} n :
   (Q ⊢ P) → (|≫{E}=[n]=> Q) ⊢ |={E}=> Nat.iter n (λ Q, ▷ Q) (◇ P).
 Proof.
  iIntros (HQP) "HQ". iApply future_plain. iApply future_mono; eauto.
 Qed.

 Lemma future_plain' {E} Q P `{Hpl: !PlainP P} n :
   (Q ⊢ P) →
   (|≫{E}=[n]=> Q) ⊢ |={E}=> (|≫{E}=[n]=> Q) ★ (Nat.iter n (λ Q, ▷ Q) (◇ P)).
 Proof.
   intros HQP.
   split => k x Hx HQ.
   pose proof (HQ) as HP; apply (future_plain'_base _ _ _ HQP) in HP; auto.
   revert HP; rewrite fupd_eq /fupd_def; unseal => HP.
   intros k' x' Hkk' Hxx' Hwo k'' yf Hk'k'' Hxx'yf.
   destruct (HP k' x' Hkk' Hxx' Hwo k'' yf Hk'k'' Hxx'yf) as [u [Hvu Hu]].
   rewrite -uPred_sep_eq in Hu.
   assert (Hvu' : ✓{k''} u) by eauto using cmra_validN_op_l.
   do 2 (apply except_0_sep' in Hu; trivial; apply sep_elim_r in Hu; trivial).
   exists (x ⋅ x'); split; trivial.
   assert (Hk'xx' : ✓{k''} (x ⋅ x')) by eauto using cmra_validN_le.
   rewrite -uPred_sep_eq. rewrite -uPred_sep_eq in Hwo.
   eapply except_0_mono; first apply sep_assoc';
    last apply except_0_frame_l; trivial.
   rewrite {1}uPred_sep_eq; eexists x', x; repeat split; first by rewrite comm.
   eapply uPred_closed; eauto using cmra_validN_op_r.
   rewrite uPred_sep_eq in Hwo.
   apply except_0_frame_l; eauto using cmra_validN_op_l.
   rewrite uPred_sep_eq. exists x, (∅ : iResUR Σ); split; first by rewrite right_id.
   split; first (eapply uPred_closed; first apply HQ);
     try omega; eauto using cmra_validN_op_l.
   rewrite -uPred_later_eq; rewrite -uPred_later_eq in Hu.
   (eapply (naught_irrel' _ _ _ ∅) in Hu); eauto using ucmra_unit_validN.
 Qed.

 Lemma later_n_except_0_future {E} P n :
   Nat.iter n (λ Q, ▷ Q) (◇ P) ⊢ (|≫{E}=[n]=> P).
 Proof.
  rewrite future_eq; induction n; simpl.
  - by iIntros "HP"; iMod "HP"; iModIntro.
  - by iIntros "HP"; iModIntro; iNext; iApply IHn.
 Qed.

 Lemma future_sep {E} P Q n :
  (|≫{E}=[n]=> P) ★ (|≫{E}=[n]=> Q) ⊢ (|≫{E}=[n]=> P ★ Q).
 Proof.
  rewrite future_eq; induction n; simpl.
  - iIntros "[HP HQ]"; iMod "HP"; iMod "HQ"; iModIntro; iFrame.
  - iIntros "[HP HQ]";iMod "HP"; iMod "HQ"; iModIntro; iNext; iApply IHn; iFrame.
 Qed.

 Lemma future_cancel_2 {E} P Q Q' m n :
  ((|≫{E}=[m - n]=> P) ★ Q ⊢ Q') →
  (|≫{E}=[m]=> P) ★ (|≫{E}=[n]=> Q) ⊢ (|≫{E}=[n]=> Q').
 Proof.
  revert m; induction n => m; simpl.
  - replace (m - 0) with m by omega. intros HA.
    iIntros "[HP HQ]". rewrite !future_unfold_O.
    iMod "HQ"; iModIntro; iApply HA; iFrame.
  - destruct m.
    + replace (0 - S n) with (0 - n) by omega. intros HB; specialize (IHn _ HB).
      iIntros "[HP HQ]"; rewrite !future_S. iMod "HQ"; iModIntro; iNext.
      iApply IHn; iFrame.
    + replace (S m - S n) with (m - n) by omega.
      intros HB; specialize (IHn _ HB).
      iIntros "[HP HQ]"; rewrite !future_S. iMod "HP"; iMod "HQ"; iModIntro; iNext.
      iApply IHn; iFrame.
 Qed.

End fupd_and_plain.