Commit 89f57821 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/bi-lemmas' into 'master'

make affinely_True_emp more useful, and make absorbingly lemmas consistent

See merge request iris/iris!796
parents 49f9097f 552a6315
Pipeline #65915 passed with stage
in 7 minutes and 35 seconds
...@@ -19,6 +19,9 @@ lemma. ...@@ -19,6 +19,9 @@ lemma.
`Absorbing` instance. This breaks uses where an `Absorbing` instance was `Absorbing` instance. This breaks uses where an `Absorbing` instance was
provided without relying on TC search (e.g. in `by apply ...`; a possible fix provided without relying on TC search (e.g. in `by apply ...`; a possible fix
is `by apply: ...`). (by Glen Mével, Bedrock Systems) is `by apply: ...`). (by Glen Mével, Bedrock Systems)
* Change statement of `affinely_True_emp` to also remove the affinely modality.
* Rename `absorbingly_True_emp` to `absorbingly_emp_True` and make statement
consistent with `affinely_True_emp`: `<absorb> emp ⊣⊢ True`.
**Changes in `proofmode`:** **Changes in `proofmode`:**
......
...@@ -672,7 +672,7 @@ Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. ...@@ -672,7 +672,7 @@ Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
Lemma affinely_exist {A} (Φ : A PROP) : <affine> ( a, Φ a) a, <affine> (Φ a). Lemma affinely_exist {A} (Φ : A PROP) : <affine> ( a, Φ a) a, <affine> (Φ a).
Proof. by rewrite /bi_affinely and_exist_l. Qed. Proof. by rewrite /bi_affinely and_exist_l. Qed.
Lemma affinely_True_emp : <affine> True <affine> emp. Lemma affinely_True_emp : <affine> True emp.
Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed. Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.
Lemma affinely_and_l P Q : <affine> P Q <affine> (P Q). Lemma affinely_and_l P Q : <affine> P Q <affine> (P Q).
...@@ -708,6 +708,8 @@ Proof. ...@@ -708,6 +708,8 @@ 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_True : <absorb> True True.
Proof. apply absorbingly_pure. Qed.
Lemma absorbingly_or P Q : <absorb> (P Q) <absorb> P <absorb> Q. Lemma absorbingly_or P Q : <absorb> (P Q) <absorb> P <absorb> Q.
Proof. by rewrite /bi_absorbingly sep_or_l. Qed. Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
Lemma absorbingly_and_1 P Q : <absorb> (P Q) <absorb> P <absorb> Q. Lemma absorbingly_and_1 P Q : <absorb> (P Q) <absorb> P <absorb> Q.
...@@ -719,8 +721,8 @@ Proof. by rewrite /bi_absorbingly sep_exist_l. Qed. ...@@ -719,8 +721,8 @@ Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
Lemma absorbingly_sep P Q : <absorb> (P Q) <absorb> P <absorb> Q. Lemma absorbingly_sep P Q : <absorb> (P Q) <absorb> P <absorb> 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 : <absorb> True <absorb> emp. Lemma absorbingly_emp_True : <absorb> emp True.
Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed. Proof. rewrite /bi_absorbingly right_id //. Qed.
Lemma absorbingly_wand P Q : <absorb> (P - Q) <absorb> P - <absorb> Q. Lemma absorbingly_wand P Q : <absorb> (P - Q) <absorb> P - <absorb> 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.
...@@ -734,7 +736,7 @@ Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed. ...@@ -734,7 +736,7 @@ Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
Lemma affinely_absorbingly_elim `{!BiPositive PROP} P : <affine> <absorb> P <affine> P. Lemma affinely_absorbingly_elim `{!BiPositive PROP} P : <affine> <absorb> P <affine> 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 left_id.
Qed. Qed.
(* Affine and absorbing propositions *) (* Affine and absorbing propositions *)
...@@ -1072,7 +1074,7 @@ Qed. ...@@ -1072,7 +1074,7 @@ Qed.
Lemma intuitionistically_emp : emp emp. Lemma intuitionistically_emp : emp emp.
Proof. Proof.
by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
affinely_True_emp affinely_emp. affinely_True_emp.
Qed. Qed.
Lemma intuitionistically_False : False False. Lemma intuitionistically_False : False False.
Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed. Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed.
......
...@@ -64,7 +64,7 @@ Proof. by rewrite /FromAffinely. Qed. ...@@ -64,7 +64,7 @@ Proof. by rewrite /FromAffinely. Qed.
(** IntoAbsorbingly *) (** IntoAbsorbingly *)
Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0. 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_emp_True. 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_intuitionistically P : Global Instance into_absorbingly_intuitionistically P :
...@@ -184,7 +184,7 @@ Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1 ...@@ -184,7 +184,7 @@ Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1
Proof. Proof.
rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl. rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //. apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id. by rewrite -affinely_affinely_if affinely_True_emp left_id.
Qed. Qed.
Global Instance into_pure_affinely P φ : IntoPure P φ IntoPure (<affine> P) φ. Global Instance into_pure_affinely P φ : IntoPure P φ IntoPure (<affine> P) φ.
......
...@@ -149,7 +149,7 @@ Lemma tac_pure_intro Δ Q φ a : ...@@ -149,7 +149,7 @@ Lemma tac_pure_intro Δ Q φ a :
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl. intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl.
- by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp. - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp.
- by apply pure_intro. - by apply pure_intro.
Qed. Qed.
...@@ -176,7 +176,7 @@ Lemma tac_pure_revert Δ φ P Q : ...@@ -176,7 +176,7 @@ Lemma tac_pure_revert Δ φ P Q :
(φ envs_entails Δ Q). (φ envs_entails Δ Q).
Proof. Proof.
rewrite /FromAffinely envs_entails_unseal. intros <- -> ?. rewrite /FromAffinely envs_entails_unseal. intros <- -> ?.
by rewrite pure_True // affinely_True_emp affinely_emp left_id. by rewrite pure_True // affinely_True_emp left_id.
Qed. Qed.
(** * Intuitionistic *) (** * Intuitionistic *)
...@@ -391,7 +391,7 @@ Proof. ...@@ -391,7 +391,7 @@ Proof.
rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=. rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp (into_wand q true) /=. rewrite -intuitionistically_if_idemp (into_wand q true) /=.
rewrite -(from_pure a P1) pure_True //. rewrite -(from_pure a P1) pure_True //.
rewrite -affinely_affinely_if affinely_True_emp affinely_emp. rewrite -affinely_affinely_if affinely_True_emp.
by rewrite intuitionistically_emp left_id wand_elim_r. by rewrite intuitionistically_emp left_id wand_elim_r.
Qed. Qed.
......
...@@ -209,7 +209,7 @@ Qed. ...@@ -209,7 +209,7 @@ Qed.
Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0. Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed. Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0. Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed. Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100. Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed. Proof. by rewrite /MakeAffinely. Qed.
...@@ -249,7 +249,7 @@ Qed. ...@@ -249,7 +249,7 @@ Qed.
Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0. Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
Proof. Proof.
by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-absorbingly_True_emp absorbingly_pure. -absorbingly_emp_True.
Qed. Qed.
Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0. Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed. Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
......
Supports Markdown
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