Commit 887fcf1e authored by Robbert Krebbers's avatar Robbert Krebbers

Conditional `<absorb>?p P` modality.

parent c20e4f25
......@@ -62,6 +62,13 @@ Instance: Params (@bi_affinely_if) 2 := {}.
Typeclasses Opaque bi_affinely_if.
Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then <absorb> P else P)%I.
Arguments bi_absorbingly_if {_} !_ _%I /.
Instance: Params (@bi_absorbingly_if) 2 := {}.
Typeclasses Opaque bi_absorbingly_if.
Notation "'<absorb>?' p P" := (bi_absorbingly_if p P) : bi_scope.
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
(<affine> <pers> P)%I.
Arguments bi_intuitionistically {_} _%I : simpl never.
......
......@@ -1144,6 +1144,57 @@ Proof. destruct p; simpl; auto using affinely_sep. Qed.
Lemma affinely_if_idemp p P : <affine>?p <affine>?p P <affine>?p P.
Proof. destruct p; simpl; auto using affinely_idemp. Qed.
(* Conditional absorbingly modality *)
Global Instance absorbingly_if_ne p : NonExpansive (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
Global Instance absorbingly_if_proper p : Proper (() ==> ()) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
Global Instance absorbingly_if_mono' p : Proper (() ==> ()) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
Global Instance absorbingly_if_flip_mono' p :
Proper (flip () ==> flip ()) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
Lemma absorbingly_if_absorbingly p P : <absorb>?p P <absorb> P.
Proof. destruct p; simpl; auto using absorbingly_intro. Qed.
Lemma absorbingly_if_intro p P : P <absorb>?p P.
Proof. destruct p; simpl; auto using absorbingly_intro. Qed.
Lemma absorbingly_if_mono p P Q : (P Q) <absorb>?p P <absorb>?p Q.
Proof. by intros ->. Qed.
Lemma absorbingly_if_flag_mono (p q : bool) P : (p q) <absorb>?p P <absorb>?q P.
Proof. destruct p, q; try naive_solver auto using absorbingly_intro. Qed.
Lemma absorbingly_if_idemp p P : <absorb>?p <absorb>?p P <absorb>?p P.
Proof. destruct p; simpl; auto using absorbingly_idemp. Qed.
Lemma absorbingly_if_pure p φ : <absorb>?p φ φ .
Proof. destruct p; simpl; auto using absorbingly_pure. Qed.
Lemma absorbingly_if_or p P Q : <absorb>?p (P Q) <absorb>?p P <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_or. Qed.
Lemma absorbingly_if_and_1 p P Q : <absorb>?p (P Q) <absorb>?p P <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_and_1. Qed.
Lemma absorbingly_if_forall {A} p (Φ : A PROP) :
<absorb>?p ( a, Φ a) a, <absorb>?p (Φ a).
Proof. destruct p; simpl; auto using absorbingly_forall. Qed.
Lemma absorbingly_if_exist {A} p (Φ : A PROP) :
<absorb>?p ( a, Φ a) a, <absorb>?p (Φ a).
Proof. destruct p; simpl; auto using absorbingly_exist. Qed.
Lemma absorbingly_if_sep p P Q : <absorb>?p (P Q) <absorb>?p P <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_sep. Qed.
Lemma absorbingly_if_wand p P Q : <absorb>?p (P - Q) <absorb>?p P - <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_wand. Qed.
Lemma absorbingly_if_sep_l p P Q : <absorb>?p P Q <absorb>?p (P Q).
Proof. destruct p; simpl; auto using absorbingly_sep_l. Qed.
Lemma absorbingly_if_sep_r p P Q : P <absorb>?p Q <absorb>?p (P Q).
Proof. destruct p; simpl; auto using absorbingly_sep_r. Qed.
Lemma absorbingly_if_sep_lr p P Q : <absorb>?p P Q P <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_sep_lr. Qed.
Lemma affinely_if_absorbingly_if_elim `{!BiPositive PROP} p P :
<affine>?p <absorb>?p P <affine>?p P.
Proof. destruct p; simpl; auto using affinely_absorbingly_elim. Qed.
(* Conditional persistently *)
Global Instance persistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
......
......@@ -188,6 +188,8 @@ Section embed.
Lemma embed_affinely_if `{!BiEmbedEmp PROP1 PROP2} P b :
<affine>?b P <affine>?b P.
Proof. destruct b; simpl; auto using embed_affinely. Qed.
Lemma embed_absorbingly_if b P : <absorb>?b P <absorb>?b P.
Proof. destruct b; simpl; auto using embed_absorbingly. Qed.
Lemma embed_intuitionistically_if_2 P b : ?b P ⎡□?b P.
Proof. destruct b; simpl; auto using embed_intuitionistically_2. Qed.
Lemma embed_intuitionistically_if `{!BiEmbedEmp PROP1 PROP2} P b :
......
......@@ -511,6 +511,8 @@ Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
Lemma monPred_at_absorbingly i P : (<absorb> P) i <absorb> (P i).
Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i <absorb>?p (P i).
Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.
Lemma monPred_wand_force i P Q : (P - Q) i - (P i - Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
......@@ -651,6 +653,8 @@ Global Instance persistently_if_objective P p `{!Objective P} : Objective (<pers
Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
Global Instance affinely_if_objective P p `{!Objective P} : Objective (<affine>?p P).
Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
Global Instance absorbingly_if_objective P p `{!Objective P} : Objective (<absorb>?p P).
Proof. rewrite /bi_absorbingly_if. destruct p; apply _. Qed.
Global Instance intuitionistically_if_objective P p `{!Objective P} : Objective (?p P).
Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.
......
......@@ -36,6 +36,8 @@ Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
right associativity, format "'<affine>?' p P").
Reserved Notation "'<absorb>' P" (at level 20, right associativity).
Reserved Notation "'<absorb>?' p P" (at level 20, p at level 9, P at level 20,
right associativity, format "'<absorb>?' p P").
Reserved Notation "□ P" (at level 20, right associativity).
Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
......
......@@ -123,6 +123,10 @@ Global Instance make_monPred_at_affinely_if i P 𝓟 p :
MakeMonPredAt i P 𝓟
MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_absorbingly_if i P 𝓟 p :
MakeMonPredAt i P 𝓟
MakeMonPredAt i (<absorb>?p P) (<absorb>?p 𝓟).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_intuitionistically_if i P 𝓟 p :
MakeMonPredAt i P 𝓟
MakeMonPredAt i (?p P) (?p 𝓟).
......
......@@ -31,7 +31,7 @@ Declare Reduction pm_prettify := cbn [
(* telescope combinators *)
tele_fold tele_bind tele_app
(* BI connectives *)
bi_persistently_if bi_affinely_if bi_intuitionistically_if
bi_persistently_if bi_affinely_if bi_absorbingly_if bi_intuitionistically_if
bi_wandM sbi_laterN
bi_tforall bi_texist
].
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment