From b57797ee1ffb70f882754ac88f35feef74bb215c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Jun 2020 13:00:44 +0200
Subject: [PATCH] Introduce notation `BiLaterContractive PROP` for `Contractive
 (bi_later (PROP:=PROP))`.

---
 theories/base_logic/bi.v          |  2 +-
 theories/bi/derived_connectives.v | 15 +++++++++------
 theories/bi/derived_laws_later.v  |  5 ++---
 theories/bi/interface.v           |  4 ++--
 theories/bi/monpred.v             |  2 +-
 theories/si_logic/bi.v            |  2 +-
 6 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index ebb60030c..516274c02 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -89,7 +89,7 @@ Canonical Structure uPredI (M : ucmraT) : bi :=
      bi_bi_mixin := uPred_bi_mixin M;
      bi_bi_later_mixin := uPred_bi_later_mixin M |}.
 
-Instance uPred_later_contractive {M} : Contractive (bi_later (PROP:=uPredI M)).
+Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
 Proof. apply later_contractive. Qed.
 
 Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index fa318bd5d..0ca78688d 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -117,15 +117,18 @@ Arguments bi_wandM {_} !_%I _%I /.
 Notation "mP -∗? Q" := (bi_wandM mP Q)
   (at level 99, Q at level 200, right associativity) : bi_scope.
 
-(** 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_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
+(** The class [BiLöb] is required for the [iLöb] tactic. However, for most BI
+logics [BiLaterContractive] should be used, which gives an instance of [BiLöb]
+automatically (see [derived_laws_later]). A direct instance of [BiLöb] is useful
+when considering a BI logic with a discrete OFE, instead of an OFE that takes
 step-indexing of the logic in account.
 
-The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derived. It is provided
-by the lemma [löb] in [derived_laws_later]. *)
+The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [BiLöb].
+It is provided by the lemma [löb] in [derived_laws_later]. *)
 Class BiLöb (PROP : bi) :=
   löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
 Hint Mode BiLöb ! : typeclass_instances.
 Arguments löb_weak {_ _} _ _.
+
+Notation BiLaterContractive PROP :=
+  (Contractive (bi_later (PROP:=PROP))) (only parsing).
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 7403b6d8d..b5c520709 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -87,7 +87,7 @@ Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
 (** * Alternatives to Löb induction *)
 (** We prove relations between the following statements:
 
-1. [Contractive (â–·)]
+1. [Contractive (â–·)], later is contractive as expressed by [BiLaterContractive].
 2. [(▷ P ⊢ P) → (True ⊢ P)], the external/"weak" of Löb as expressed by [BiLöb].
 3. [(▷ P → P) ⊢ P], the internal version/"strong" of Löb.
 4. [□ (□ ▷ P -∗ P) ⊢ P], an internal version of Löb with magic wand instead of
@@ -121,8 +121,7 @@ Proof. split; intros HLöb P. apply löb. by intros ->%entails_impl_True. Qed.
 
 (** Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
 Their [Ψ] is called [Q] in our proof. *)
-Global Instance later_contractive_bi_löb :
-  Contractive (bi_later (PROP:=PROP)) → BiLöb PROP.
+Global Instance later_contractive_bi_löb : BiLaterContractive PROP → BiLöb PROP.
 Proof.
   intros=> P.
   pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index c0044e908..25198a338 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -120,8 +120,8 @@ Section bi_mixin.
   For non step-indexed BIs the later modality can simply be defined as the
   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_later].)
+  of the class [BiLaterContractive PROP] or [BiLöb PROP]. (Note that there is an
+  instance [BiLaterContractive PROP → 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/monpred.v b/theories/bi/monpred.v
index 5d83a8e82..ee70c6117 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -401,7 +401,7 @@ Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_i
 Proof. solve_proper. Qed.
 
 Global Instance monPred_later_contractive :
-  Contractive (bi_later (PROP:=PROP)) → Contractive (bi_later (PROP:=monPredI)).
+  BiLaterContractive PROP → BiLaterContractive monPredI.
 Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
 Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
 Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index a12d22cc4..8392463e4 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -115,7 +115,7 @@ Canonical Structure siPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of siProp;
      bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
 
-Instance siProp_later_contractive : Contractive (bi_later (PROP:=siPropI)).
+Instance siProp_later_contractive : BiLaterContractive siPropI.
 Proof. apply later_contractive. Qed.
 
 Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
-- 
GitLab