From ceedda120493b46a6becdb48573d5295623d5066 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 13 Aug 2022 16:58:33 -0400 Subject: [PATCH 1/3] move MakePersistently instances to the correct file --- iris/proofmode/class_instances_frame.v | 11 ----------- iris/proofmode/class_instances_make.v | 14 ++++++++++++++ 2 files changed, 14 insertions(+), 11 deletions(-) diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v index 26065b4ec..2c9d71237 100644 --- a/iris/proofmode/class_instances_frame.v +++ b/iris/proofmode/class_instances_frame.v @@ -177,17 +177,6 @@ Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed. -Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True. -Proof. - by rewrite /KnownMakePersistently /MakePersistently - -persistently_True_emp persistently_pure. -Qed. -Global Instance make_persistently_True : @KnownMakePersistently PROP True True. -Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed. -Global Instance make_persistently_default P : - MakePersistently P ( P) | 100. -Proof. by rewrite /MakePersistently. Qed. - Global Instance frame_persistently R P Q Q' : Frame true R P Q → MakePersistently Q Q' → Frame true R ( P) Q' | 2. (* Same cost as default. *) diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v index 3fef78dbe..336873be2 100644 --- a/iris/proofmode/class_instances_make.v +++ b/iris/proofmode/class_instances_make.v @@ -117,6 +117,20 @@ Qed. Global Instance make_absorbingly_default P : MakeAbsorbingly P ( P) | 100. Proof. by rewrite /MakeAbsorbingly. Qed. +(** Persistently *) +Global Instance make_persistently_emp : + @KnownMakePersistently PROP emp True | 0. +Proof. + by rewrite /KnownMakePersistently /MakePersistently + -persistently_True_emp persistently_pure. +Qed. +Global Instance make_persistently_True : + @KnownMakePersistently PROP True True | 0. +Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed. +Global Instance make_persistently_default P : + MakePersistently P ( P) | 100. +Proof. by rewrite /MakePersistently. Qed. + (** Intuitionistically *) Global Instance make_intuitionistically_emp : @KnownMakeIntuitionistically PROP emp emp | 0. -- GitLab From 8e14fcf891048d1457e53bf4835f2e97d234da08 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 13 Aug 2022 16:58:52 -0400 Subject: [PATCH 2/3] avoid MakeIntuitionistically turning a True into emp for affine BI --- iris/proofmode/class_instances_make.v | 11 ++++++++++- tests/proofmode.ref | 15 +++++++++++++-- tests/proofmode.v | 9 ++++++++- 3 files changed, 31 insertions(+), 4 deletions(-) diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v index 336873be2..df86ed206 100644 --- a/iris/proofmode/class_instances_make.v +++ b/iris/proofmode/class_instances_make.v @@ -138,8 +138,17 @@ Proof. by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically intuitionistically_emp. Qed. +(** For affine BIs, we would prefer [□ True] to become [True] rather than [emp], +so we have this instance with lower cost than the next. *) +Global Instance make_intuitionistically_True_affine : + BiAffine PROP → + @KnownMakeIntuitionistically PROP True True | 0. +Proof. + intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically + intuitionistically_True_emp True_emp //. +Qed. Global Instance make_intuitionistically_True : - @KnownMakeIntuitionistically PROP True emp | 0. + @KnownMakeIntuitionistically PROP True emp | 1. Proof. by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically intuitionistically_True_emp. diff --git a/tests/proofmode.ref b/tests/proofmode.ref index 749eb5b97..57992ccc9 100644 --- a/tests/proofmode.ref +++ b/tests/proofmode.ref @@ -503,9 +503,9 @@ No applicable tactic. 1 goal PROP : bi - H : BiAffine PROP + BiAffine0 : BiAffine PROP P, Q : PROP - H0 : Laterable Q + H : Laterable Q ============================ "HP" : ▷ P "HQ" : Q @@ -534,6 +534,17 @@ No applicable tactic. "H" : ⌜φ⌝ -∗ P --------------------------------------∗ ⌜φ⌝ -∗ P +"test_iFrame_not_add_emp_for_intuitionistically" + : string +1 goal + + PROP : bi + BiAffine0 : BiAffine PROP + P : PROP + ============================ + "H" : P + --------------------------------------□ + ∃ _ : nat, True "elim_mod_accessor" : string 1 goal diff --git a/tests/proofmode.v b/tests/proofmode.v index 3fe9aed5f..2d08f83fe 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -1261,7 +1261,7 @@ Proof. iIntros "[P _]". done. Qed. -Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) : +Lemma test_iModIntro_make_laterable `{!BiAffine PROP} (P Q : PROP) : Laterable Q → P -∗ Q -∗ make_laterable (▷ P ∗ Q). Proof. @@ -1284,6 +1284,13 @@ Proof. iIntros (Hφ) "H". iRevert (Hφ). Show. done. Qed. +(* Check that when framing things under the □ modality, we do not add [emp] in +affine BIs. *) +Check "test_iFrame_not_add_emp_for_intuitionistically". +Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP) : + □ P -∗ ∃ _ : nat, □ P. +Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed. + End tests. Section parsing_tests. -- GitLab From 72217e388467d1764e438d03d541f38868ef2984 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 15 Aug 2022 09:28:41 -0400 Subject: [PATCH 3/3] fix Known with not-Known Make instances --- iris/proofmode/class_instances_make.v | 16 ++++++++++++---- iris/proofmode/classes_make.v | 5 ++++- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v index df86ed206..bb638daf7 100644 --- a/iris/proofmode/class_instances_make.v +++ b/iris/proofmode/class_instances_make.v @@ -85,10 +85,14 @@ Proof. by rewrite /MakeOr. Qed. to avoid [emp] in goals involving affine BIs, we give [make_affinely_affine] a lower cost than [make_affinely_True]. - [make_affinely_default] adds the modality. This is the default instance since - it can always be used, and thus has the highest cost. *) + it can always be used, and thus has the highest cost. + (For this last point, the cost of the [KnownMakeAffinely] instances does not + actually matter, since this is a [MakeAffinely] instance, i.e. an instance of + a different class. What really matters is that the [known_make_affinely] + instance has a lower cost than [make_affinely_default].) *) Global Instance make_affinely_affine P : - QuickAffine P → MakeAffinely P P | 0. + QuickAffine P → KnownMakeAffinely P P | 0. Proof. apply affine_affinely. Qed. Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1. Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed. @@ -105,10 +109,14 @@ Proof. by rewrite /MakeAffinely. Qed. it does not really matter since goals in affine BIs typically do not contain occurrences of [emp] to start with. - [make_absorbingly_default] adds the modality. This is the default instance - since it can always be used, and thus has the highest cost. *) + since it can always be used, and thus has the highest cost. + (For this last point, the cost of the [KnownMakeAbsorbingly] instances does not + actually matter, since this is a [MakeAbsorbingly] instance, i.e. an instance of + a different class. What really matters is that the [known_make_absorbingly] + instance has a lower cost than [make_absorbingly_default].) *) Global Instance make_absorbingly_absorbing P : - QuickAbsorbing P → MakeAbsorbingly P P | 0. + QuickAbsorbing P → KnownMakeAbsorbingly P P | 0. Proof. apply absorbing_absorbingly. Qed. Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1. Proof. diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v index 7d0bda7a2..4af72163f 100644 --- a/iris/proofmode/classes_make.v +++ b/iris/proofmode/classes_make.v @@ -35,7 +35,10 @@ evar, then [MakeX] will not instantiate it arbitrarily. The reason for this is that if given an evar, these classes would typically try to instantiate this evar with some arbitrary logical constructs such as [emp] or [True]. Therefore, we use a [Hint Mode] to disable all the instances -that would have this behavior. *) +that would have this behavior. + +In practice this means that usually only the default instance should use [MakeX], +and most specialized instances should use [KnownMakeX]. *) From iris.bi Require Export bi. From iris.prelude Require Import options. -- GitLab