Commit f6040640 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove notation for `bi_absorbingly`.

We do not have a notation for `bi_affinely` either, so this is at
least consistent.
parent cbc5b184
...@@ -49,9 +49,8 @@ Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I. ...@@ -49,9 +49,8 @@ Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
Arguments bi_absorbingly {_} _%I : simpl never. Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1. Instance: Params (@bi_absorbingly) 1.
Typeclasses Opaque bi_absorbingly. Typeclasses Opaque bi_absorbingly.
Notation "▲ P" := (bi_absorbingly P) (at level 20, right associativity) : bi_scope.
Class Absorbing {PROP : bi} (P : PROP) := absorbing : P P. Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P P.
Arguments Absorbing {_} _%I : simpl never. Arguments Absorbing {_} _%I : simpl never.
Arguments absorbing {_} _%I. Arguments absorbing {_} _%I.
...@@ -767,53 +766,57 @@ Global Instance absorbingly_flip_mono' : ...@@ -767,53 +766,57 @@ Global Instance absorbingly_flip_mono' :
Proper (flip () ==> flip ()) (@bi_absorbingly PROP). Proper (flip () ==> flip ()) (@bi_absorbingly PROP).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Lemma absorbingly_intro P : P P. Lemma absorbingly_intro P : P bi_absorbingly P.
Proof. by rewrite /bi_absorbingly -True_sep_2. Qed. Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
Lemma absorbingly_mono P Q : (P Q) P Q. Lemma absorbingly_mono P Q : (P Q) bi_absorbingly P bi_absorbingly Q.
Proof. by intros ->. Qed. Proof. by intros ->. Qed.
Lemma absorbingly_idemp P : P P. Lemma absorbingly_idemp P : bi_absorbingly (bi_absorbingly P) bi_absorbingly P.
Proof. Proof.
apply (anti_symm _), absorbingly_intro. apply (anti_symm _), absorbingly_intro.
rewrite /bi_absorbingly assoc. apply sep_mono; auto. rewrite /bi_absorbingly assoc. apply sep_mono; auto.
Qed. Qed.
Lemma absorbingly_pure φ : φ φ . Lemma absorbingly_pure φ : bi_absorbingly φ φ .
Proof. Proof.
apply (anti_symm _), absorbingly_intro. apply (anti_symm _), absorbingly_intro.
apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto. apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
Qed. Qed.
Lemma absorbingly_or P Q : (P Q) P Q. Lemma absorbingly_or P Q :
bi_absorbingly (P Q) bi_absorbingly P bi_absorbingly Q.
Proof. by rewrite /bi_absorbingly sep_or_l. Qed. Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
Lemma absorbingly_and P Q : (P Q) P Q. Lemma absorbingly_and P Q :
bi_absorbingly (P Q) bi_absorbingly P bi_absorbingly Q.
Proof. apply and_intro; apply absorbingly_mono; auto. Qed. Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
Lemma absorbingly_forall {A} (Φ : A PROP) : ( a, Φ a) a, Φ a. Lemma absorbingly_forall {A} (Φ : A PROP) :
bi_absorbingly ( a, Φ a) a, bi_absorbingly (Φ a).
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
Lemma absorbingly_exist {A} (Φ : A PROP) : ( a, Φ a) a, Φ a. Lemma absorbingly_exist {A} (Φ : A PROP) :
bi_absorbingly ( a, Φ a) a, bi_absorbingly (Φ a).
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed. Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : (x y) x y. Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : bi_absorbingly (x y) x y.
Proof. Proof.
apply (anti_symm _), absorbingly_intro. apply (anti_symm _), absorbingly_intro.
apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True - x y)%I); auto. apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True - x y)%I); auto.
apply wand_intro_l, internal_eq_refl. apply wand_intro_l, internal_eq_refl.
Qed. Qed.
Lemma absorbingly_sep P Q : (P Q) P Q. Lemma absorbingly_sep P Q : bi_absorbingly (P Q) bi_absorbingly P bi_absorbingly Q.
Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed. Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
Lemma absorbingly_True_emp : True emp. Lemma absorbingly_True_emp : bi_absorbingly True bi_absorbingly emp.
Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed. Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
Lemma absorbingly_wand P Q : (P - Q) P - Q. Lemma absorbingly_wand P Q : bi_absorbingly (P - Q) bi_absorbingly P - bi_absorbingly Q.
Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed. Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
Lemma absorbingly_sep_l P Q : P Q (P Q). Lemma absorbingly_sep_l P Q : bi_absorbingly P Q bi_absorbingly (P Q).
Proof. by rewrite /bi_absorbingly assoc. Qed. Proof. by rewrite /bi_absorbingly assoc. Qed.
Lemma absorbingly_sep_r P Q : P Q (P Q). Lemma absorbingly_sep_r P Q : P bi_absorbingly Q bi_absorbingly (P Q).
Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed. Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
Lemma absorbingly_sep_lr P Q : P Q P Q. Lemma absorbingly_sep_lr P Q : bi_absorbingly P Q P bi_absorbingly Q.
Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed. Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
Lemma affinely_absorbingly `{!PositiveBI PROP} P : Lemma affinely_absorbingly `{!PositiveBI PROP} P :
bi_affinely ( P) bi_affinely P. bi_affinely (bi_absorbingly P) bi_affinely P.
Proof. Proof.
apply (anti_symm _), affinely_mono, absorbingly_intro. apply (anti_symm _), affinely_mono, absorbingly_intro.
by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id. by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id.
...@@ -872,13 +875,13 @@ Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed. ...@@ -872,13 +875,13 @@ Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.
Global Instance wand_absorbing P Q : Absorbing Q Absorbing (P - Q). Global Instance wand_absorbing P Q : Absorbing Q Absorbing (P - Q).
Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed. Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed.
Global Instance absorbingly_absorbing P : Absorbing ( P). Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
Proof. rewrite /bi_absorbingly. apply _. Qed. Proof. rewrite /bi_absorbingly. apply _. Qed.
(* Properties of affine and absorbing propositions *) (* Properties of affine and absorbing propositions *)
Lemma affine_affinely P `{!Affine P} : bi_affinely P P. Lemma affine_affinely P `{!Affine P} : bi_affinely P P.
Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed. Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
Lemma absorbing_absorbingly P `{!Absorbing P} : P P. Lemma absorbing_absorbingly P `{!Absorbing P} : bi_absorbingly P P.
Proof. by apply (anti_symm _), absorbingly_intro. Qed. Proof. by apply (anti_symm _), absorbingly_intro. Qed.
Lemma True_affine_all_affine P : Affine (True%I : PROP) Affine P. Lemma True_affine_all_affine P : Affine (True%I : PROP) Affine P.
...@@ -965,7 +968,8 @@ Global Instance persistently_flip_mono' : ...@@ -965,7 +968,8 @@ Global Instance persistently_flip_mono' :
Proper (flip () ==> flip ()) (@bi_persistently PROP). Proper (flip () ==> flip ()) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed. Proof. intros P Q; apply persistently_mono. Qed.
Lemma absorbingly_persistently P : bi_persistently P bi_persistently P. Lemma absorbingly_persistently P :
bi_absorbingly (bi_persistently P) bi_persistently P.
Proof. Proof.
apply (anti_symm _), absorbingly_intro. apply (anti_symm _), absorbingly_intro.
by rewrite /bi_absorbingly comm persistently_absorbing. by rewrite /bi_absorbingly comm persistently_absorbing.
...@@ -987,7 +991,7 @@ Proof. ...@@ -987,7 +991,7 @@ Proof.
Qed. Qed.
Lemma persistently_and_emp_elim P : emp bi_persistently P P. Lemma persistently_and_emp_elim P : emp bi_persistently P P.
Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed. Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
Lemma persistently_elim_absorbingly P : bi_persistently P P. Lemma persistently_elim_absorbingly P : bi_persistently P bi_absorbingly P.
Proof. Proof.
rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I). rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I).
by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm. by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm.
...@@ -1171,7 +1175,7 @@ Global Instance plainly_flip_mono' : ...@@ -1171,7 +1175,7 @@ Global Instance plainly_flip_mono' :
Proper (flip () ==> flip ()) (@bi_plainly PROP). Proper (flip () ==> flip ()) (@bi_plainly PROP).
Proof. intros P Q; apply plainly_mono. Qed. Proof. intros P Q; apply plainly_mono. Qed.
Lemma absorbingly_plainly P : bi_plainly P bi_plainly P. Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) bi_plainly P.
Proof. Proof.
apply (anti_symm _), absorbingly_intro. apply (anti_symm _), absorbingly_intro.
by rewrite /bi_absorbingly comm plainly_absorbing. by rewrite /bi_absorbingly comm plainly_absorbing.
...@@ -1195,7 +1199,7 @@ Proof. ...@@ -1195,7 +1199,7 @@ Proof.
Qed. Qed.
Lemma plainly_and_emp_elim P : emp bi_plainly P P. Lemma plainly_and_emp_elim P : emp bi_plainly P P.
Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed. Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
Lemma plainly_elim_absorbingly P : bi_plainly P P. Lemma plainly_elim_absorbingly P : bi_plainly P bi_absorbingly P.
Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed. Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
Lemma plainly_elim P `{!Absorbing P} : bi_plainly P P. Lemma plainly_elim P `{!Absorbing P} : bi_plainly P P.
Proof. by rewrite plainly_elim_persistently persistently_elim. Qed. Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
...@@ -1662,7 +1666,7 @@ Proof. ...@@ -1662,7 +1666,7 @@ Proof.
Qed. Qed.
Global Instance affinely_plain P : Plain P Plain (bi_affinely P). Global Instance affinely_plain P : Plain P Plain (bi_affinely P).
Proof. rewrite /bi_affinely. apply _. Qed. Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance absorbingly_plain P : Plain P Plain ( P). Global Instance absorbingly_plain P : Plain P Plain (bi_absorbingly P).
Proof. rewrite /bi_absorbingly. apply _. Qed. Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance from_option_palin {A} P (Ψ : A PROP) (mx : option A) : Global Instance from_option_palin {A} P (Ψ : A PROP) (mx : option A) :
( x, Plain (Ψ x)) Plain P Plain (from_option Ψ P mx). ( x, Plain (Ψ x)) Plain P Plain (from_option Ψ P mx).
...@@ -1742,7 +1746,7 @@ Global Instance persistently_persistent P : Persistent (bi_persistently P). ...@@ -1742,7 +1746,7 @@ Global Instance persistently_persistent P : Persistent (bi_persistently P).
Proof. by rewrite /Persistent persistently_idemp. Qed. Proof. by rewrite /Persistent persistently_idemp. Qed.
Global Instance affinely_persistent P : Persistent P Persistent (bi_affinely P). Global Instance affinely_persistent P : Persistent P Persistent (bi_affinely P).
Proof. rewrite /bi_affinely. apply _. Qed. Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance absorbingly_persistent P : Persistent P Persistent ( P). Global Instance absorbingly_persistent P : Persistent P Persistent (bi_absorbingly P).
Proof. rewrite /bi_absorbingly. apply _. Qed. Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance from_option_persistent {A} P (Ψ : A PROP) (mx : option A) : Global Instance from_option_persistent {A} P (Ψ : A PROP) (mx : option A) :
( x, Persistent (Ψ x)) Persistent P Persistent (from_option Ψ P mx). ( x, Persistent (Ψ x)) Persistent P Persistent (from_option Ψ P mx).
...@@ -1796,7 +1800,8 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed. ...@@ -1796,7 +1800,8 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
Lemma persistent_entails_r P Q `{!Persistent Q} : (P Q) P P Q. Lemma persistent_entails_r P Q `{!Persistent Q} : (P Q) P P Q.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed. Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
Lemma persistent_absorbingly_affinely P `{!Persistent P} : P bi_affinely P. Lemma persistent_absorbingly_affinely P `{!Persistent P} :
P bi_absorbingly (bi_affinely P).
Proof. Proof.
by rewrite {1}(persistent_persistently_2 P) -persistently_affinely by rewrite {1}(persistent_persistently_2 P) -persistently_affinely
persistently_elim_absorbingly. persistently_elim_absorbingly.
...@@ -2005,7 +2010,7 @@ Lemma later_affinely_plainly_if_2 p P : ■?p ▷ P ⊢ ▷ ■?p P. ...@@ -2005,7 +2010,7 @@ Lemma later_affinely_plainly_if_2 p P : ■?p ▷ P ⊢ ▷ ■?p P.
Proof. destruct p; simpl; auto using later_affinely_plainly_2. Qed. Proof. destruct p; simpl; auto using later_affinely_plainly_2. Qed.
Lemma later_affinely_persistently_if_2 p P : ?p P ?p P. Lemma later_affinely_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed. Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed.
Lemma later_absorbingly P : P P. Lemma later_absorbingly P : bi_absorbingly P bi_absorbingly ( P).
Proof. by rewrite /bi_absorbingly later_sep later_True. Qed. Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
Global Instance later_plain P : Plain P Plain ( P). Global Instance later_plain P : Plain P Plain ( P).
...@@ -2080,7 +2085,7 @@ Lemma laterN_affinely_plainly_if_2 n p P : ■?p ▷^n P ⊢ ▷^n ■?p P. ...@@ -2080,7 +2085,7 @@ Lemma laterN_affinely_plainly_if_2 n p P : ■?p ▷^n P ⊢ ▷^n ■?p P.
Proof. destruct p; simpl; auto using laterN_affinely_plainly_2. Qed. Proof. destruct p; simpl; auto using laterN_affinely_plainly_2. Qed.
Lemma laterN_affinely_persistently_if_2 n p P : ?p ^n P ^n ?p P. Lemma laterN_affinely_persistently_if_2 n p P : ?p ^n P ^n ?p P.
Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed. Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed.
Lemma laterN_absorbingly n P : ^n P ^n P. Lemma laterN_absorbingly n P : ^n (bi_absorbingly P) bi_absorbingly (^n P).
Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed. Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
Global Instance laterN_plain n P : Plain P Plain (^n P). Global Instance laterN_plain n P : Plain P Plain (^n P).
...@@ -2163,7 +2168,7 @@ Lemma except_0_affinely_plainly_if_2 p P : ■?p ◇ P ⊢ ◇ ■?p P. ...@@ -2163,7 +2168,7 @@ Lemma except_0_affinely_plainly_if_2 p P : ■?p ◇ P ⊢ ◇ ■?p P.
Proof. destruct p; simpl; auto using except_0_affinely_plainly_2. Qed. Proof. destruct p; simpl; auto using except_0_affinely_plainly_2. Qed.
Lemma except_0_affinely_persistently_if_2 p P : ?p P ?p P. Lemma except_0_affinely_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed. Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
Lemma except_0_absorbingly P : P P. Lemma except_0_absorbingly P : (bi_absorbingly P) bi_absorbingly ( P).
Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed. Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
Lemma except_0_frame_l P Q : P Q (P Q). Lemma except_0_frame_l P Q : P Q (P Q).
...@@ -2250,7 +2255,7 @@ Qed. ...@@ -2250,7 +2255,7 @@ Qed.
Global Instance affinely_timeless P : Global Instance affinely_timeless P :
Timeless (emp%I : PROP) Timeless P Timeless (bi_affinely P). Timeless (emp%I : PROP) Timeless P Timeless (bi_affinely P).
Proof. rewrite /bi_affinely; apply _. Qed. Proof. rewrite /bi_affinely; apply _. Qed.
Global Instance absorbingly_timeless P : Timeless P Timeless ( P). Global Instance absorbingly_timeless P : Timeless P Timeless (bi_absorbingly P).
Proof. rewrite /bi_absorbingly; apply _. Qed. Proof. rewrite /bi_absorbingly; apply _. Qed.
Global Instance eq_timeless {A : ofeT} (a b : A) : Global Instance eq_timeless {A : ofeT} (a b : A) :
......
...@@ -18,7 +18,7 @@ Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0. ...@@ -18,7 +18,7 @@ Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed. Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
Global Instance into_absorbingly_absorbing P : Absorbing P IntoAbsorbingly P P | 1. Global Instance into_absorbingly_absorbing P : Absorbing P IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed. Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
Global Instance into_absorbingly_default P : IntoAbsorbingly ( P) P | 100. Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
Proof. by rewrite /IntoAbsorbingly. Qed. Proof. by rewrite /IntoAbsorbingly. Qed.
(* FromAssumption *) (* FromAssumption *)
...@@ -35,7 +35,7 @@ Global Instance from_assumption_affinely_r P Q : ...@@ -35,7 +35,7 @@ Global Instance from_assumption_affinely_r P Q :
FromAssumption true P Q FromAssumption true P (bi_affinely Q). FromAssumption true P Q FromAssumption true P (bi_affinely Q).
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed. Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed.
Global Instance from_assumption_absorbingly_r p P Q : Global Instance from_assumption_absorbingly_r p P Q :
FromAssumption p P Q FromAssumption p P ( Q). FromAssumption p P Q FromAssumption p P (bi_absorbingly Q).
Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed. Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
Global Instance from_assumption_affinely_plainly_l p P Q : Global Instance from_assumption_affinely_plainly_l p P Q :
...@@ -108,7 +108,7 @@ Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qe ...@@ -108,7 +108,7 @@ Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qe
Global Instance into_pure_affinely P φ : Global Instance into_pure_affinely P φ :
IntoPure P φ IntoPure (bi_affinely P) φ. IntoPure P φ IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed. Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
Global Instance into_pure_absorbingly P φ : IntoPure P φ IntoPure ( P) φ. Global Instance into_pure_absorbingly P φ : IntoPure P φ IntoPure (bi_absorbingly P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed. Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_plainly P φ : IntoPure P φ IntoPure (bi_plainly P) φ. Global Instance into_pure_plainly P φ : IntoPure P φ IntoPure (bi_plainly P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed. Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
...@@ -159,7 +159,7 @@ Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed. ...@@ -159,7 +159,7 @@ Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
Global Instance from_pure_affinely P φ `{!Affine P} : Global Instance from_pure_affinely P φ `{!Affine P} :
FromPure P φ FromPure (bi_affinely P) φ. FromPure P φ FromPure (bi_affinely P) φ.
Proof. by rewrite /FromPure affine_affinely. Qed. Proof. by rewrite /FromPure affine_affinely. Qed.
Global Instance from_pure_absorbingly P φ : FromPure P φ FromPure ( P) φ. Global Instance from_pure_absorbingly P φ : FromPure P φ FromPure (bi_absorbingly P) φ.
Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed. Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
(* IntoInternalEq *) (* IntoInternalEq *)
...@@ -170,7 +170,7 @@ Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P : ...@@ -170,7 +170,7 @@ Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq (bi_affinely P) x y. IntoInternalEq P x y IntoInternalEq (bi_affinely P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed. Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P : Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq ( P) x y. IntoInternalEq P x y IntoInternalEq (bi_absorbingly P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed. Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P : Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq (bi_plainly P) x y. IntoInternalEq P x y IntoInternalEq (bi_plainly P) x y.
...@@ -353,7 +353,7 @@ Global Instance from_sep_affinely P Q1 Q2 : ...@@ -353,7 +353,7 @@ Global Instance from_sep_affinely P Q1 Q2 :
FromSep P Q1 Q2 FromSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2). FromSep P Q1 Q2 FromSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed. Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
Global Instance from_sep_absorbingly P Q1 Q2 : Global Instance from_sep_absorbingly P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2). FromSep P Q1 Q2 FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed. Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Global Instance from_sep_plainly P Q1 Q2 : Global Instance from_sep_plainly P Q1 Q2 :
FromSep P Q1 Q2 FromSep P Q1 Q2
...@@ -491,7 +491,7 @@ Global Instance from_or_affinely P Q1 Q2 : ...@@ -491,7 +491,7 @@ Global Instance from_or_affinely P Q1 Q2 :
FromOr P Q1 Q2 FromOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2). FromOr P Q1 Q2 FromOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed. Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
Global Instance from_or_absorbingly P Q1 Q2 : Global Instance from_or_absorbingly P Q1 Q2 :
FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2). FromOr P Q1 Q2 FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed. Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
Global Instance from_or_plainly P Q1 Q2 : Global Instance from_or_plainly P Q1 Q2 :
FromOr P Q1 Q2 FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). FromOr P Q1 Q2 FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
...@@ -510,7 +510,7 @@ Global Instance into_or_affinely P Q1 Q2 : ...@@ -510,7 +510,7 @@ Global Instance into_or_affinely P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2). IntoOr P Q1 Q2 IntoOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed. Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
Global Instance into_or_absorbingly P Q1 Q2 : Global Instance into_or_absorbingly P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr ( P) ( Q1) ( Q2). IntoOr P Q1 Q2 IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed. Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
Global Instance into_or_plainly P Q1 Q2 : Global Instance into_or_plainly P Q1 Q2 :
IntoOr P Q1 Q2 IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). IntoOr P Q1 Q2 IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
...@@ -530,7 +530,7 @@ Global Instance from_exist_affinely {A} P (Φ : A → PROP) : ...@@ -530,7 +530,7 @@ Global Instance from_exist_affinely {A} P (Φ : A → PROP) :
FromExist P Φ FromExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I. FromExist P Φ FromExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed. Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
Global Instance from_exist_absorbingly {A} P (Φ : A PROP) : Global Instance from_exist_absorbingly {A} P (Φ : A PROP) :
FromExist P Φ FromExist ( P) (λ a, (Φ a))%I. FromExist P Φ FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed. Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
Global Instance from_exist_plainly {A} P (Φ : A PROP) : Global Instance from_exist_plainly {A} P (Φ : A PROP) :
FromExist P Φ FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I. FromExist P Φ FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
...@@ -562,7 +562,7 @@ Proof. ...@@ -562,7 +562,7 @@ Proof.
rewrite -exist_intro //. apply sep_elim_r, _. rewrite -exist_intro //. apply sep_elim_r, _.
Qed. Qed.
Global Instance into_exist_absorbingly {A} P (Φ : A PROP) : Global Instance into_exist_absorbingly {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I. IntoExist P Φ IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed. Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
Global Instance into_exist_plainly {A} P (Φ : A PROP) : Global Instance into_exist_plainly {A} P (Φ : A PROP) :
IntoExist P Φ IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I. IntoExist P Φ IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
...@@ -633,7 +633,7 @@ Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → PROP) : ...@@ -633,7 +633,7 @@ Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → PROP) :
Proof. Proof.
rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a). rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed. Qed.
Global Instance elim_modal_absorbingly P Q : Absorbing Q ElimModal ( P) P Q Q. Global Instance elim_modal_absorbingly P Q : Absorbing Q ElimModal (bi_absorbingly P) P Q Q.
Proof. Proof.
rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly. rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
Qed. Qed.
...@@ -666,11 +666,11 @@ Global Instance make_sep_emp_r P : MakeSep P emp P. ...@@ -666,11 +666,11 @@ Global Instance make_sep_emp_r P : MakeSep P emp P.
Proof. by rewrite /MakeSep right_id. Qed. Proof. by rewrite /MakeSep right_id. Qed.
Global Instance make_sep_true_l P : Absorbing P MakeSep True P P. Global Instance make_sep_true_l P : Absorbing P MakeSep True P P.
Proof. intros. by rewrite /MakeSep True_sep. Qed. Proof. intros. by rewrite /MakeSep True_sep. Qed.
Global Instance make_and_emp_l_absorbingly P : MakeSep True P ( P) | 10. Global Instance make_and_emp_l_absorbingly P : MakeSep True P (bi_absorbingly P) | 10.
Proof. intros. by rewrite /MakeSep. Qed. Proof. intros. by rewrite /MakeSep. Qed.
Global Instance make_sep_true_r P : Absorbing P MakeSep P True P. Global Instance make_sep_true_r P : Absorbing P MakeSep P True P.
Proof. intros. by rewrite /MakeSep sep_True. Qed. Proof. intros. by rewrite /MakeSep sep_True. Qed.
Global Instance make_and_emp_r_absorbingly P : MakeSep P True ( P) | 10. Global Instance make_and_emp_r_absorbingly P : MakeSep P True (bi_absorbingly P) | 10.
Proof. intros. by rewrite /MakeSep comm. Qed. Proof. intros. by rewrite /MakeSep comm. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P Q) | 100. Global Instance make_sep_default P Q : MakeSep P Q (P Q) | 100.
Proof. by rewrite /MakeSep. Qed. Proof. by rewrite /MakeSep. Qed.
...@@ -794,18 +794,18 @@ Proof. ...@@ -794,18 +794,18 @@ Proof.
by rewrite -{1}affinely_idemp affinely_sep_2. by rewrite -{1}affinely_idemp affinely_sep_2.
Qed. Qed.
Class MakeAbsorbingly (P Q : PROP) := make_absorbingly : P Q. Class MakeAbsorbingly (P Q : PROP) := make_absorbingly : bi_absorbingly P Q.
Arguments MakeAbsorbingly _%I _%I. Arguments MakeAbsorbingly _%I _%I.
Global Instance make_absorbingly_emp : MakeAbsorbingly emp True | 0. Global Instance make_absorbingly_emp : MakeAbsorbingly emp True | 0.
Proof. by rewrite /MakeAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed. Proof. by rewrite /MakeAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
(* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P` (* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
because framing will never turn a proposition that is not absorbing into because framing will never turn a proposition that is not absorbing into
something that is absorbing. *) something that is absorbing. *)
Global Instance make_absorbingly_default P : MakeAbsorbingly P ( P) | 100. Global Instance make_absorbingly_default P : MakeAbsorbingly P (bi_absorbingly P) | 100.
Proof. by rewrite /MakeAbsorbingly. Qed. Proof. by rewrite /MakeAbsorbingly. Qed.
Global Instance frame_absorbingly p R P Q Q' : Global Instance frame_absorbingly p R P Q Q' :
Frame p R P Q MakeAbsorbingly Q Q' Frame p R ( P) Q'. Frame p R P Q MakeAbsorbingly Q Q' Frame p R (bi_absorbingly P) Q'.
Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed. Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed.
Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P Q. Class MakePersistently (P Q : PROP) := make_persistently : bi_persistently P Q.
...@@ -834,7 +834,7 @@ Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) : ...@@ -834,7 +834,7 @@ Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed. Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.