Library iris.proofmode.class_instances_plainly

From iris.bi Require Import bi.
From iris.proofmode Require Import modality_instances classes.
From iris.prelude Require Import options.
Import bi.

Section class_instances_plainly.
Context {PROP} `{!BiPlainly PROP}.
Implicit Types P Q R : PROP.

Global Instance from_assumption_plainly_l_true P Q :
  FromAssumption true P Q → KnownLFromAssumption true (■ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite intuitionistically_plainly_elim //.
Qed.
Global Instance from_assumption_plainly_l_false `{!BiAffine PROP} P Q :
  FromAssumption true P Q → KnownLFromAssumption false (■ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite plainly_elim_persistently intuitionistically_into_persistently //.
Qed.

Global Instance from_pure_plainly P φ :
  FromPure false P φ → FromPure false (■ P) φ.
Proof. rewrite /FromPure⇒ <-. by rewrite plainly_pure. Qed.

Global Instance into_pure_plainly P φ :
  IntoPure P φ → IntoPure (■ P) φ.
Proof. rewrite /IntoPure⇒ →. apply: plainly_elim. Qed.

Global Instance into_wand_plainly_true q R P Q :
  IntoWand true q R P Q → IntoWand true q (■ R) P Q.
Proof. rewrite /IntoWand /= intuitionistically_plainly_elim //. Qed.
Global Instance into_wand_plainly_false q R P Q :
  Absorbing R → IntoWand false q R P Q → IntoWand false q (■ R) P Q.
Proof. intros ?. by rewrite /IntoWand plainly_elim. Qed.

Global Instance from_and_plainly P Q1 Q2 :
  FromAnd P Q1 Q2 → FromAnd (■ P) (■ Q1) (■ Q2).
Proof. rewrite /FromAnd⇒ <-. by rewrite plainly_and. Qed.

Global Instance from_sep_plainly P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite plainly_sep_2. Qed.

Global Instance into_and_plainly p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
Proof.
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -plainly_and -[(□ ■ P)%I]intuitionistically_idemp intuitionistically_plainly =>->.
    rewrite [(□ (_ ∧ _))%I]intuitionistically_elim //.
  - intros →. by rewrite plainly_and.
Qed.

Global Instance into_sep_plainly `{!BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
Proof. rewrite /IntoSep /= ⇒ →. by rewrite plainly_sep. Qed.
Global Instance into_sep_plainly_affine P Q1 Q2 :
  IntoSep P Q1 Q2 →
  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
  IntoSep (■ P) (■ Q1) (■ Q2).
Proof.
  rewrite /IntoSep /= ⇒ → ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
Qed.

Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
Proof. rewrite /FromOr⇒ <-. by rewrite -plainly_or_2. Qed.

Global Instance into_or_plainly `{!BiPlainlyExist PROP} P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.

Global Instance from_exist_plainly {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
Proof. rewrite /FromExist⇒ <-. by rewrite -plainly_exist_2. Qed.

Global Instance into_exist_plainly `{!BiPlainlyExist PROP} {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (■ P) (λ a, ■ (Φ a))%I name.
Proof. rewrite /IntoExist⇒ HP. by rewrite HP plainly_exist. Qed.

Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
Proof. rewrite /IntoForall⇒ HP. by rewrite HP plainly_forall. Qed.

Global Instance from_forall_plainly {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall (■ P) (λ a, ■ (Φ a))%I name.
Proof. rewrite /FromForall⇒ <-. by rewrite plainly_forall. Qed.

Global Instance from_modal_plainly P :
  FromModal True modality_plainly (■ P) (■ P) P | 2.
Proof. by rewrite /FromModal. Qed.

Global Instance into_except_0_plainly `{!BiPlainlyExist PROP} P Q :
  IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
Proof. rewrite /IntoExcept0⇒ →. by rewrite except_0_plainly. Qed.

Global Instance into_later_plainly n P Q :
  IntoLaterN false n P Q → IntoLaterN false n (■ P) (■ Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN⇒ →. by rewrite laterN_plainly. Qed.
End class_instances_plainly.