Commit 16c90c69 authored by Ralf Jung's avatar Ralf Jung
Browse files

Revert "Use implication in core so that we can test it.", add a dedicated test

This reverts commit daaabf41.  We have tests for
testcase, we shouldn't depend on using arcane features in our definitions for
this purpose.  Also, this exposes that there still is a bug somewhere (see the
FIXME).
parent daaabf41
Pipeline #7342 passed with stage
in 23 minutes and 59 seconds
...@@ -7,7 +7,9 @@ Import bi. ...@@ -7,7 +7,9 @@ Import bi.
i.e. the conjunction of all persistent assertions that are weaker i.e. the conjunction of all persistent assertions that are weaker
than P (as in, implied by P). *) than P (as in, implied by P). *)
Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP := Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
( Q : PROP, (Q - <pers> Q) (P - Q) Q)%I. (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
using conjunction/implication here. *)
( Q : PROP, <affine> (Q - <pers> Q) - <affine> (P - Q) - Q)%I.
Instance: Params (@coreP) 1. Instance: Params (@coreP) 1.
Typeclasses Opaque coreP. Typeclasses Opaque coreP.
...@@ -16,14 +18,20 @@ Section core. ...@@ -16,14 +18,20 @@ Section core.
Implicit Types P Q : PROP. Implicit Types P Q : PROP.
Lemma coreP_intro P : P - coreP P. Lemma coreP_intro P : P - coreP P.
Proof. rewrite /coreP. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed. Proof.
rewrite /coreP. iIntros "HP" (Q) "_ HPQ".
(* FIXME: Cannot apply HPQ directly. This works if we move it to the
persistent context, but why should we? *)
iDestruct (affinely_plainly_elim with "HPQ") as "HPQ".
by iApply "HPQ".
Qed.
Global Instance coreP_persistent P : Persistent (coreP P). Global Instance coreP_persistent P : Persistent (coreP P).
Proof. Proof.
rewrite /coreP /Persistent. iIntros "HC" (Q). rewrite /coreP /Persistent. iIntros "HC" (Q).
iApply persistently_impl_plainly. iIntros "#HQ". iApply persistently_wand_affinely_plainly. iIntros "#HQ".
iApply persistently_impl_plainly. iIntros "#HPQ". iApply persistently_wand_affinely_plainly. iIntros "#HPQ".
iApply "HQ". by iApply ("HC" with "[#] [#]"). iApply "HQ". iApply "HC"; auto.
Qed. Qed.
Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)). Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)).
...@@ -35,7 +43,7 @@ Section core. ...@@ -35,7 +43,7 @@ Section core.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Lemma coreP_elim P : Persistent P coreP P - P. Lemma coreP_elim P : Persistent P coreP P - P.
Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" with "[#] [#]"); auto. Qed. Proof. rewrite /coreP. iIntros (?) "HCP". iApply "HCP"; auto. Qed.
(* TODO: Can we generalize this to non-affine BIs? *) (* TODO: Can we generalize this to non-affine BIs? *)
Lemma coreP_wand `{!BiAffine PROP} P Q : (coreP P Q) (P <pers> Q). Lemma coreP_wand `{!BiAffine PROP} P Q : (coreP P Q) (P <pers> Q).
......
...@@ -419,4 +419,8 @@ Qed. ...@@ -419,4 +419,8 @@ Qed.
Lemma test_iAssumption_False_no_loop : R, R P, P. Lemma test_iAssumption_False_no_loop : R, R P, P.
Proof. eexists. iIntros "?" (P). done. Qed. Proof. eexists. iIntros "?" (P). done. Qed.
Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
P - ( Q : PROP, (Q - <pers> Q) (P - Q) Q).
Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
End tests. End tests.
Markdown is supported
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