From b42d1571025684e5d509c6cc537688b26cd0bf57 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 Mar 2020 23:50:28 +0200
Subject: [PATCH] =?UTF-8?q?Let=20`iNext`=20detect=20equalities=20`Next=20x?=
 =?UTF-8?q?=20=E2=89=A1=20Next=20y`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/proofmode.v                        | 4 ++++
 theories/proofmode/class_instances_sbi.v | 5 +++++
 2 files changed, 9 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index f657edfe7..b92a17884 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -377,6 +377,10 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
   (∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y).
 Proof. iIntros "H". iNext. done. Qed.
 
+Lemma text_iNext_Next {A B : ofeT} (f : A -n> A) x y :
+  Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP).
+Proof. iIntros "H". iNext. by iRewrite "H". Qed.
+
 Lemma test_iFrame_persistent (P Q : PROP) :
   □ P -∗ Q -∗ <pers> (P ∗ P) ∗ (P ∗ Q ∨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index bda75b778..debfbfa98 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -373,6 +373,11 @@ Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_laterN n P :
   FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
 Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_Next {A : ofeT} (x y : A) :
+  FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
+    (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
+Proof. by rewrite /FromModal /= later_equivI. Qed.
+
 Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) (â—‡ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.
 
-- 
GitLab