(* iris/proofmode/class_instances_updates.v *)
From stdpp Require Import nat_cancel
From iris.bi Require Import bi
From iris.proofmode Require Import modality_instances classes
From iris.proofmode Require Import ltac_tactics class_instances
From iris.prelude Require Import options
FromAssumption p P Q → KnownRFromAssumption p P (|==> Q)
FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q)
FromPure a P φ → FromPure a (|==> P) φ
FromPure a P φ → FromPure a (|={E}=> P) φ
FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2)
FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2)
FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2)
FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2)
FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I
FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I
FromForall P Φ name → (∀ x, Plain (Φ x)) →
FromForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> (Φ a))%I name
FromForall P Φ name → (∀ x, Plain (Φ x)) →
FromForall (|={E1}[E2]▷=> P) (λ a, |={E1}[E2]▷=> (Φ a))%I name
FromModal True modality_id (|==> P) (|==> P) P
FromModal True modality_id (|={E}=> P) (|={E}=> P) P
FromModal

Global Instancefrom_assumption_bupd `{!BiBUpd PROP} p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.

Global Instancefrom_assumption_fupd
    `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} E p P Q :
  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.

Global Instancefrom_pure_bupd `{!BiBUpd PROP} a P φ :
  FromPure a P φ → FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.

Global Instancefrom_pure_fupd `{!BiFUpd PROP} a E P φ :
  FromPure a P φ → FromPure a (|={E}=> P) φ.
Proof. rewrite /FromPure=> <-. apply fupd_intro. Qed.

Global Instanceinto_wand_bupd `{!BiBUpd PROP} p q R P Q :
  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.

Global Instanceinto_wand_fupd `{!BiFUpd PROP} E p q R P Q :
  IntoWand false false R P Q →
  IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
Qed.

Global Instanceinto_wand_bupd_persistent `{!BiBUpd PROP} p q R P Q :
  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.

Global Instanceinto_wand_fupd_persistent `{!BiFUpd PROP} E1 E2 p q R P Q :
  IntoWand false q R P Q → IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
Qed.

Global Instanceinto_wand_bupd_args `{!BiBUpd PROP} p q R P Q :
  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite intuitionistically_if_elim bupd_wand_r.
Qed.

Global Instanceinto_wand_fupd_args `{!BiFUpd PROP} E1 E2 p q R P Q :
  IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite intuitionistically_if_elim fupd_wand_r.
Qed.

Global Instancefrom_sep_bupd `{!BiBUpd PROP} P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.

Global Instancefrom_sep_fupd `{!BiFUpd PROP} E P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.

Global Instancefrom_or_bupd `{!BiBUpd PROP} P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromOr=><-. apply bupd_or. Qed.

Global Instancefrom_or_fupd `{!BiFUpd PROP} E1 E2 P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply fupd_or. Qed.

Global Instanceinto_and_bupd `{!BiBUpd PROP} P Q1 Q2 :
  IntoAnd false P Q1 Q2 → IntoAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /IntoAnd/==>->. apply bupd_and. Qed.

Global Instanceinto_and_fupd `{!BiFUpd PROP} E1 E2 P Q1 Q2 :
  IntoAnd false P Q1 Q2 → IntoAnd false (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /IntoAnd/==>->. apply fupd_and. Qed.

Global Instancefrom_exist_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof. rewrite /FromExist=><-. apply bupd_exist. Qed.

Global Instancefrom_exist_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
  FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof. rewrite /FromExist=><-. apply fupd_exist. Qed.

Global Instanceinto_forall_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (|==> P) (λ a, |==> Φ a)%I.
Proof. rewrite /IntoForall=>->. apply bupd_forall. Qed.

Global Instanceinto_forall_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof. rewrite /IntoForall=>->. apply fupd_forall. Qed.

Global Instancefrom_forall_fupd
    `{!BiFUpd PROP, !Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}
    E1 E2 {A} P (Φ : A → PROP) name :

Global Instancefrom_forall_step_fupd
    `{!BiFUpd PROP, !Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}
    E1 E2 {A} P (Φ : A → PROP) name :

Global Instanceis_except_0_bupd `{!BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P).
Proof.
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed.

Global Instanceis_except_0_fupd `{!BiFUpd PROP} E1 E2 P :
  IsExcept0 (|={E1,E2}=> P).
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.

Global Instancefrom_modal_bupd `{!BiBUpd PROP} P :
  FromModal True modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.

Global Instancefrom_modal_fupd E P `{!BiFUpd PROP} :
  FromModal True modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.

Global Instancefrom_modal_fupd_wrong_mask E1 E2 P `{!BiFUpd PROP} :
  FromModal
        (pm_error "Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities")
    modality_id (|={E1,E2}=> P) (|={E1,E2}=> P) P | 100.
Proof. by intros []. Qed.

Global Instanceelim_modal_bupd `{!BiBUpd PROP} p P Q :
  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
  by rewrite /ElimModal
    intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
Qed.

Global Instanceelim_modal_bupd_plain_goal
    `{!BiBUpd PROP, !Sbi PROP, !BiBUpdSbi PROP, !BiAffine PROP} p P Q :
  Plain Q → ElimModal True p false (|==> P) P Q Q.
Proof.
  intros. by rewrite /ElimModal intuitionistically_if_elim
    bupd_frame_r wand_elim_r bupd_elim.
Qed.

Global Instanceelim_modal_bupd_plain
    `{!BiBUpd PROP, !Sbi PROP, !BiBUpdSbi PROP, !BiAffine PROP} p P Q :
  Plain P → ElimModal True p p (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_elim wand_elim_r. Qed.

Global Instanceelim_modal_bupd_fupd
    `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} p E1 E2 P Q :
  ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof.
  by rewrite /ElimModal intuitionistically_if_elim
    (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.

Global Instanceelim_modal_fupd_fupd `{!BiFUpd PROP} p E1 E2 E3 P Q :
  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof.
  by rewrite /ElimModal intuitionistically_if_elim
    fupd_frame_r wand_elim_r fupd_trans.
Qed.

Global Instanceelim_modal_fupd_fupd_wrong_mask `{!BiFUpd PROP} p E0 E1 E2 E3 P Q :
  ElimModal
    (pm_error "Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
    p false
    (|={E1,E2}=> P) False (|={E0,E3}=> Q) False | 100.
Proof. intros []. Qed.

Global Instanceadd_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.

Global Instanceadd_modal_fupd `{!BiFUpd PROP} E1 E2 P Q :
  AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.

Global Instanceelim_acc_bupd `{!BiBUpd PROP} {X} α β mγ Q :
  ElimAcc (X:=X) True bupd bupd α β mγ
          (|==> Q)
          (λ x, |==> β x ∗ (mγ x -∗? |==> Q))%I.
Proof.
  iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
Qed.

Global Instanceelim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
  ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β mγ
          (|={E1,E}=> Q)
          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
Proof.
  iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
Qed.