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 `{!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 (Absorbing Q1) (Affine Q2)
  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 /IntoExistHP. by rewrite HP plainly_exist. Qed.

Global Instance into_forall_plainly {A} P (Φ : A PROP) :
  IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForallHP. 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.