Library iris.proofmode.class_instances

From iris.bi Require Import telescopes.
From iris.proofmode Require Import base modality_instances classes classes_make.
From iris.proofmode Require Import ltac_tactics.
From iris.prelude Require Import options.
Import bi.

Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Global Hint Extern 0 (FromAssumption _ _ _) ⇒
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.

Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Hint Extern 0 (FromExist _ _) ⇒
  notypeclasses refine (from_exist_exist _) : typeclass_instances.

Section class_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Implicit Types mP : option PROP.

Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (⊢ P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
Proof. split; [ apply bi.entails_wand | apply bi.wand_entails ]. Qed.
Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
Proof. split; [ apply bi.equiv_wand_iff | apply bi.wand_iff_equiv ]. Qed.

Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
Proof.
  rewrite /AsEmpValid⇒H1. split⇒H2.
  - apply bi.forall_intro=>?. apply H1, H2.
  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.
Global Instance as_emp_valid_tforall {TT : tele} (φ : TT → Prop) (P : TT → PROP) :
  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀.. x, φ x) (∀.. x, P x).
Proof.
  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
  apply as_emp_valid_forall.
Qed.

Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
Proof. by rewrite /FromAffinely. Qed.
Global Instance from_affinely_intuitionistically P :
  FromAffinely (□ P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.

Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
Proof. by rewrite /IntoAbsorbingly -absorbingly_emp_True. Qed.
Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
Global Instance into_absorbingly_intuitionistically P :
  IntoAbsorbingly (<pers> P) (□ P) | 2.
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
Proof. by rewrite /IntoAbsorbingly. Qed.

Global Instance from_assumption_persistently_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (<pers> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply intuitionistically_persistent.
Qed.
Global Instance from_assumption_affinely_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (<affine> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.
Global Instance from_assumption_intuitionistically_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (□ Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_idemp.
Qed.
Global Instance from_assumption_absorbingly_r p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (<absorb> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.

Global Instance from_assumption_intuitionistically_l p P Q :
  FromAssumption true P Q → KnownLFromAssumption p (□ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_if_elim.
Qed.
Global Instance from_assumption_persistently_l_true P Q :
  FromAssumption true P Q → KnownLFromAssumption true (<pers> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite intuitionistically_persistently_elim //.
Qed.
Global Instance from_assumption_persistently_l_false `{!BiAffine PROP} P Q :
  FromAssumption true P Q → KnownLFromAssumption false (<pers> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_into_persistently.
Qed.
Global Instance from_assumption_affinely_l_true p P Q :
  FromAssumption p P Q → KnownLFromAssumption p (<affine> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.
Global Instance from_assumption_intuitionistically_l_true p P Q :
  FromAssumption p P Q → KnownLFromAssumption p (□ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_elim.
Qed.

Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀ x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption⇒ <-.
  by rewrite forall_elim.
Qed.
Global Instance from_assumption_tforall {TT : tele} p (Φ : TT → PROP) Q x :
  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption⇒ <-.
  by rewrite bi_tforall_forall forall_elim.
Qed.

Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
Proof. rewrite /IntoPure pure_and. by intros → →. Qed.
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∨ P2) (φ1 ∨ φ2).
Proof. rewrite /IntoPure pure_or. by intros → →. Qed.
Global Instance into_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2 :
  FromPure false P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2).
Proof. rewrite /FromPure /IntoPure /= ⇒ <- →. apply pure_impl_2. Qed.

Global Instance into_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
Proof. rewrite /IntoPure⇒Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
Global Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
Global Instance into_pure_forall `{!BiPureForall PROP}
    {A} (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).
Proof. rewrite /IntoPure⇒Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
Global Instance into_pure_tforall `{!BiPureForall PROP}
    {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
Proof.
  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
Qed.

Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2).
Proof. rewrite /IntoPure⇒ → →. by rewrite sep_and pure_and. Qed.
Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
Proof.
  rewrite /FromPure /IntoPure⇒ <- → /=. rewrite pure_impl.
  apply impl_intro_l, pure_elim_l⇒ ?. rewrite (pure_True φ1) //.
  by rewrite -affinely_affinely_if affinely_True_emp left_id.
Qed.

Global Instance into_pure_affinely P φ : IntoPure P φ → IntoPure (<affine> P) φ.
Proof. rewrite /IntoPure⇒ →. apply affinely_elim. Qed.
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ → IntoPure (□ P) φ.
Proof. rewrite /IntoPure⇒ →. apply intuitionistically_elim. Qed.
Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (<absorb> P) φ.
Proof. rewrite /IntoPure⇒ →. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
  IntoPure P φ → IntoPure (<pers> P) φ.
Proof. rewrite /IntoPure⇒ →. apply: persistently_elim. Qed.

Global Instance into_pure_big_sepL {A}
    (Φ : nat → A → PROP) (φ : nat → A → Prop) (l : list A) :
  (∀ k x, IntoPure (Φ k x) (φ k x)) →
  IntoPure ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepL_pure_1. done.
Qed.
Global Instance into_pure_big_sepM `{Countable K} {A}
    (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) :
  (∀ k x, IntoPure (Φ k x) (φ k x)) →
  IntoPure ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepM_pure_1. done.
Qed.
Global Instance into_pure_big_sepS `{Countable A}
    (Φ : A → PROP) (φ : A → Prop) (X : gset A) :
  (∀ x, IntoPure (Φ x) (φ x)) →
  IntoPure ([∗ set] x ∈ X, Φ x) (set_Forall φ X).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepS_pure_1. done.
Qed.
Global Instance into_pure_big_sepMS `{Countable A}
    (Φ : A → PROP) (φ : A → Prop) (X : gmultiset A) :
  (∀ x, IntoPure (Φ x) (φ x)) →
  IntoPure ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepMS_pure_1. done.
Qed.

Global Instance from_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure /=. apply (affine _). Qed.
Global Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Proof. by rewrite /FromPure /=. Qed.
Global Instance from_pure_pure_and a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
  FromPure (if a1 then true else a2) (P1 ∧ P2) (φ1 ∧ φ2).
Proof.
  rewrite /FromPure pure_and⇒ <- <- /=. rewrite affinely_if_and.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_or a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
  FromPure (if a1 then true else a2) (P1 ∨ P2) (φ1 ∨ φ2).
Proof.
  rewrite /FromPure pure_or⇒ <- <- /=. rewrite affinely_if_or.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → FromPure a P2 φ2 → FromPure a (P1 → P2) (φ1 → φ2).
Proof.
  rewrite /FromPure /IntoPure pure_impl_1⇒ → <-. destruct a=>//=.
  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
Qed.

Global Instance from_pure_exist {A} a (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃ x, Φ x) (∃ x, φ x).
Proof.
  rewrite /FromPure⇒Hx. rewrite pure_exist affinely_if_exist.
  by setoid_rewrite Hx.
Qed.
Global Instance from_pure_texist {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃.. x, Φ x) (∃.. x, φ x).
Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
Global Instance from_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
Proof.
  rewrite /FromPure⇒Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.
Global Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀.. x, Φ x) (∀.. x, φ x).
Proof.
  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
Qed.

Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
  FromPure (if a1 then a2 else false) (P1 ∗ P2) (φ1 ∧ φ2).
Proof.
  rewrite /FromPure⇒ <- <-. destruct a1; simpl.
  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
Qed.
Global Instance from_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → FromPure a P2 φ2 →
  TCOr (TCEq a false) (Affine P1) →
  FromPure a (P1 -∗ P2) (φ1 → φ2).
Proof.
  rewrite /FromPure /IntoPure⇒ HP1 <- Ha /=. apply wand_intro_l.
  destruct a; simpl.
  - destruct Ha as [Ha|?]; first inversion Ha.
    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
    by rewrite affinely_and_l pure_impl_1 impl_elim_r.
  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
Qed.

Global Instance from_pure_persistently P a φ :
  FromPure true P φ → FromPure a (<pers> P) φ.
Proof.
  rewrite /FromPure⇒ <- /=.
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
Qed.
Global Instance from_pure_affinely_true a P φ :
  FromPure a P φ → FromPure true (<affine> P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.
Global Instance from_pure_intuitionistically_true a P φ :
  FromPure a P φ → FromPure true (□ P) φ.
Proof.
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
Qed.
Global Instance from_pure_absorbingly a P φ :
  FromPure a P φ → FromPure false (<absorb> P) φ.
Proof.
  rewrite /FromPure⇒ <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
Qed.

Global Instance from_pure_big_sepL {A}
    a (Φ : nat → A → PROP) (φ : nat → A → Prop) (l : list A) :
  (∀ k x, FromPure a (Φ k x) (φ k x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepL_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepL_pure. setoid_rewrite HΦ. done.
Qed.
Global Instance from_pure_big_sepM `{Countable K} {A}
    a (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) :
  (∀ k x, FromPure a (Φ k x) (φ k x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepM_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepM_pure. setoid_rewrite HΦ. done.
Qed.
Global Instance from_pure_big_sepS `{Countable A}
    a (Φ : A → PROP) (φ : A → Prop) (X : gset A) :
  (∀ x, FromPure a (Φ x) (φ x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ set] x ∈ X, Φ x) (set_Forall φ X).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepS_pure. setoid_rewrite HΦ. done.
Qed.
Global Instance from_pure_big_sepMS `{Countable A}
    a (Φ : A → PROP) (φ : A → Prop) (X : gmultiset A) :
  (∀ x, FromPure a (Φ x) (φ x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepMS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepMS_pure. setoid_rewrite HΦ. done.
Qed.

Global Instance into_persistent_persistently p P Q :
  IntoPersistent true P Q → IntoPersistent p (<pers> P) Q | 0.
Proof.
  rewrite /IntoPersistent /= ⇒ →.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
Global Instance into_persistent_affinely p P Q :
  IntoPersistent p P Q → IntoPersistent p (<affine> P) Q | 0.
Proof. rewrite /IntoPersistent /= ⇒ <-. by rewrite affinely_elim. Qed.
Global Instance into_persistent_intuitionistically p P Q :
  IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
Proof.
  rewrite /IntoPersistent /= =><-.
  destruct p; simpl;
    eauto using persistently_mono, intuitionistically_elim,
    intuitionistically_into_persistently_1.
Qed.
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.
Global Instance into_persistent_persistent P :
  Persistent P → IntoPersistent false P P | 100.
Proof. intros. by rewrite /IntoPersistent. Qed.

Global Instance from_modal_affinely P :
  FromModal True modality_affinely (<affine> P) (<affine> P) P | 2.
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
  FromModal True modality_persistently (<pers> P) (<pers> P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_intuitionistically P :
  FromModal True modality_intuitionistically (□ P) (□ P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_intuitionistically_affine_bi P :
  BiAffine PROP → FromModal True modality_persistently (□ P) (□ P) P | 0.
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.

Global Instance from_modal_absorbingly P :
  FromModal True modality_id (<absorb> P) (<absorb> P) P.
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
  IntoWand' p q (mP -∗? Q) P' Q' → IntoWand p q (mP -∗? Q) P' Q' | 100.
Proof. done. Qed.

Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand⇒ HP. by rewrite HP intuitionistically_if_elim.
Qed.

Global Instance into_wand_impl_false_false P Q P' P'' :
  Absorbing P →
  
  TCOr (BiAffine PROP) (Persistent P) →
  MakeAffinely P P' →
  FromAssumption false P'' P' →
  IntoWand false false (P → Q) P'' Q.
Proof.
  rewrite /MakeAffinely /IntoWand /FromAssumption /= ⇒ ? Hpers <- →.
  apply wand_intro_l. destruct Hpers.
  - rewrite impl_wand_1 affinely_elim wand_elim_r //.
  - rewrite persistent_impl_wand_affinely wand_elim_r //.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
  Absorbing P' →
  FromAssumption true P P' →
  IntoWand false true (P' → Q) P Q.
Proof.
  rewrite /IntoWand /FromAssumption /= ⇒ ? HP. apply wand_intro_l.
  rewrite -(persistently_elim P').
  rewrite persistent_impl_wand_affinely.
  rewrite -(intuitionistically_idemp P) HP.
  apply wand_elim_r.
Qed.
Global Instance into_wand_impl_true_false P Q P' P'' :
  MakeAffinely P P' →
  FromAssumption false P'' P' →
  IntoWand true false (P → Q) P'' Q.
Proof.
  rewrite /MakeAffinely /IntoWand /FromAssumption /= ⇒ <- →.
  apply wand_intro_r.
  rewrite sep_and intuitionistically_elim affinely_elim impl_elim_l //.
Qed.
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P' →
  IntoWand true true (P' → Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand /= ⇒ <-. apply wand_intro_l.
  rewrite sep_and [(□ (_ → _))%I]intuitionistically_elim impl_elim_r //.
Qed.

Global Instance into_wand_wandM p q mP' P Q :
  FromAssumption q P (default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Global Instance into_wand_and_l p q R1 R2 P' Q' :
  IntoWand p q R1 P' Q' → IntoWand p q (R1 ∧ R2) P' Q'.
Proof. rewrite /IntoWand⇒ ?. by rewrite /bi_wand_iff and_elim_l. Qed.
Global Instance into_wand_and_r p q R1 R2 P' Q' :
  IntoWand p q R2 Q' P' → IntoWand p q (R1 ∧ R2) Q' P'.
Proof. rewrite /IntoWand⇒ ?. by rewrite /bi_wand_iff and_elim_r. Qed.

Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true (∀ _ : φ, P) ⌜ φ ⌝ P.
Proof.
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
  MakeAffinely ⌜ φ ⌝ Pφ →
  IntoWand p false (∀ _ : φ, P) Pφ P.
Proof.
  rewrite /MakeAffinely /IntoWand⇒ <-.
  rewrite (intuitionistically_if_elim p) /=.
  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
Qed.

Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
  IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
Proof. rewrite /IntoWand⇒ <-. by rewrite (forall_elim x). Qed.
Global Instance into_wand_tforall {TT : tele} p q (Φ : TT → PROP) P Q x :
  IntoWand p q (Φ x) P Q → IntoWand p q (∀.. x, Φ x) P Q.
Proof. rewrite /IntoWand⇒ <-. by rewrite bi_tforall_forall (forall_elim x). Qed.

Global Instance into_wand_affine p q R P Q :
  IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand /= ⇒ HR. apply wand_intro_r. destruct p; simpl in ×.
  - rewrite (affinely_elim R) -(affine_affinely (□ R)) HR. destruct q; simpl in ×.
    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
  - rewrite HR. destruct q; simpl in ×.
    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
Qed.
Global Instance into_wand_affine_args q R P Q :
  IntoWand true q R P Q → IntoWand' true q R (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= ⇒ HR. apply wand_intro_r.
  rewrite -(affine_affinely (□ R)) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.

Global Instance into_wand_intuitionistically p q R P Q :
  IntoWand true q R P Q → IntoWand p q (□ R) P Q.
Proof. rewrite /IntoWand /= ⇒ →. by rewrite {1}intuitionistically_if_elim. Qed.
Global Instance into_wand_persistently_true q R P Q :
  IntoWand true q R P Q → IntoWand true q (<pers> R) P Q.
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
Global Instance into_wand_persistently_false q R P Q :
  Absorbing R → IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.

Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
Global Instance from_wand_wandM mP1 P2 :
  FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
Proof. by rewrite /FromWand wandM_sound. Qed.

Global Instance from_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.

Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
Proof. by rewrite /FromAnd. Qed.
Global Instance from_and_sep_persistent_l P1 P1' P2 :
  Persistent P1 → IntoAbsorbingly P1' P1 → FromAnd (P1 ∗ P2) P1' P2 | 9.
Proof.
  rewrite /IntoAbsorbingly /FromAnd⇒ ? →.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
Qed.
Global Instance from_and_sep_persistent_r P1 P2 P2' :
  Persistent P2 → IntoAbsorbingly P2' P2 → FromAnd (P1 ∗ P2) P1 P2' | 10.
Proof.
  rewrite /IntoAbsorbingly /FromAnd⇒ ? →.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
Qed.

Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.

Global Instance from_and_persistently P Q1 Q2 :
  FromAnd P Q1 Q2 →
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromAnd⇒ <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
  FromSep P Q1 Q2 →
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Proof. rewrite /FromAnd⇒ <-. by rewrite -persistently_and persistently_and_sep. Qed.

Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) l x l' :
  IsCons l x l' →
  Persistent (Φ 0 x) →
  FromAnd ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
Proof. rewrite /IsCons⇒ → ?. by rewrite /FromAnd big_sepL_cons persistent_and_sep_1. Qed.
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat → A → PROP) l l1 l2 :
  IsApp l l1 l2 →
  (∀ k y, Persistent (Φ k y)) →
  FromAnd ([∗ list] k ↦ y ∈ l, Φ k y)
    ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp⇒ → ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.

Global Instance from_and_big_sepL2_cons_persistent {A B}
    (Φ : nat → A → B → PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  Persistent (Φ 0 x1 x2) →
  FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
Proof.
  rewrite /IsCons⇒ → → ?.
  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
Qed.
Global Instance from_and_big_sepL2_app_persistent {A B}
    (Φ : nat → A → B → PROP) l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
  (∀ k y1 y2, Persistent (Φ k y1 y2)) →
  FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
  rewrite /IsApp⇒ → → ?. rewrite /FromAnd persistent_and_sep_1.
  apply wand_elim_l', big_sepL2_app.
Qed.

Global Instance from_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A → PROP) X1 X2 :
  (∀ y, Persistent (Φ y)) →
  FromAnd ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.

Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
Global Instance from_sep_and P1 P2 :
  TCOr (Affine P1) (Absorbing P2) → TCOr (Affine P2) (Absorbing P1) →
  FromSep (P1 ∧ P2) P1 P2 | 101.
Proof. intros. by rewrite /FromSep sep_and. Qed.

Global Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.

Global Instance from_sep_affinely P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite affinely_sep_2. Qed.
Global Instance from_sep_intuitionistically P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite intuitionistically_sep_2. Qed.
Global Instance from_sep_absorbingly P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite absorbingly_sep. Qed.
Global Instance from_sep_persistently P Q1 Q2 :
  FromSep P Q1 Q2 →
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite persistently_sep_2. Qed.

Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
  IsCons l x l' →
  FromSep ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
Proof. rewrite /IsCons⇒ →. by rewrite /FromSep big_sepL_cons. Qed.
Global Instance from_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
  IsApp l l1 l2 →
  FromSep ([∗ list] k ↦ y ∈ l, Φ k y)
    ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp⇒ →. by rewrite /FromSep big_opL_app. Qed.

Global Instance from_sep_big_sepL2_cons {A B} (Φ : nat → A → B → PROP)
    l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons⇒ → →. by rewrite /FromSep big_sepL2_cons. Qed.
Global Instance from_sep_big_sepL2_app {A B} (Φ : nat → A → B → PROP)
    l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
  FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> →. apply wand_elim_l', big_sepL2_app. Qed.

Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A → PROP) X1 X2 :
  FromSep ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.