Merge branch 'ralf/löb' into 'gen_proofmode'

Derive löb induction from later introduction and guarded fixpoints

See merge request FP/iris-coq!145

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; first done.
+    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,8 @@ 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 equiv_spec; naive_solver. 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,34 @@ 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.
+     Their Ψ is called Q in our proof. *)
+  Lemma weak_löb P : (▷ P ⊢ P) → (True ⊢ P).
+  Proof.
+    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 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.

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) :
@@ -229,6 +229,7 @@ Structure sbi := Sbi {
   sbi_internal_eq : ∀ A : ofeT, A → A → sbi_car;
   sbi_later : sbi_car → sbi_car;
   sbi_ofe_mixin : OfeMixin sbi_car;
+  sbi_cofe : Cofe (OfeT sbi_car sbi_ofe_mixin);
   sbi_bi_mixin : BiMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl
                          sbi_forall sbi_exist sbi_sep sbi_wand sbi_persistently;
   sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
@@ -247,6 +248,8 @@ Canonical Structure sbi_ofeC.
 Coercion sbi_bi (PROP : sbi) : bi :=
   {| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}.
 Canonical Structure sbi_bi.
+Global Instance sbi_cofe' (PROP : sbi) : Cofe PROP.
+Proof. apply sbi_cofe. Qed.
 
 Arguments sbi_car : simpl never.
 Arguments sbi_dist : simpl never.
@@ -454,8 +457,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.