Derive löb induction from later introduction

This follows the proof at https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem

theories/base_logic/upred.v

@@ -508,9 +508,9 @@ Proof.
   - (* (P ⊢ Q) → ▷ P ⊢ ▷ Q *)
     intros P Q.
     unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
-  - (* (▷ P → P) ⊢ P *)
-    intros P. unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
-    apply HP, IH, uPred_mono with (S n) x; eauto using cmra_validN_S.
+  - (* P ⊢ ▷ P *)
+    intros P. unseal; split=> n x ? HP. destruct n; first done. simpl.
+    apply uPred_mono with (S n) x; eauto using cmra_validN_S.
   - (* (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a *)
     intros A Φ. unseal; by split=> -[|n] x.
   - (* (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a) *)

theories/bi/derived_laws_bi.v

@@ -122,6 +122,12 @@ Proof.
     + apply and_intro; first done. by apply pure_intro.
     + rewrite -EQ impl_elim_r. done.
 Qed.
+Lemma entails_impl_True P Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)).
+Proof.
+  rewrite entails_eq_True. split.
+  - by intros <-.
+  - intros. apply (anti_symm (⊢)); last done. apply True_intro.
+Qed.
 
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.

theories/bi/derived_laws_sbi.v

@@ -158,12 +158,6 @@ Global Instance later_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@sbi_later PROP).
 Proof. intros P Q; apply later_mono. Qed.
 
-Lemma later_intro P : P ⊢ ▷ P.
-Proof.
-  rewrite -(and_elim_l (▷ P)%I P) -(löb (▷ P ∧ P)%I).
-  apply impl_intro_l. by rewrite {1}(and_elim_r (▷ P)%I).
-Qed.
-
 Lemma later_True : ▷ True ⊣⊢ True.
 Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
 Lemma later_emp `{!BiAffine PROP} : ▷ emp ⊣⊢ emp.
@@ -209,6 +203,45 @@ 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.
 
+Section löb.
+  (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem *)
+  Definition flöb_pre (P Ψ : PROP) : PROP := (▷ Ψ → P)%I.
+
+  Local Instance flöb_pre_contractive P : Contractive (flöb_pre P).
+  Proof. solve_contractive. Qed.
+
+  Context `{Cofe PROP}.
+
+  Definition flöb (P : PROP) := fixpoint (flöb_pre P).
+
+  Lemma weak_löb P : (▷ P ⊢ P) → (True ⊢ P).
+  Proof.
+    set (Ψ := flöb P). assert (Ψ ⊣⊢ (▷ Ψ → P)) as HΨ.
+    { exact: fixpoint_unfold. }
+    intros HP. rewrite -HP.
+    assert (Ψ ⊢ (▷ Ψ → P)) as HΨ'%entails_impl_True by by rewrite -HΨ.
+    rewrite ->(later_intro (Ψ → _))%I in HΨ'.
+    rewrite ->later_impl in HΨ'.
+    rewrite ->later_impl in HΨ'.
+    assert (▷ Ψ ⊢ P) as HΨP.
+    { rewrite -HP. rewrite -(idemp (∧) (▷ Ψ))%I {2}(later_intro (▷ Ψ))%I.
+      apply impl_elim_l', entails_impl_True. done. }
+    rewrite -HΨP HΨ -2!later_intro.
+    apply (entails_impl_True _ P). done.
+  Qed.
+
+  Lemma löb P : (▷ P → P) ⊢ P.
+  Proof.
+    apply entails_impl_True, weak_löb. apply impl_intro_r.
+    rewrite -{2}(idemp (∧) (▷ P → P))%I.
+    rewrite {2}(later_intro (▷ P → P))%I.
+    rewrite later_impl.
+    rewrite assoc impl_elim_l.
+    rewrite impl_elim_r. done.
+  Qed.
+
+End löb.
+
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@sbi_laterN PROP m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
@@ -379,7 +412,7 @@ Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
 Global Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
 Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
 
-Global Instance impl_timeless P Q : Timeless Q → Timeless (P → Q).
+Global Instance impl_timeless `{Cofe PROP} P Q : Timeless Q → Timeless (P → Q).
 Proof.
   rewrite /Timeless=> HQ. rewrite later_false_em.
   apply or_mono, impl_intro_l; first done.
@@ -392,7 +425,7 @@ Proof.
   intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono.
 Qed.
 
-Global Instance wand_timeless P Q : Timeless Q → Timeless (P -∗ Q).
+Global Instance wand_timeless `{Cofe PROP} P Q : Timeless Q → Timeless (P -∗ Q).
 Proof.
   rewrite /Timeless=> HQ. rewrite later_false_em.
   apply or_mono, wand_intro_l; first done.

theories/bi/interface.v

@@ -146,7 +146,7 @@ Section bi_mixin.
     sbi_mixin_later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y;
 
     sbi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q;
-    sbi_mixin_löb P : (▷ P → P) ⊢ P;
+    sbi_mixin_later_intro P : P ⊢ ▷ P;
 
     sbi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a;
     sbi_mixin_later_exist_false {A} (Φ : A → PROP) :
@@ -454,8 +454,8 @@ Proof. eapply sbi_mixin_later_eq_2, sbi_sbi_mixin. Qed.
 
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof. eapply sbi_mixin_later_mono, sbi_sbi_mixin. Qed.
-Lemma löb P : (▷ P → P) ⊢ P.
-Proof. eapply sbi_mixin_löb, sbi_sbi_mixin. Qed.
+Lemma later_intro P : P ⊢ ▷ P.
+Proof. eapply sbi_mixin_later_intro, sbi_sbi_mixin. Qed.
 
 Lemma later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
 Proof. eapply sbi_mixin_later_forall_2, sbi_sbi_mixin. Qed.

theories/bi/monpred.v

@@ -336,8 +336,7 @@ Proof.
   - intros A x y. split=> i. by apply bi.later_eq_1.
   - intros A x y. split=> i. by apply bi.later_eq_2.
   - intros P Q [?]. split=> i. by apply bi.later_mono.
-  - intros P. split=> i /=.
-    setoid_rewrite bi.pure_impl_forall. rewrite /= !bi.forall_elim //. by apply bi.löb.
+  - intros P. split=> i /=. by apply bi.later_intro.
   - intros A Ψ. split=> i. by apply bi.later_forall_2.
   - intros A Ψ. split=> i. by apply bi.later_exist_false.
   - intros P Q. split=> i. by apply bi.later_sep_1.

theories/proofmode/coq_tactics.v

@@ -1396,7 +1396,7 @@ Proof.
   - by rewrite Hs //= right_id.
 Qed.
 
-Lemma tac_löb Δ Δ' i Q :
+Lemma tac_löb `{Cofe PROP} Δ Δ' i Q :
   env_spatial_is_nil Δ = true →
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   envs_entails Δ' Q → envs_entails Δ Q.

theories/proofmode/ltac_tactics.v

@@ -1659,7 +1659,8 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      refine should use the other unification algorithm, which should
      not have this issue. *)
   notypeclasses refine (tac_löb _ _ IH _ _ _ _);
-    [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
+    [iSolveTC || fail "iLöb: PROP is not a Cofe"
+    |reflexivity || fail "iLöb: spatial context not empty, this should not happen"
     |env_reflexivity || fail "iLöb:" IH "not fresh"|].
 
 Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) :=

theories/tests/proofmode.v

 From iris.proofmode Require Import tactics intro_patterns.
 From stdpp Require Import gmap hlist.
-Set Default Proof Using "Type".
+Set Default Proof Using "Type*".
 
 Section tests.
-Context {PROP : sbi}.
+Context {PROP : sbi} `{Cofe PROP}.
 Implicit Types P Q R : PROP.
 
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
@@ -381,8 +381,8 @@ Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qe
 
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : PROP.
 Proof.
-  iIntros (H).
-  iEval (rewrite (Nat.add_comm x y) // H).
+  iIntros (Hn).
+  iEval (rewrite (Nat.add_comm x y) // Hn).
   done.
 Qed.