From 15ce289f3b3da9717b250e6d1124a4d075e586d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 13:05:10 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`derived=5Flaws=5Fbi`=20=E2=86=92=20`d?=
=?UTF-8?q?erived=5Flaws`=20and=20`derived=5Flaws=5Fsbi`=20=E2=86=92=20`de?=
=?UTF-8?q?rived=5Flaws=5Flater`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
_CoqProject | 4 ++--
theories/bi/bi.v | 6 +++---
theories/bi/big_op.v | 4 ++--
theories/bi/derived_connectives.v | 2 +-
theories/bi/{derived_laws_bi.v => derived_laws.v} | 4 ++--
theories/bi/{derived_laws_sbi.v => derived_laws_later.v} | 9 +++++----
theories/bi/embedding.v | 2 +-
theories/bi/interface.v | 2 +-
theories/bi/internal_eq.v | 4 ++--
theories/bi/plainly.v | 4 ++--
theories/bi/updates.v | 4 ++--
11 files changed, 23 insertions(+), 22 deletions(-)
rename theories/bi/{derived_laws_bi.v => derived_laws.v} (99%)
rename theories/bi/{derived_laws_sbi.v => derived_laws_later.v} (99%)
diff --git a/_CoqProject b/_CoqProject
index f01a9bc22..fa1ddef99 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,8 +44,8 @@ theories/si_logic/bi.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
-theories/bi/derived_laws_bi.v
-theories/bi/derived_laws_sbi.v
+theories/bi/derived_laws.v
+theories/bi/derived_laws_later.v
theories/bi/plainly.v
theories/bi/internal_eq.v
theories/bi/big_op.v
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 9fde00f1a..8f5aa1aa0 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,9 +1,9 @@
-From iris.bi Require Export derived_laws_bi derived_laws_sbi big_op.
+From iris.bi Require Export derived_laws derived_laws_later big_op.
From iris.bi Require Export updates internal_eq plainly embedding.
Set Default Proof Using "Type".
Module Import bi.
Export bi.interface.bi.
- Export bi.derived_laws_bi.bi.
- Export bi.derived_laws_sbi.bi.
+ Export bi.derived_laws.bi.
+ Export bi.derived_laws_later.bi.
End bi.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 4bb194021..bfe5cd184 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,8 +1,8 @@
From stdpp Require Import countable fin_sets functions.
-From iris.bi Require Import derived_laws_sbi.
+From iris.bi Require Import derived_laws_later.
From iris.algebra Require Export big_op.
Set Default Proof Using "Type".
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
(** Notations for unary variants *)
Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 4a64793a0..b6c10d542 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -119,7 +119,7 @@ Notation "mP -∗? Q" := (bi_wandM mP Q)
(** This class is required for the [iLöb] tactic. For most logics this class
should not be inhabited directly, but the instance [Contractive (▷) → BiLöb PROP]
-in [derived_laws_sbi] should be used. A direct instance of the class is useful
+in [derived_laws_later] should be used. A direct instance of the class is useful
when considering a BI logic with a discrete OFE, instead of a OFE that takes
step-indexing of the logic in account.*)
Class BiLöb (PROP : bi) :=
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws.v
similarity index 99%
rename from theories/bi/derived_laws_bi.v
rename to theories/bi/derived_laws.v
index 1127e290b..40641c9b9 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws.v
@@ -10,7 +10,7 @@ From iris.algebra Require Import monoid.
Module bi.
Import interface.bi.
-Section bi_derived.
+Section derived.
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
@@ -1551,5 +1551,5 @@ Qed.
Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP) :
NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-End bi_derived.
+End derived.
End bi.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_later.v
similarity index 99%
rename from theories/bi/derived_laws_sbi.v
rename to theories/bi/derived_laws_later.v
index 19bafd7bf..7f3d4bd4e 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,10 +1,11 @@
-From iris.bi Require Export derived_laws_bi.
+From iris.bi Require Export derived_laws.
From iris.algebra Require Import monoid.
Module bi.
Import interface.bi.
-Import derived_laws_bi.bi.
-Section sbi_derived.
+Import derived_laws.bi.
+
+Section later_derived.
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
@@ -398,5 +399,5 @@ Proof. split; try apply _. apply laterN_intro. Qed.
Global Instance bi_except_0_sep_entails_homomorphism :
MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_intro. Qed.
-End sbi_derived.
+End later_derived.
End bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 24f4c237f..9862bcd95 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import interface derived_laws_sbi big_op.
+From iris.bi Require Import interface derived_laws_later big_op.
From iris.bi Require Import plainly updates internal_eq.
From iris.algebra Require Import monoid.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 5a460db1c..c0044e908 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -121,7 +121,7 @@ Section bi_mixin.
identity function, as the Löb axiom or contractiveness of later is not part of
[BiLaterMixin]. For step-indexed BIs one should separately prove an instance
of the class [BiLöb PROP] or [Contractive (▷)]. (Note that there is an
- instance [Contractive (▷) → BiLöb PROP] in [derived_laws_sbi].)
+ instance [Contractive (▷) → BiLöb PROP] in [derived_laws_later].)
For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
the smart constructor [bi_later_mixin_id] below. *)
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 6e97b92e6..6ecd8ec6f 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -1,5 +1,5 @@
-From iris.bi Require Import derived_laws_sbi big_op.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+From iris.bi Require Import derived_laws_later big_op.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
(** This file defines a type class for BIs with a notion of internal equality.
Internal equality is not part of the [bi] canonical structure as [internal_eq]
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index f99e4b68a..a5b5af021 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,6 +1,6 @@
-From iris.bi Require Import derived_laws_sbi big_op internal_eq.
+From iris.bi Require Import derived_laws_later big_op internal_eq.
From iris.algebra Require Import monoid.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
Class Plainly (A : Type) := plainly : A → A.
Hint Mode Plainly ! : typeclass_instances.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 7b2498daf..51f54aa59 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,6 +1,6 @@
From stdpp Require Import coPset.
-From iris.bi Require Import interface derived_laws_sbi big_op plainly.
-Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
+From iris.bi Require Import interface derived_laws_later big_op plainly.
+Import interface.bi derived_laws.bi derived_laws_later.bi.
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
--
GitLab