Commit 07ea98fe authored by Robbert Krebbers's avatar Robbert Krebbers

When framing, `▷ emp` should be turned into `emp` if the BI is affine.

If the BI is not affine, this should not happen, as it may lead to
information loss.

This commit fixes issue #190.
parent 4417e093
......@@ -158,6 +158,9 @@ Lemma test_iFrame_conjunction_2 P Q :
P - Q - (P P) (Q Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
Lemma test_iFrame_later `{BiAffine PROP} P Q : P - Q - P Q.
Proof. iIntros "H1 H2". by iFrame "H1". Qed.
Lemma test_iAssert_modality P : False - P.
Proof.
iIntros "HF".
......
......@@ -270,6 +270,9 @@ Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q).
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 :
@KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
Proof. by rewrite /MakeLaterN. Qed.
Global Instance make_laterN_1 P : MakeLaterN 1 P ( P) | 2.
......
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