Factor out lemma `löb_weak`.

theories/bi/derived_laws_later.v

@@ -84,23 +84,33 @@ 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 (▷)]
+2. [(▷ P → P) ⊢ P], the internal version of Löb as expressed by [BiLöb].
+3. [(▷ P ⊢ P) → (True ⊢ P)], the external/"weak" version of Löb induction.
+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_weak]).
+- (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]).
+
+In particular, this gives that (2), (3), (4) and (5) are logically equivalent in
+affine BI logics such as Iris. *)
+
+Lemma löb_alt_weak : BiLöb PROP ↔ ∀ P, (▷ P ⊢ P) → (True ⊢ 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.
+  split; intros HLöb P.
+  { by intros ->%entails_impl_True. }
+  apply entails_impl_True, HLöb. apply impl_intro_r.
   rewrite -{2}(idemp (∧) (▷ P → P))%I.
   rewrite {2}(later_intro (▷ P → P))%I.
   rewrite later_impl.
@@ -108,6 +118,24 @@ Proof.
   rewrite impl_elim_r. done.
 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.
+Proof.
+  intros. apply löb_alt_weak=> 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,7 +151,7 @@ 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|].
   rewrite bi.impl_alt. apply bi.exist_elim=> R. apply impl_elim_r'.