Introduce notation `BiLaterContractive PROP` for `Contractive (bi_later (PROP:=PROP))`.

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).

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).

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).

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. *)

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.

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).