From a095bb8af708a8b88fa219d1bafaef32123fe9c2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Aug 2016 23:53:33 +0200
Subject: [PATCH] Remove FIXME.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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)'.
---
 program_logic/counter_examples.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 14710eba5..34795155f 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -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]".
+  Proof.
+    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).
   Proof.
-    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.
-- 
GitLab