From bb6452359c6f72091f89aa8f2bf72cb8d9064b6a Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 11 Aug 2022 11:05:18 +0200 Subject: [PATCH 1/4] Make sure that `Make` instances are consistent and "constant time". --- iris/proofmode/class_instances_make.v | 82 +++++++++++++++++++-------- iris/proofmode/classes_make.v | 8 +++ tests/proofmode.v | 4 -- 3 files changed, 65 insertions(+), 29 deletions(-) diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v index 9ccd7acca..85528ee68 100644 --- a/iris/proofmode/class_instances_make.v +++ b/iris/proofmode/class_instances_make.v @@ -8,6 +8,29 @@ Section class_instances_make. Context {PROP : bi}. Implicit Types P Q R : PROP. +(** Affine *) +Global Instance bi_affine_quick_affine P : BiAffine PROP → QuickAffine P. +Proof. rewrite /QuickAffine. apply _. Qed. +Global Instance False_quick_affine : @QuickAffine PROP False. +Proof. rewrite /QuickAffine. apply _. Qed. +Global Instance emp_quick_affine : @QuickAffine PROP emp. +Proof. rewrite /QuickAffine. apply _. Qed. +Global Instance affinely_quick_affine P : QuickAffine ( P). +Proof. rewrite /QuickAffine. apply _. Qed. +Global Instance intuitionistically_quick_affine P : QuickAffine (□ P). +Proof. rewrite /QuickAffine. apply _. Qed. + +(** Absorbing *) +Global Instance bi_affine_quick_absorbing P : BiAffine PROP → QuickAbsorbing P. +Proof. rewrite /QuickAbsorbing. apply _. Qed. +Global Instance pure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝. +Proof. rewrite /QuickAbsorbing. apply _. Qed. +Global Instance absorbingly_quick_absorbing P : QuickAbsorbing ( P). +Proof. rewrite /QuickAbsorbing. apply _. Qed. +Global Instance persistently_quick_absorbing P : QuickAbsorbing ( P). +Proof. rewrite /QuickAbsorbing. apply _. Qed. + +(** Embed *) Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ : KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝. Proof. apply embed_pure. Qed. @@ -18,46 +41,63 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P : MakeEmbed P ⎡P⎤ | 100. Proof. by rewrite /MakeEmbed. Qed. +(** Sep *) Global Instance make_sep_emp_l P : KnownLMakeSep emp P P. Proof. apply left_id, _. Qed. Global Instance make_sep_emp_r P : KnownRMakeSep P emp P. Proof. apply right_id, _. Qed. -Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P. -Proof. intros. apply True_sep, _. Qed. -Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P. -Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed. +Global Instance make_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P. +Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply True_sep. Qed. +Global Instance make_sep_true_r P : QuickAbsorbing P → KnownRMakeSep P True P. +Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply sep_True. Qed. Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100. Proof. by rewrite /MakeSep. Qed. +(** And *) Global Instance make_and_true_l P : KnownLMakeAnd True P P. Proof. apply left_id, _. Qed. Global Instance make_and_true_r P : KnownRMakeAnd P True P. Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed. -Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P. -Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed. -Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P. -Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed. +Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P. +Proof. apply emp_and. Qed. +Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P. +Proof. apply and_emp. Qed. Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100. Proof. by rewrite /MakeAnd. Qed. +(** Or *) Global Instance make_or_true_l P : KnownLMakeOr True P True. Proof. apply left_absorb, _. Qed. Global Instance make_or_true_r P : KnownRMakeOr P True True. Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed. -Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp. -Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed. -Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp. -Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed. +Global Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp. +Proof. apply emp_or. Qed. +Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp. +Proof. apply or_emp. Qed. Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100. Proof. by rewrite /MakeOr. Qed. -Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0. -Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed. +(** Affinely *) Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0. -Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed. +-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed. +Global Instance make_affinely_affine P : + QuickAffine P → MakeAffinely P P | 99. +Proof. apply affine_affinely. Qed. Global Instance make_affinely_default P : MakeAffinely P ( P) | 100. Proof. by rewrite /MakeAffinely. Qed. +(** Absorbingly *) +Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0. +Proof. + by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True. +Qed. +Global Instance make_absorbingly_absorbing P : + QuickAbsorbing P → MakeAbsorbingly P P | 99. +Proof. apply absorbing_absorbingly. Qed. +Global Instance make_absorbingly_default P : MakeAbsorbingly P ( P) | 100. +Proof. by rewrite /MakeAbsorbingly. Qed. + +(** Intuitionistically *) Global Instance make_intuitionistically_emp : @KnownMakeIntuitionistically PROP emp emp | 0. Proof. @@ -74,16 +114,7 @@ Global Instance make_intuitionistically_default P : MakeIntuitionistically P (□ P) | 100. Proof. by rewrite /MakeIntuitionistically. Qed. -Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0. -Proof. - by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly - -absorbingly_emp_True. -Qed. -Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0. -Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed. -Global Instance make_absorbingly_default P : MakeAbsorbingly P ( P) | 100. -Proof. by rewrite /MakeAbsorbingly. Qed. - +(** Later *) Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0. Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed. Global Instance make_laterN_emp `{!BiAffine PROP} n : @@ -92,6 +123,7 @@ Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed. Global Instance make_laterN_default n P : MakeLaterN n P (▷^n P) | 100. Proof. by rewrite /MakeLaterN. Qed. +(** Except-0 *) Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True. Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed. Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100. diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v index a0d8f1342..7d0bda7a2 100644 --- a/iris/proofmode/classes_make.v +++ b/iris/proofmode/classes_make.v @@ -39,6 +39,14 @@ that would have this behavior. *) From iris.bi Require Export bi. From iris.prelude Require Import options. +(** Aliases for [Affine] and [Absorbing], but the instances are severely +restricted. They only inspect the top-level symbol or check if the whole BI +is affine. *) +Class QuickAffine {PROP : bi} (P : PROP) := quick_affine : Affine P. +Global Hint Mode QuickAffine + ! : typeclass_instances. +Class QuickAbsorbing {PROP : bi} (P : PROP) := quick_absorbing : Absorbing P. +Global Hint Mode QuickAbsorbing + ! : typeclass_instances. + Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') := make_embed : ⎡P⎤ ⊣⊢ Q. Global Arguments MakeEmbed {_ _ _} _%I _%I. diff --git a/tests/proofmode.v b/tests/proofmode.v index ea515a6b8..8577e06e7 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -51,10 +51,6 @@ Proof. - iSplitL "HQ"; first iAssumption. by iSplitL "H1". Qed. -Lemma demo_3 P1 P2 P3 : - P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). -Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed. - Lemma test_pure_space_separated P1 : ⌜True⌝ ∗ P1 -∗ P1. Proof. -- GitLab From 634a873df861d91cacf2ba2b1d5461337cbe0cf1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 12 Aug 2022 10:22:44 +0200 Subject: [PATCH 2/4] More documentation. --- iris/proofmode/class_instances_make.v | 38 ++++++++++++++++++++------- 1 file changed, 29 insertions(+), 9 deletions(-) diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v index 85528ee68..3fef78dbe 100644 --- a/iris/proofmode/class_instances_make.v +++ b/iris/proofmode/class_instances_make.v @@ -77,23 +77,43 @@ Proof. apply or_emp. Qed. Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100. Proof. by rewrite /MakeOr. Qed. -(** Affinely *) -Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0. --Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed. +(** Affinely + +- [make_affinely_affine] adds no modality, but only if the argument is affine. +- [make_affinely_True] turns [True] into [emp]. For an affine BI this instance + overlaps with [make_affinely_affine], since [True] is affine. Since we prefer + 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. *) + Global Instance make_affinely_affine P : - QuickAffine P → MakeAffinely P P | 99. + QuickAffine P → MakeAffinely 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. Global Instance make_affinely_default P : MakeAffinely P ( P) | 100. Proof. by rewrite /MakeAffinely. Qed. -(** Absorbingly *) -Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0. +(** Absorbingly + +- [make_absorbingly_absorbing] adds no modality, but only if the argument is + absorbing. +- [make_absorbingly_emp] turns [emp] into [True]. For an affine BI this instance + overlaps with [make_absorbingly_absorbing], since [emp] is absorbing. For + consistency, we give this instance the same cost as [make_affinely_True], but + 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. *) + +Global Instance make_absorbingly_absorbing P : + QuickAbsorbing P → MakeAbsorbingly P P | 0. +Proof. apply absorbing_absorbingly. Qed. +Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1. Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True. Qed. -Global Instance make_absorbingly_absorbing P : - QuickAbsorbing P → MakeAbsorbingly P P | 99. -Proof. apply absorbing_absorbingly. Qed. Global Instance make_absorbingly_default P : MakeAbsorbingly P ( P) | 100. Proof. by rewrite /MakeAbsorbingly. Qed. -- GitLab From 741ca1f7ae2501051276a869d12f502270619dfd Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 12 Aug 2022 10:34:16 +0200 Subject: [PATCH 3/4] More tests. --- tests/proofmode.ref | 59 +++++++++++++++++++++++++++++++++++++++++++++ tests/proofmode.v | 56 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 115 insertions(+) diff --git a/tests/proofmode.ref b/tests/proofmode.ref index 2557911ad..2107e27c6 100644 --- a/tests/proofmode.ref +++ b/tests/proofmode.ref @@ -147,6 +147,65 @@ Tactic failure: iSpecialize: Q not persistent. : string The command has indeed failed with message: Tactic failure: iSpecialize: (|==> P)%I not persistent. +"test_iFrame_affinely_emp" + : string +1 goal + + PROP : bi + P : PROP + ============================ + "H" : P + --------------------------------------□ + ∃ _ : nat, emp +"test_iFrame_affinely_True" + : string +1 goal + + PROP : bi + BiAffine0 : BiAffine PROP + P : PROP + ============================ + "H" : P + --------------------------------------□ + ∃ _ : nat, True +"test_iFrame_or_1" + : string +1 goal + + PROP : bi + P1, P2, P3 : PROP + ============================ + --------------------------------------∗ + ▷ (∃ _ : nat, emp) +"test_iFrame_or_2" + : string +1 goal + + PROP : bi + P1, P2, P3 : PROP + ============================ + --------------------------------------∗ + ▷ (∃ x : nat, emp ∧ ⌜x = 0⌝ ∨ emp) +"test_iFrame_or_affine_1" + : string +1 goal + + PROP : bi + BiAffine0 : BiAffine PROP + P1, P2, P3 : PROP + ============================ + --------------------------------------∗ + ▷ (∃ _ : nat, True) +"test_iFrame_or_affine_2" + : string +1 goal + + PROP : bi + BiAffine0 : BiAffine PROP + P1, P2, P3 : PROP + ============================ + --------------------------------------∗ + ▷ (∃ _ : nat, True) "test_iInduction_multiple_IHs" : string 1 goal diff --git a/tests/proofmode.v b/tests/proofmode.v index 8577e06e7..c9a370ee1 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -557,6 +557,62 @@ Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} : P -∗ Q -∗ (P ∗ Q). Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed. +Check "test_iFrame_affinely_emp". +Lemma test_iFrame_affinely_emp P : + □ P -∗ ∃ _ : nat, P. (* The ∃ makes sure [iFrame] does not solve the + goal and we can [Show] the result *) +Proof. + iIntros "#H". iFrame "H". + Show. (* This should become [∃ _ : nat, emp]. *) + by iExists 1. +Qed. +Check "test_iFrame_affinely_True". +Lemma test_iFrame_affinely_True `{!BiAffine PROP} P : + □ P -∗ ∃ x : nat, P. +Proof. + iIntros "#H". iFrame "H". + Show. (* This should become [∃ _ : nat, True]. Since we are in an affine BI, + no unnecessary [emp]s should be created. *) + by iExists 1. +Qed. + +Check "test_iFrame_or_1". +Lemma test_iFrame_or_1 P1 P2 P3 : + P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3). +Proof. + iIntros "($ & $ & $)". + Show. (* By framing [P3], the disjunction becomes [ ⌜x = 0⌝ ∨ emp], + since [ ⌜x = 0⌝] is trivially affine, the disjunction is simplified + to [emp] *) + by iExists 0. +Qed. +Check "test_iFrame_or_2". +Lemma test_iFrame_or_2 P1 P2 P3 : + P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). +Proof. + iIntros "($ & $ & $)". + Show. (* By framing [P3], the disjunction becomes [emp ∧ ⌜x = 0⌝ ∨ emp], + since [emp ∧ ⌜x = 0⌝] is not trivially affine (i.e., by just looking at the + head symbol), this not simplified to [emp] *) + iExists 0. auto. +Qed. +Check "test_iFrame_or_affine_1". +Lemma test_iFrame_or_affine_1 `{!BiAffine PROP} P1 P2 P3 : + P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3). +Proof. + iIntros "($ & $ & $)". + Show. (* If the BI is affine, the disjunction should be turned into [True]. *) + by iExists 0. +Qed. +Check "test_iFrame_or_affine_2". +Lemma test_iFrame_or_affine_2 `{!BiAffine PROP} P1 P2 P3 : + P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). +Proof. + iIntros "($ & $ & $)". + Show. (* If the BI is affine, the disjunction should be turned into [True]. *) + by iExists 0. +Qed. + Lemma test_iAssert_modality P : ◇ False -∗ ▷ P. Proof. iIntros "HF". -- GitLab From 79d2ac8a91f54182abc5b932378aa7d82ce0625d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 12 Aug 2022 17:00:55 +0200 Subject: [PATCH 4/4] Improve comments in tests. --- tests/proofmode.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/tests/proofmode.v b/tests/proofmode.v index c9a370ee1..d98cccf87 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -581,9 +581,12 @@ Lemma test_iFrame_or_1 P1 P2 P3 : P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3). Proof. iIntros "($ & $ & $)". - Show. (* By framing [P3], the disjunction becomes [ ⌜x = 0⌝ ∨ emp], - since [ ⌜x = 0⌝] is trivially affine, the disjunction is simplified - to [emp] *) + Show. (* By framing [P3], the disjunction becomes [ ⌜x = 0⌝ ∨ emp]. + The [iFrame] tactic simplifies disjunctions if one side is trivial. In a + general BI, it can only turn [Q ∨ emp] into [emp]---without information + loss---if [Q] is affine. Here, we have [Q := ⌜x = 0⌝], which is + trivially affine (i.e., [QuickAffine]), and the disjunction is thus + simplified to [emp]. *) by iExists 0. Qed. Check "test_iFrame_or_2". @@ -591,9 +594,9 @@ Lemma test_iFrame_or_2 P1 P2 P3 : P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). Proof. iIntros "($ & $ & $)". - Show. (* By framing [P3], the disjunction becomes [emp ∧ ⌜x = 0⌝ ∨ emp], - since [emp ∧ ⌜x = 0⌝] is not trivially affine (i.e., by just looking at the - head symbol), this not simplified to [emp] *) + Show. (* By framing [P3], the disjunction becomes [emp ∧ ⌜x = 0⌝ ∨ emp]. + Since [emp ∧ ⌜x = 0⌝] is not trivially affine (i.e., not [QuickAffine]) it + is not simplified to [emp]. *) iExists 0. auto. Qed. Check "test_iFrame_or_affine_1". -- GitLab