Commit bcce68db authored by Ralf Jung's avatar Ralf Jung

Stop iFrame from introducing modalities

Fixes #176
parent 458a6d45
......@@ -85,8 +85,7 @@ Section greatest.
F (bi_greatest_fixpoint F) x bi_greatest_fixpoint F x.
Proof.
iIntros "HF". iExists (CofeMor (F (bi_greatest_fixpoint F))).
(* FIXME: The framing here adds an <affine> modality that we have to introduce. *)
iIntros "{$HF} !# !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed.
......
......@@ -58,12 +58,8 @@ 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_and_emp_l_absorbingly P : KnownLMakeSep True P (<absorb> P) | 10.
Proof. intros. by rewrite /KnownLMakeSep /MakeSep. 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_and_emp_r_absorbingly P : KnownRMakeSep P True (<absorb> P) | 10.
Proof. intros. by rewrite /KnownRMakeSep /MakeSep comm. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P Q) | 100.
Proof. by rewrite /MakeSep. Qed.
......@@ -101,12 +97,8 @@ 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_l_affinely P : KnownLMakeAnd emp P (<affine> P) | 10.
Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd. 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_r_affinely P : KnownRMakeAnd P emp (<affine> P) | 10.
Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd comm. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
......
......@@ -57,7 +57,7 @@ Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
Proof. iIntros "[#? _] [_ #?]". auto. Qed.
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P Q P Q)%I.
Proof. iIntros "H1 #H2". by iFrame. Qed.
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ ( φ P φ ψ P)%I.
Proof. iIntros (??) "H". auto. Qed.
......@@ -374,7 +374,7 @@ Lemma test_assert_affine_pure (φ : Prop) P :
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
Lemma test_assert_pure (φ : Prop) P :
φ P P ⌜φ⌝.
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
Lemma test_iEval x y : (y + x)%nat = 1 - S (x + y) = 2%nat : PROP.
Proof.
......
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