diff --git a/tests/proofmode.v b/tests/proofmode.v index e766a357d6d4ba2a0dbac5b6addea2d454ed825e..1c083285540092977af4c86c79c35e977f65bffc 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -325,6 +325,45 @@ Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} : P -∗ Q -∗ <affine> (P ∗ Q). Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_affinely_3 P Q : + □ P -∗ <affine> Q -∗ <affine> (<pers> P ∗ Q). +Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_affinely_4 P Q `{!BiPositive PROP, !Affine P} : + <affine> P -∗ <affine> Q -∗ <affine> (<absorb> P ∗ Q). +Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. + +Lemma test_iFrame_intuitionistically_1 P Q `{!Persistent P} : + <affine> P -∗ □ Q -∗ □ (P ∗ Q). +Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_intuitionistically_2 P Q `{!Persistent P, !Affine P} : + P -∗ □ Q -∗ □ (P ∗ Q). +Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_intuitionistically_3 P Q : + □ P -∗ □ Q -∗ □ (<pers> P ∗ Q). +Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed. + +Lemma test_iFrame_absorbingly_1 P Q `{!Absorbing P, !Persistent P} : + P -∗ Q -∗ <absorb> (P ∧ Q). +Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_absorbingly_2 P Q : + <pers> P -∗ Q -∗ <absorb> (□ P ∗ Q). +Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_absorbingly_3 P Q `{!Absorbing P, !Persistent P} : + P -∗ Q -∗ True ∗ (P ∧ Q). +Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_absorbingly_4 P Q : + <pers> P -∗ Q -∗ True ∗ (□ P ∗ Q). +Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed. + +Lemma test_iFrame_persistently_1 P Q `{!Persistent P} : + <absorb> P -∗ □ Q -∗ <pers> (P ∗ Q). +Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_persistently_2 P Q `{!Persistent P, !Absorbing P} : + P -∗ □ Q -∗ <pers> (P ∗ Q). +Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed. +Lemma test_iFrame_persistently_3 P Q : + <pers> P -∗ □ Q -∗ <pers> (□ P ∗ Q). +Proof. iIntros "HP #HQ". iFrame "HQ". iExact "HP". Qed. Lemma test_iAssert_modality P : ◇ False -∗ ▷ P. Proof. diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v index 4a665e1e3d9c9a0cfc463d54c5e7c0ae05dfa9c7..7a84dc2d609e43fe216cefe0b837bcd72d8b81ec 100644 --- a/theories/proofmode/frame_instances.v +++ b/theories/proofmode/frame_instances.v @@ -66,10 +66,12 @@ 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 P1 P2 : + MakeAbsorbingly P1 P2 → KnownLMakeSep True P1 P2. +Proof. by rewrite /MakeAbsorbingly /KnownLMakeSep /MakeSep=> <-. Qed. +Global Instance make_sep_true_r P1 P2 : + MakeAbsorbingly P1 P2 → KnownRMakeSep P1 True P2. +Proof. rewrite /MakeAbsorbingly /KnownRMakeSep /MakeSep=> <-. by rewrite comm. Qed. Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100. Proof. by rewrite /MakeSep. Qed. @@ -124,10 +126,10 @@ 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 P1 P2 : MakeAffinely P1 P2 → KnownLMakeAnd emp P1 P2. +Proof. by rewrite /MakeAffinely /KnownLMakeAnd /MakeAnd=> <-. Qed. +Global Instance make_and_emp_r P1 P2 : MakeAffinely P1 P2 → KnownRMakeAnd P1 emp P2. +Proof. rewrite /MakeAffinely /KnownRMakeAnd /MakeAnd=> <-. by rewrite comm. Qed. Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100. Proof. by rewrite /MakeAnd. Qed. @@ -188,8 +190,17 @@ Proof. by rewrite assoc (comm _ P1) -assoc wand_elim_r. Qed. +(** * Affinely *) Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0. Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed. +Global Instance make_affinely_persistently P : KnownMakeAffinely (<pers> P) (□ P) | 0. +Proof. by rewrite /KnownMakeAffinely /MakeAffinely. Qed. +Global Instance make_affinely_absorbingly P1 P2 : + BiPositive PROP → MakeAffinely P1 P2 → KnownMakeAffinely (<absorb> P1) P2 | 0. +Proof. + rewrite /KnownMakeAffinely /MakeAffinely=> ? <-. + by rewrite affinely_absorbingly_elim. +Qed. Global Instance make_affinely_affine P : Affine P → KnownMakeAffinely P P | 1. Proof. intros. by rewrite /KnownMakeAffinely /MakeAffinely affine_affinely. Qed. Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100. @@ -203,17 +214,21 @@ Proof. by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2. Qed. +(** * Intuitionistically *) Global Instance make_intuitionistically_True : @KnownMakeIntuitionistically PROP True emp | 0. Proof. by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically intuitionistically_True_emp. Qed. -Global Instance make_intuitionistically_intuitionistic P : - Affine P → Persistent P → KnownMakeIntuitionistically P P | 1. +(** The instance below also turns [<pers> P] into [□ P] *) +Global Instance make_intuitionistically_intuitionistic P1 P2 : + Persistent P1 → MakeAffinely P1 P2 → KnownMakeIntuitionistically P1 P2 | 1. Proof. - intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically. - rewrite intuitionistic_intuitionistically //. + rewrite /MakeAffinely /KnownMakeIntuitionistically + /MakeIntuitionistically=> ? <-. apply (anti_symm _). + - apply intuitionistically_affinely. + - by rewrite {1}(persistent P1). Qed. Global Instance make_intuitionistically_default P : MakeIntuitionistically P (□ P) | 100. @@ -226,14 +241,31 @@ Proof. rewrite -intuitionistically_sep_2 intuitionistically_idemp //. Qed. +(** * Absorbingly *) Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0. Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed. -(* 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 -something that is absorbing. *) +Global Instance make_absorbingly_affinely P1 P2 : + Persistent P1 → MakeAbsorbingly P1 P2 → + KnownMakeAbsorbingly (<affine> P1) P2 | 0. +Proof. + rewrite /KnownMakeAbsorbingly /MakeAbsorbingly=> ? <-. apply (anti_symm _). + - by rewrite affinely_elim. + - by rewrite -(absorbingly_idemp (<affine> _))%I -persistent_absorbingly_affinely_2. +Qed. +Global Instance make_absorbingly_absorbing P : + Absorbing P → KnownMakeAbsorbingly P P | 1. +Proof. + intros. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbing_absorbingly. +Qed. +(** The instance [make_absorbingly_intuitionistically] should be used after +[make_absorbingly_absorbing], otherwise it will also turn [□] modalities into +[<pers>] modalities if the BI is affine. *) +Global Instance make_absorbingly_intuitionistically P : + KnownMakeAbsorbingly (□ P) (<pers> P) | 2. +Proof. apply absorbingly_intuitionistically_into_persistently. Qed. Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100. Proof. by rewrite /MakeAbsorbingly. Qed. @@ -243,6 +275,7 @@ Proof. rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r. Qed. +(** * Persistently *) Global Instance make_persistently_true : @KnownMakePersistently PROP True True. Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed. Global Instance make_persistently_emp : @KnownMakePersistently PROP emp True. @@ -250,6 +283,15 @@ Proof. by rewrite /KnownMakePersistently /MakePersistently -persistently_True_emp persistently_pure. Qed. +(** The instance below also turns [□ P] into [<pers> P]. *) +Global Instance make_persistently_persistent_absorbing P1 P2 : + Persistent P1 → MakeAbsorbingly P1 P2 → KnownMakePersistently P1 P2 | 1. +Proof. + rewrite /MakeAbsorbingly /KnownMakePersistently + /MakePersistently=> ? <-. apply (anti_symm _). + - apply persistently_into_absorbingly. + - by rewrite {1}(persistent P1) absorbingly_elim_persistently. +Qed. Global Instance make_persistently_default P : MakePersistently P (<pers> P) | 100. Proof. by rewrite /MakePersistently. Qed.