From 6ae844abb5740b5d1f61f6bbabdbd03b17fe5105 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 3 Mar 2019 12:24:46 +0100
Subject: [PATCH] Allow swapping later^n and forall

For half of #231.
---
 tests/proofmode.v                        |  5 +++++
 theories/proofmode/class_instances_sbi.v | 10 ++++++++++
 2 files changed, 15 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index b2e87333f..981242fe3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -380,6 +380,11 @@ Proof.
   iSpecialize ("Hφ" with "[% //] HP"). done.
 Qed.
 
+Lemma demo_laterN_forall {A} (Φ Ψ: A → PROP) n: (∀ x, ▷^n Φ x) -∗ ▷^n (∀ x, Φ x).
+Proof.
+  iIntros "H" (w). iApply ("H" $! w).
+Qed.
+
 Lemma test_iNext_laterN_later P n : ▷ ▷^n P -∗ ▷^n ▷ P.
 Proof. iIntros "H". iNext. by iNext. Qed.
 Lemma test_iNext_later_laterN P n : ▷^n ▷ P -∗ ▷ ▷^n P.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 5d8aae731..d6eaeb496 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -301,6 +301,11 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_forall_later {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
+
+Global Instance into_forall_laterN {A} P (Φ : A → PROP) n :
+  IntoForall P Φ → IntoForall (▷^n P) (λ a, ▷^n (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP laterN_forall. Qed.
+
 Global Instance into_forall_except_0 {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
@@ -313,6 +318,11 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance from_forall_later {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
+
+Global Instance from_forall_laterN {A} P (Φ : A → PROP) n :
+      FromForall P Φ → FromForall (▷^n P)%I (λ a, ▷^n (Φ a))%I.
+Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
+
 Global Instance from_forall_except_0 {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
-- 
GitLab