Commit c2e7d39b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge branch 'gen_proofmode' into jh/exist_plainly

parents edae2dc1 ca0996a8
......@@ -26,7 +26,8 @@ theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/bi/interface.v
theories/bi/derived.v
theories/bi/derived_connectives.v
theories/bi/derived_laws.v
theories/bi/big_op.v
theories/bi/bi.v
theories/bi/tactics.v
......
From iris.base_logic Require Export upred.
From iris.bi Require Export interface derived.
From iris.bi Require Export derived_laws.
Set Default Proof Using "Type".
Import upred.uPred.
Import interface.bi derived.bi.
Import interface.bi derived_laws.bi.
Module uPred.
Section derived.
......@@ -31,10 +31,6 @@ Proof.
apply limit_preserving_and; by apply limit_preserving_entails.
Qed.
(* Affine *)
Global Instance uPred_affine : AffineBI (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
(* Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
a bi_persistently ( a : uPred M).
......@@ -131,6 +127,6 @@ Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
End derived.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [AffineBI] as a premise. *)
many lemmas that have [BiAffine] as a premise. *)
Hint Immediate uPred_affine.
End uPred.
From iris.algebra Require Export cmra updates.
From iris.bi Require Export interface.
From iris.bi Require Export derived_connectives.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
......@@ -608,10 +608,13 @@ Proof.
Qed.
Global Instance bupd_proper : Proper (() ==> ()) (@uPred_bupd M) := ne_proper _.
(** PlainlyExist1BI *)
(** BI instances *)
Global Instance uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
Proof. unfold PlainlyExist1BI. by unseal. Qed.
Global Instance uPred_affine : BiAffine (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredI M).
Proof. unfold BiPlainlyExist. by unseal. Qed.
(** Limits *)
Lemma entails_lim (cP cQ : chain (uPredC M)) :
......
From iris.bi Require Export interface derived big_op.
From iris.bi Require Export derived_laws big_op.
Set Default Proof Using "Type".
Module Import bi.
Export bi.interface.bi.
Export bi.derived.bi.
Export bi.derived_laws.bi.
Export bi.big_op.bi.
End bi.
......
From iris.algebra Require Export big_op.
From iris.bi Require Export derived.
From iris.bi Require Export derived_laws.
From stdpp Require Import countable fin_collections functions.
Set Default Proof Using "Type".
......@@ -41,7 +41,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
(** * Properties *)
Module bi.
Import interface.bi derived.bi.
Import interface.bi derived_laws.bi.
Section bi_big_op.
Context {PROP : bi}.
Implicit Types Ps Qs : list PROP.
......@@ -55,7 +55,7 @@ Section sep_list.
Lemma big_sepL_nil Φ : ([ list] ky nil, Φ k y) emp.
Proof. done. Qed.
Lemma big_sepL_nil' `{AffineBI PROP} P Φ : P [ list] ky nil, Φ k y.
Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P [ list] ky nil, Φ k y.
Proof. apply (affine _). Qed.
Lemma big_sepL_cons Φ x l :
([ list] ky x :: l, Φ k y) Φ 0 x [ list] ky l, Φ (S k) y.
......@@ -75,7 +75,7 @@ Section sep_list.
( k y, l !! k = Some y Φ k y Ψ k y)
([ list] k y l, Φ k y) ([ list] k y l, Ψ k y).
Proof. apply big_opL_proper. Qed.
Lemma big_sepL_submseteq `{AffineBI PROP} (Φ : A PROP) l1 l2 :
Lemma big_sepL_submseteq `{BiAffine PROP} (Φ : A PROP) l1 l2 :
l1 + l2 ([ list] y l2, Φ y) [ list] y l1, Φ y.
Proof.
intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
......@@ -125,16 +125,16 @@ Section sep_list.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepL_plainly `{AffineBI PROP} Φ l :
Lemma big_sepL_plainly `{BiAffine PROP} Φ l :
bi_plainly ([ list] kx l, Φ k x) [ list] kx l, bi_plainly (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
bi_persistently ([ list] kx l, Φ k x)
[ list] kx l, bi_persistently (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_forall `{AffineBI PROP} Φ l :
Lemma big_sepL_forall `{BiAffine PROP} Φ l :
( k x, Persistent (Φ k x))
([ list] kx l, Φ k x) ( k x, l !! k = Some x Φ k x).
Proof.
......@@ -287,7 +287,7 @@ Section and_list.
[ list] kx l, bi_persistently (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_andL_forall `{AffineBI PROP} Φ l :
Lemma big_andL_forall `{BiAffine PROP} Φ l :
([ list] kx l, Φ k x) ( k x, l !! k = Some x Φ k x).
Proof.
apply (anti_symm _).
......@@ -328,7 +328,7 @@ Section gmap.
( k x, m !! k = Some x Φ k x Ψ k x)
([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
Proof. apply big_opM_proper. Qed.
Lemma big_sepM_subseteq `{AffineBI PROP} Φ m1 m2 :
Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 :
m2 m1 ([ map] k x m1, Φ k x) [ map] k x m2, Φ k x.
Proof. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
......@@ -339,7 +339,7 @@ Section gmap.
Lemma big_sepM_empty Φ : ([ map] kx , Φ k x) emp.
Proof. by rewrite big_opM_empty. Qed.
Lemma big_sepM_empty' `{AffineBI PROP} P Φ : P [ map] kx , Φ k x.
Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P [ map] kx , Φ k x.
Proof. rewrite big_sepM_empty. apply: affine. Qed.
Lemma big_sepM_insert Φ m i x :
......@@ -420,16 +420,16 @@ Section gmap.
([ map] kx m, Φ k x) ([ map] kx m, Ψ k x).
Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepM_plainly `{AffineBI PROP} Φ m :
Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
bi_plainly ([ map] kx m, Φ k x) [ map] kx m, bi_plainly (Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
(bi_persistently ([ map] kx m, Φ k x))
([ map] kx m, bi_persistently (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_forall `{AffineBI PROP} Φ m :
Lemma big_sepM_forall `{BiAffine PROP} Φ m :
( k x, Persistent (Φ k x))
([ map] kx m, Φ k x) ( k x, m !! k = Some x Φ k x).
Proof.
......@@ -499,7 +499,7 @@ Section gset.
( x, x X Φ x Ψ x)
([ set] x X, Φ x) ([ set] x X, Ψ x).
Proof. apply big_opS_proper. Qed.
Lemma big_sepS_subseteq `{AffineBI PROP} Φ X Y :
Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y :
Y X ([ set] x X, Φ x) [ set] x Y, Φ x.
Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
......@@ -509,7 +509,7 @@ Section gset.
Lemma big_sepS_empty Φ : ([ set] x , Φ x) emp.
Proof. by rewrite big_opS_empty. Qed.
Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P [ set] x , Φ x.
Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P [ set] x , Φ x.
Proof. rewrite big_sepS_empty. apply: affine. Qed.
Lemma big_sepS_insert Φ X x :
......@@ -575,12 +575,12 @@ Section gset.
by apply sep_mono_r, wand_intro_l.
Qed.
Lemma big_sepS_filter `{AffineBI PROP}
Lemma big_sepS_filter `{BiAffine PROP}
(P : A Prop) `{ x, Decision (P x)} Φ X :
([ set] y filter P X, Φ y) ([ set] y X, P y Φ y).
Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
Lemma big_sepS_filter_acc `{AffineBI PROP}
Lemma big_sepS_filter_acc `{BiAffine PROP}
(P : A Prop) `{ y, Decision (P y)} Φ X Y :
( y, y Y P y y X)
([ set] y X, Φ y) -
......@@ -596,15 +596,15 @@ Section gset.
([ set] y X, Φ y Ψ y) ([ set] y X, Φ y) ([ set] y X, Ψ y).
Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepS_plainly `{AffineBI PROP} Φ X :
Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
bi_plainly ([ set] y X, Φ y) [ set] y X, bi_plainly (Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
bi_persistently ([ set] y X, Φ y) [ set] y X, bi_persistently (Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_forall `{AffineBI PROP} Φ X :
Lemma big_sepS_forall `{BiAffine PROP} Φ X :
( x, Persistent (Φ x)) ([ set] x X, Φ x) ( x, x X Φ x).
Proof.
intros. apply (anti_symm _).
......@@ -671,7 +671,7 @@ Section gmultiset.
( x, x X Φ x Ψ x)
([ mset] x X, Φ x) ([ mset] x X, Ψ x).
Proof. apply big_opMS_proper. Qed.
Lemma big_sepMS_subseteq `{AffineBI PROP} Φ X Y :
Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y :
Y X ([ mset] x X, Φ x) [ mset] x Y, Φ x.
Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
......@@ -681,7 +681,7 @@ Section gmultiset.
Lemma big_sepMS_empty Φ : ([ mset] x , Φ x) emp.
Proof. by rewrite big_opMS_empty. Qed.
Lemma big_sepMS_empty' `{!AffineBI PROP} P Φ : P [ mset] x , Φ x.
Lemma big_sepMS_empty' `{!BiAffine PROP} P Φ : P [ mset] x , Φ x.
Proof. rewrite big_sepMS_empty. apply: affine. Qed.
Lemma big_sepMS_union Φ X Y :
......@@ -714,11 +714,11 @@ Section gmultiset.
([ mset] y X, Φ y Ψ y) ([ mset] y X, Φ y) ([ mset] y X, Ψ y).
Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepMS_plainly `{AffineBI PROP} Φ X :
Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
bi_plainly ([ mset] y X, Φ y) [ mset] y X, bi_plainly (Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
bi_persistently ([ mset] y X, Φ y)
[ mset] y X, bi_persistently (Φ y).
Proof. apply (big_opMS_commute _). Qed.
......@@ -756,11 +756,11 @@ Section list.
Implicit Types l : list A.
Implicit Types Φ Ψ : nat A PROP.
Lemma big_sepL_later `{AffineBI PROP} Φ l :
Lemma big_sepL_later `{BiAffine PROP} Φ l :
([ list] kx l, Φ k x) ([ list] kx l, Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_laterN `{AffineBI PROP} Φ n l :
Lemma big_sepL_laterN `{BiAffine PROP} Φ n l :
^n ([ list] kx l, Φ k x) ([ list] kx l, ^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
......@@ -781,11 +781,11 @@ Section gmap.
Implicit Types m : gmap K A.
Implicit Types Φ Ψ : K A PROP.
Lemma big_sepM_later `{AffineBI PROP} Φ m :
Lemma big_sepM_later `{BiAffine PROP} Φ m :
([ map] kx m, Φ k x) ([ map] kx m, Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_laterN `{AffineBI PROP} Φ n m :
Lemma big_sepM_laterN `{BiAffine PROP} Φ n m :
^n ([ map] kx m, Φ k x) ([ map] kx m, ^n Φ k x).
Proof. apply (big_opM_commute _). Qed.
......@@ -803,11 +803,11 @@ Section gset.
Implicit Types X : gset A.
Implicit Types Φ : A PROP.
Lemma big_sepS_later `{AffineBI PROP} Φ X :
Lemma big_sepS_later `{BiAffine PROP} Φ X :
([ set] y X, Φ y) ([ set] y X, Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_laterN `{AffineBI PROP} Φ n X :
Lemma big_sepS_laterN `{BiAffine PROP} Φ n X :
^n ([ set] y X, Φ y) ([ set] y X, ^n Φ y).
Proof. apply (big_opS_commute _). Qed.
......@@ -825,11 +825,11 @@ Section gmultiset.
Implicit Types X : gmultiset A.
Implicit Types Φ : A PROP.
Lemma big_sepMS_later `{AffineBI PROP} Φ X :
Lemma big_sepMS_later `{BiAffine PROP} Φ X :
([ mset] y X, Φ y) ([ mset] y X, Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_laterN `{AffineBI PROP} Φ n X :
Lemma big_sepMS_laterN `{BiAffine PROP} Φ n X :
^n ([ mset] y X, Φ y) ([ mset] y X, ^n Φ y).
Proof. apply (big_opMS_commute _). Qed.
......
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type*".
(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependent allocation. *)
Module savedprop. Section savedprop.
Context `{AffineBI PROP}.
Context `{BiAffine PROP}.
Notation "¬ P" := ( (P False))%I : bi_scope.
Implicit Types P : PROP.
......@@ -65,7 +65,7 @@ End savedprop. End savedprop.
(** This proves that we need the ▷ when opening invariants. *)
Module inv. Section inv.
Context `{AffineBI PROP}.
Context `{BiAffine PROP}.
Implicit Types P : PROP.
(** Assumptions *)
......
From iris.bi Require Export interface.
From iris.algebra Require Import monoid.
From stdpp Require Import hlist.
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P Q) (Q P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_iff) 1.
Infix "↔" := bi_iff : bi_scope.
Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
((P - Q) (Q - P))%I.
Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
Class Plain {PROP : bi} (P : PROP) := plain : P bi_plainly P.
Arguments Plain {_} _%I : simpl never.
Arguments plain {_} _%I {_}.
Hint Mode Plain + ! : typeclass_instances.
Instance: Params (@Plain) 1.
Class Persistent {PROP : bi} (P : PROP) := persistent : P bi_persistently P.
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp P)%I.
Arguments bi_affinely {_} _%I : simpl never.
Instance: Params (@bi_affinely) 1.
Typeclasses Opaque bi_affinely.
Notation "□ P" := (bi_affinely (bi_persistently P))%I
(at level 20, right associativity) : bi_scope.
Notation "■ P" := (bi_affinely (bi_plainly P))%I
(at level 20, right associativity) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q emp.
Arguments Affine {_} _%I : simpl never.
Arguments affine {_} _%I {_}.
Hint Mode Affine + ! : typeclass_instances.
Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Existing Instance absorbing_bi | 0.
Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : bi_affinely (P Q) bi_affinely P Q.
Class BiPlainlyExist (PROP : bi) :=
plainly_exist_1 A (Ψ : A PROP) :
bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a).
Arguments plainly_exist_1 _ {_ _} _.
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1.
Typeclasses Opaque bi_absorbingly.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P P.
Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I.
Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then bi_plainly P else P)%I.
Arguments bi_plainly_if {_} !_ _%I /.
Instance: Params (@bi_plainly_if) 2.
Typeclasses Opaque bi_plainly_if.
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then bi_persistently P else P)%I.
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then bi_affinely P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Typeclasses Opaque bi_affinely_if.
Notation "□? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
(at level 20, p at level 9, P at level 20,
right associativity, format "□? p P") : bi_scope.
Notation "■? p P" := (bi_affinely_if p (bi_plainly_if p P))%I
(at level 20, p at level 9, P at level 20,
right associativity, format "■? p P") : bi_scope.
Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP PROP :=
match As return himpl As PROP PROP with
| tnil => id
| tcons A As => λ Φ, x, bi_hexist (Φ x)
end%I.
Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP PROP :=
match As return himpl As PROP PROP with
| tnil => id
| tcons A As => λ Φ, x, bi_hforall (Φ x)
end%I.
Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
Nat.iter n bi_later P.
Arguments bi_laterN {_} !_%nat_scope _%I.
Instance: Params (@bi_laterN) 2.
Notation "▷^ n P" := (bi_laterN n P)
(at level 20, n at level 9, P at level 20, format "▷^ n P") : bi_scope.
Notation "▷? p P" := (bi_laterN (Nat.b2n p) P)
(at level 20, p at level 9, P at level 20, format "▷? p P") : bi_scope.
Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := ( False P)%I.
Arguments bi_except_0 {_} _%I : simpl never.
Notation "◇ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
Instance: Params (@bi_except_0) 1.
Typeclasses Opaque bi_except_0.
Class Timeless {PROP : sbi} (P : PROP) := timeless : P P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.
......@@ -329,10 +329,6 @@ Coercion sbi_valid {PROP : sbi} : PROP → Prop := bi_valid.
Arguments bi_valid {_} _%I : simpl never.
Typeclasses Opaque bi_valid.
Class PlainlyExist1BI (PROP : bi) :=
plainly_exist_1 A (Ψ : A PROP) : bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a).
Arguments plainly_exist_1 {_ _ _} _.
Module bi.
Section bi_laws.
Context {PROP : bi}.
......
......@@ -32,7 +32,7 @@ Module bi_reflection. Section bi_reflection.
Qed.
(* Can be related to the RHS being affine *)
Lemma flatten_entails `{AffineBI PROP} Σ e1 e2 :
Lemma flatten_entails `{BiAffine PROP} Σ e1 e2 :
flatten e2 + flatten e1 eval Σ e1 eval Σ e2.
Proof. intros. rewrite !eval_flatten. by apply big_sepL_submseteq. Qed.
Lemma flatten_equiv Σ e1 e2 :
......
......@@ -50,7 +50,7 @@ Proof.
rewrite /FromAssumption /= =><-.
by rewrite persistently_elim plainly_elim_persistently.
Qed.
Global Instance from_assumption_plainly_l_false `{AffineBI PROP} P Q :
Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
FromAssumption true P Q FromAssumption false (bi_plainly P) Q.
Proof.
rewrite /FromAssumption /= =><-.
......@@ -62,7 +62,7 @@ Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim
Global Instance from_assumption_persistently_l_true P Q :
FromAssumption true P Q FromAssumption true (bi_persistently P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
FromAssumption true P Q FromAssumption false (bi_persistently P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
Global Instance from_assumption_affinely_l_true p P Q :
......@@ -224,7 +224,7 @@ Proof.
rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Qed.
Global Instance into_wand_impl_false_false `{!AffineBI PROP} P Q P' :
Global Instance into_wand_impl_false_false `{!BiAffine PROP} P Q P' :
FromAssumption false P P' IntoWand false false (P' Q) P Q.
Proof.
rewrite /FromAssumption /IntoWand /= => ->. apply wand_intro_r.
......@@ -274,7 +274,7 @@ Proof. by rewrite /IntoWand affinely_plainly_elim. Qed.
Global Instance into_wand_plainly_true q R P Q :
IntoWand true q R P Q IntoWand true q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
Global Instance into_wand_plainly_false `{!AffineBI PROP} q R P Q :
Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
IntoWand false q R P Q IntoWand false q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand plainly_elim. Qed.
......@@ -284,7 +284,7 @@ Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
Global Instance into_wand_persistently_true q R P Q :
IntoWand true q R P Q IntoWand true q (bi_persistently R) P Q.
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
IntoWand false q R P Q IntoWand false q (bi_persistently R) P Q.
Proof. by rewrite /IntoWand persistently_elim. Qed.
......@@ -388,7 +388,7 @@ Proof.
by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
Qed.
Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P Q) P Q.
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P Q) P Q.
Proof.
by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
......@@ -460,10 +460,10 @@ Global Instance into_sep_affinely P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
Global Instance into_sep_plainly `{PositiveBI PROP} P Q1 Q2 :
Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
IntoSep P Q1 Q2 IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
IntoSep P Q1 Q2
IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
......@@ -512,7 +512,7 @@ Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
Global Instance into_or_absorbingly P Q1 Q2 :