Library iris.proofmode.class_instances_updates

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.
Import bi.

Section class_instances_updates.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

Global Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
  FromAssumption p P Q KnownRFromAssumption p P (|==> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
Global Instance from_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 Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
  FromPure a P φ FromPure a (|==> P) φ.
Proof. rewrite /FromPure⇒ <-. apply bupd_intro. Qed.
Global Instance from_pure_fupd `{!BiFUpd PROP} a E P φ :
  FromPure a P φ FromPure a (|={E}=> P) φ.
Proof. rewrite /FromPure⇒ <-. apply fupd_intro. Qed.

Global Instance into_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 Instance into_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 Instance into_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 Instance into_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 Instance into_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 Instance into_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 Instance from_sep_bupd `{!BiBUpd PROP} P Q1 Q2 :
  FromSep P Q1 Q2 FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
Global Instance from_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 Instance from_or_bupd `{!BiBUpd PROP} P Q1 Q2 :
  FromOr P Q1 Q2 FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromOr=><-. apply bupd_or. Qed.
Global Instance from_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 Instance into_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 Instance into_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 Instance from_exist_bupd `{!BiBUpd PROP} {A} P (Φ : A PROP) :
  FromExist P Φ FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof. rewrite /FromExist=><-. apply bupd_exist. Qed.
Global Instance from_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 Instance into_forall_bupd `{!BiBUpd PROP} {A} P (Φ : A PROP) :
  IntoForall P Φ IntoForall (|==> P) (λ a, |==> Φ a)%I.
Proof. rewrite /IntoForall=>->. apply bupd_forall. Qed.
Global Instance into_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 Instance from_forall_fupd
    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A PROP) name :
  
  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ) (TCEq E2 ))
  FromForall P Φ name ( x, Plain (Φ x))
  FromForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> (Φ a))%I name.
Proof.
  rewrite /FromForall⇒ -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
Qed.
Global Instance from_forall_step_fupd
    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A PROP) name :
  
  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ) (TCEq E2 ))
  FromForall P Φ name ( x, Plain (Φ x))
  FromForall (|={E1}[E2]▷=> P) (λ a, |={E1}[E2]▷=> (Φ a))%I name.
Proof.
  rewrite /FromForall⇒ -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
Qed.

Global Instance is_except_0_bupd `{!BiBUpd PROP} P : IsExcept0 P IsExcept0 (|==> P).
Proof.
  rewrite /IsExcept0HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed.
Global Instance is_except_0_fupd `{!BiFUpd PROP} E1 E2 P :
  IsExcept0 (|={E1,E2}=> P).
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.

Global Instance from_modal_bupd `{!BiBUpd PROP} P :
  FromModal True modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.
Global Instance from_modal_fupd E P `{!BiFUpd PROP} :
  FromModal True modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.
Global Instance from_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 Instance elim_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 Instance elim_modal_bupd_plain_goal
    `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly 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 Instance elim_modal_bupd_plain
    `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly 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 Instance elim_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 Instance elim_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 Instance elim_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 Instance add_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.

Global Instance add_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 Instance elim_acc_bupd `{!BiBUpd PROP} {X} α β Q :
  ElimAcc (X:=X) True bupd bupd α β
          (|==> Q)
          (λ x, |==> β x ( 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 Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β Q :
  ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β
          (|={E1,E}=> Q)
          (λ x, |={E2}=> β x ( 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.
End class_instances_updates.