diff --git a/_CoqProject b/_CoqProject index e3a98170f1f67a6a5a086700759d8b9a519a33d5..6b739e43e9ec0775d9a4c3f88fe145a3a4c1fc84 100644 --- a/_CoqProject +++ b/_CoqProject @@ -97,7 +97,7 @@ theories/tests/heap_lang.v theories/tests/one_shot.v theories/tests/proofmode.v theories/tests/proofmode_iris.v -theories/tests/proofmode_monPred.v +theories/tests/proofmode_monpred.v theories/tests/list_reverse.v theories/tests/tree_sum.v theories/tests/ipm_paper.v diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v index 0dabf37cd9a737f7a5161f08ae8d5b8eac127311..f3842e4b8dbf7056cba1256573bf3d1ca9359a86 100644 --- a/theories/proofmode/monpred.v +++ b/theories/proofmode/monpred.v @@ -2,18 +2,21 @@ From iris.bi Require Export monpred. From iris.proofmode Require Import tactics. Import MonPred. +Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I) + (P : monPred I PROP) (š : PROP) := + make_monPred_car : P i ā£ā¢ š. +Arguments MakeMonPredCar {_ _} _ _%I _%I. +Hint Mode MakeMonPredCar + + - ! -. + Section bi. Context {I : bi_index} {PROP : bi}. Local Notation monPred := (monPred I PROP). +Local Notation MakeMonPredCar := (@MakeMonPredCar I PROP). Implicit Types P Q R : monPred. Implicit Types š š  š” : PROP. Implicit Types Ļ : Prop. Implicit Types i j : I. -Class MakeMonPredCar i P š := - make_monPred_car : P i ā£ā¢ š. -Arguments MakeMonPredCar _ _%I _%I. - Global Instance make_monPred_car_pure Ļ i : MakeMonPredCar i āĻā āĻā. Proof. rewrite /MakeMonPredCar. by unseal. Qed. Global Instance make_monPred_car_internal_eq {A : ofeT} (x y : A) i : @@ -141,17 +144,21 @@ Proof. by destruct a, pe=><-; try unseal. Qed. -(* FIXME : P and Q do not go through MakeMonPredCar, which prevent - lazilly unfolding of monPred connectives there. The reason we - cannot do that is that IntoWand is sometimes called with known - values, which we do not wnat to replace with existentials. *) -Global Instance into_wand_monPred_car p q R P Q i : - IntoWand p q R P Q ā IntoWand p q (R i) (P i) (Q i). +Lemma into_wand_monPred_car_unknown_unknown p q R P š Q š  i : + IntoWand p q R P Q ā MakeMonPredCar i P š ā MakeMonPredCar i Q š  ā + IntoWand p q (R i) š š . Proof. rewrite /IntoWand /MakeMonPredCar /bi_affinely_if /bi_persistently_if. - destruct p, q=> /bi.wand_elim_l' [/(_ i) H]; apply bi.wand_intro_r; + destruct p, q=> /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r; revert H; unseal; done. Qed. +Lemma into_wand_monPred_car_unknown_known p q R P š Q i : + IntoWand p q R P Q ā MakeMonPredCar i P š ā IntoWand p q (R i) š (Q i). +Proof. intros. eapply into_wand_monPred_car_unknown_unknown=>//. apply _. Qed. +Lemma into_wand_monPred_car_known_unknown p q R P Q š  i : + IntoWand p q R P Q ā MakeMonPredCar i Q š  ā IntoWand p q (R i) (P i) š . +Proof. intros. eapply into_wand_monPred_car_unknown_unknown=>//. apply _. Qed. + Global Instance into_wand_wand'_monPred p q P Q š š  i : IntoWand' p q ((P -ā Q) i) š š  ā IntoWand p q ((P -ā Q) i) š š  | 100. Proof. done. Qed. @@ -163,31 +170,37 @@ Global Instance from_forall_monPred_car_wand P Q (Ī¦ ĪØ : I ā PROP) i : (ā j, MakeMonPredCar j P (Ī¦ j)) ā (ā j, MakeMonPredCar j Q (ĪØ j)) ā FromForall ((P -ā Q) i)%I (Ī» j, āi ā jā ā Ī¦ j -ā ĪØ j)%I. Proof. - rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2. - setoid_rewrite H1. setoid_rewrite H2. done. -Qed. -Global Instance into_forall_monPred_car_wand P Q (Ī¦ ĪØ : I ā PROP) i : - (ā j, MakeMonPredCar j P (Ī¦ j)) ā (ā j, MakeMonPredCar j Q (ĪØ j)) ā - IntoForall ((P -ā Q) i) (Ī» j, āi ā jā ā Ī¦ j -ā ĪØ j)%I. -Proof. - rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2. - setoid_rewrite H1. setoid_rewrite H2. done. + rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2. do 2 f_equiv. + by rewrite H1 H2. Qed. Global Instance from_forall_monPred_car_impl P Q (Ī¦ ĪØ : I ā PROP) i : (ā j, MakeMonPredCar j P (Ī¦ j)) ā (ā j, MakeMonPredCar j Q (ĪØ j)) ā FromForall ((P ā Q) i)%I (Ī» j, āi ā jā ā Ī¦ j ā ĪØ j)%I. Proof. - rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2. - setoid_rewrite H1. setoid_rewrite H2. done. -Qed. -Global Instance into_forall_monPred_car_impl P Q (Ī¦ ĪØ : I ā PROP) i : - (ā j, MakeMonPredCar j P (Ī¦ j)) ā (ā j, MakeMonPredCar j Q (ĪØ j)) ā - IntoForall ((P ā Q) i) (Ī» j, āi ā jā ā Ī¦ j ā ĪØ j)%I. -Proof. - rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2. - setoid_rewrite H1. setoid_rewrite H2. done. + rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2. do 2 f_equiv. + by rewrite H1 H2 bi.pure_impl_forall. Qed. +(* FIXME : I disable these instances, because I prefer not adding the + corresponding IntoWand instance. Adding the IntoWand instance would + be ambiguous, because we want to be abble to iApply without proving + view inclusion when they match (i.e., we want to use + [into_wand_monPred_car]). *) +(* Global Instance into_forall_monPred_car_wand P Q (Ī¦ ĪØ : I ā PROP) i : *) +(* (ā j, MakeMonPredCar j P (Ī¦ j)) ā (ā j, MakeMonPredCar j Q (ĪØ j)) ā *) +(* IntoForall ((P -ā Q) i) (Ī» j, āi ā jā ā Ī¦ j -ā ĪØ j)%I. *) +(* Proof. *) +(* rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2. do 2 f_equiv. *) +(* by rewrite H1 H2. *) +(* Qed. *) +(* Global Instance into_forall_monPred_car_impl P Q (Ī¦ ĪØ : I ā PROP) i : *) +(* (ā j, MakeMonPredCar j P (Ī¦ j)) ā (ā j, MakeMonPredCar j Q (ĪØ j)) ā *) +(* IntoForall ((P ā Q) i) (Ī» j, āi ā jā ā Ī¦ j ā ĪØ j)%I. *) +(* Proof. *) +(* rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2. do 2 f_equiv. *) +(* by rewrite H1 H2 bi.pure_impl_forall. *) +(* Qed. *) + Global Instance from_and_monPred_car P Q1 š 1 Q2 š 2 i : FromAnd P Q1 Q2 ā MakeMonPredCar i Q1 š 1 ā MakeMonPredCar i Q2 š 2 ā FromAnd (P i) š 1 š 2. @@ -272,7 +285,24 @@ Global Instance from_modal_monPred_car i P Q š  : Proof. by rewrite /FromModal /MakeMonPredCar=> <- <-. Qed. End bi. -Hint Mode MakeMonPredCar + + - ! -. +(* When P and/or Q are evars when doing typeclass search on [IntoWand + (R i) P Q], we use [MakeMonPredCar] in order to normalize the + result of unification. However, when they are not evars, we want to + propagate the known information through typeclass search. Hence, we + do not want to use [MakeMonPredCar]. + + As a result, depending on P and Q being evars, we use a different + version of [into_wand_monPred_car_xx_xx]. *) +Hint Extern 3 (IntoWand _ _ (monPred_car _ _) ?P ?Q) => + is_evar P; is_evar Q; + eapply @into_wand_monPred_car_unknown_unknown + : typeclass_instances. +Hint Extern 2 (IntoWand _ _ (monPred_car _ _) ?P (monPred_car ?Q _)) => + eapply @into_wand_monPred_car_unknown_known + : typeclass_instances. +Hint Extern 2 (IntoWand _ _ (monPred_car _ _) (monPred_car ?P _) ?Q) => + eapply @into_wand_monPred_car_known_unknown + : typeclass_instances. Section sbi. Context {I : bi_index} {PROP : sbi}. diff --git a/theories/tests/proofmode_monPred.v b/theories/tests/proofmode_monpred.v similarity index 57% rename from theories/tests/proofmode_monPred.v rename to theories/tests/proofmode_monpred.v index e9f2053eaa6aaa9166ab7ff808c2e83b74d2856f..a18ce8ef0eeeb5d60a23538a274dd37c4b9a921f 100644 --- a/theories/tests/proofmode_monPred.v +++ b/theories/tests/proofmode_monpred.v @@ -27,4 +27,27 @@ Section tests. Lemma test_iStartProof_7 P : ((P ā” P)%I : monPredI). Proof. iStartProof PROP. done. Qed. -End tests. \ No newline at end of file + Lemma test_intowand_1 P Q : (P -ā Q) -ā P -ā Q. + Proof. + iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW". + Qed. + Lemma test_intowand_2 P Q : (P -ā Q) -ā P -ā Q. + Proof. + iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". + iSpecialize ("HW" with "[HP //]"). done. + Qed. + Lemma test_intowand_3 P Q : (P -ā Q) -ā P -ā Q. + Proof. + iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". + iSpecialize ("HW" with "HP"). done. + Qed. + Lemma test_intowand_4 P Q : (P -ā Q) -ā ā· P -ā ā· Q. + Proof. + iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW". + Qed. + Lemma test_intowand_5 P Q : (P -ā Q) -ā ā· P -ā ā· Q. + Proof. + iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". + iSpecialize ("HW" with "HP"). done. + Qed. +End tests.