Commit a095bb8a authored by Robbert Krebbers's avatar Robbert Krebbers

Remove FIXME.

1.) iDestruct is able turns  into two implications (because uPred_iff
    is (type classes) transparent).
2.) iApply only backtracks on turning P  Q into P → Q or Q → P when
    there are no future premises. This is not the case for
    'P  □ (P → False)'.
parent 2285a577
Pipeline #2560 passed with stage
in 4 minutes and 1 second
......@@ -20,8 +20,8 @@ Section savedprop.
(* Self-contradicting assertions are inconsistent *)
Lemma no_self_contradiction P `{!PersistentP P} : (P ¬ P) False.
Proof. (* FIXME: Cannot destruct the <-> as two implications. iApply with <-> also does not work. *)
rewrite /uPred_iff. iIntros "#[H1 H2]".
iIntros "#[H1 H2]".
iAssert P as "#HP".
{ iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
by iApply ("H1" with "[#]").
......@@ -31,7 +31,7 @@ Section savedprop.
Definition A (i : sprop) : iProp := P, saved i P P.
Lemma saved_is_A i P `{!PersistentP P} : saved i P (A i P).
rewrite /uPred_iff. iIntros "#HS !". iSplit.
iIntros "#HS !". iSplit.
- iDestruct 1 as (Q) "[#HSQ HQ]".
iApply (sprop_agree i P Q with "[]"); eauto.
- iIntros "#HP". iExists P. by iSplit.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment