Merge branch 'robbert/loeb_weak' into 'master'

Factor out lemma `löb_weak`.

See merge request iris/iris!459

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,12 +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
-step-indexing of the logic in account.*)
+(** 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 derivable from [BiLöb].
+It is provided by the lemma [löb] in [derived_laws_later]. *)
 Class BiLöb (PROP : bi) :=
-  löb (P : PROP) : (▷ P → P) ⊢ P.
+  löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
 Hint Mode BiLöb ! : typeclass_instances.
-Arguments löb {_ _} _.
+Arguments löb_weak {_ _} _ _.
+
+Notation BiLaterContractive PROP :=
+  (Contractive (bi_later (PROP:=PROP))) (only parsing).

theories/bi/derived_laws_later.v

@@ -84,23 +84,31 @@ Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
 Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. 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.
+(** * Alternatives to Löb induction *)
+(** We prove relations between the following statements:
+
+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
+   implication.
+5. [□ (▷ P -∗ P) ⊢ P], a weaker version of the former statement, which does not
+   make the induction hypothesis intuitionistic.
+
+We prove that:
+
+- (1) implies (2) in all BI logics (lemma [later_contractive_bi_löb]).
+- (2) and (3) are logically equivalent in all BI logics (lemma [löb_alt_strong]).
+- (2) implies (4) and (5) in all BI logics (lemmas [löb_wand_intuitionistically]
+  and [löb_wand]).
+- (5) and (2) are logically equivalent in affine BI logics (lemma [löb_alt_wand]).
+
+In particular, this gives that (2), (3), (4) and (5) are logically equivalent in
+affine BI logics such as Iris. *)
+
+Lemma löb `{!BiLöb PROP} P : (▷ P → P) ⊢ P.
 Proof.
-  intros. assert (∀ P, (▷ P ⊢ P) → (True ⊢ P)) as weak_löb.
-  { intros P. pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
-    assert (∀ P, Contractive (flöb_pre P)) by solve_contractive.
-    set (Q := fixpoint (flöb_pre P)).
-    assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold).
-    intros HP. rewrite -HP.
-    assert (▷ Q ⊢ P) as HQP.
-    { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q))%I.
-      by rewrite {1}HQ {1}later_impl impl_elim_l. }
-    rewrite -HQP HQ -2!later_intro.
-    apply (entails_impl_True _ P). done. }
-  intros P. apply entails_impl_True, weak_löb. apply impl_intro_r.
+  apply entails_impl_True, löb_weak. apply impl_intro_r.
   rewrite -{2}(idemp (∧) (▷ P → P))%I.
   rewrite {2}(later_intro (▷ P → P))%I.
   rewrite later_impl.
@@ -108,6 +116,26 @@ Proof.
   rewrite impl_elim_r. done.
 Qed.
 
+Lemma löb_alt_strong : BiLöb PROP ↔ ∀ P, (▷ P → P) ⊢ P.
+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 : BiLaterContractive PROP → BiLöb PROP.
+Proof.
+  intros=> P.
+  pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
+  assert (∀ P, Contractive (flöb_pre P)) by solve_contractive.
+  set (Q := fixpoint (flöb_pre P)).
+  assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold).
+  intros HP. rewrite -HP.
+  assert (▷ Q ⊢ P) as HQP.
+  { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q))%I.
+    by rewrite {1}HQ {1}later_impl impl_elim_l. }
+  rewrite -HQP HQ -2!later_intro.
+  apply (entails_impl_True _ P). done.
+Qed.
+
 Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P.
 Proof.
   rewrite -{3}(intuitionistically_elim P) -(löb (□ P)%I). apply impl_intro_l.
@@ -123,9 +151,10 @@ Qed.
 
 (** The proof of the right-to-left direction relies on the BI being affine. It
 is unclear how to generalize the lemma or proof to support non-affine BIs. *)
-Lemma löb_alt `{!BiAffine PROP} : BiLöb PROP ↔ ∀ P, □ (▷ P -∗ P) ⊢ P.
+Lemma löb_alt_wand `{!BiAffine PROP} : BiLöb PROP ↔ ∀ P, □ (▷ P -∗ P) ⊢ P.
 Proof.
-  split; intros Hlöb P; [by apply löb_wand|].
+  split; intros Hlöb; [by apply löb_wand|].
+  apply löb_alt_strong=> P.
   rewrite bi.impl_alt. apply bi.exist_elim=> R. apply impl_elim_r'.
   rewrite -(Hlöb (R → P)%I) -intuitionistically_into_persistently.
   apply intuitionistically_intro', wand_intro_l, impl_intro_l.

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,12 +401,10 @@ 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.
-  split=> i. unseal. by rewrite (bi.forall_elim i) bi.pure_True // left_id löb.
-Qed.
+Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
 Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
 Proof. split => ?. unseal. apply bi_positive. Qed.
 Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.

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