Fixpoint/Cofixpoint lemmas

CHANGELOG.md

@@ -5,6 +5,25 @@ lemma.
 
 ## Iris master
 
+**Changes in `bi`:**
+* Rename `least_fixpoint_ind` into `least_fixpoint_iter`,
+  rename `greatest_fixpoint_coind` into `greatest_fixpoint_coiter`,
+  rename `least_fixpoint_strong_ind` into `least_fixpoint_ind`,
+  add lemmas `least_fixpoint_{ind_wf, ne', strong_mono}`, and
+  add lemmas `greatest_fixpoint_{coind, paco, ne', strong_mono}`.
+
+The following `sed` script helps adjust your code to the renaming (on macOS,
+replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# least/greatest fixpoint renames
+s/\bleast_fixpoint_ind\b/least_fixpoint_iter/g
+s/\bgreatest_fixpoint_coind\b/greatest_fixpoint_coiter/g
+s/\bleast_fixpoint_strong_ind\b/least_fixpoint_ind/g
+EOF
+```
+
 ## Iris 3.5.0 (2021-11-05)
 
 The highlights and most notable changes of this release are:

iris/bi/lib/atomic.v

@@ -253,7 +253,7 @@ Section lemmas.
   Proof.
     rewrite atomic_update_eq {2}/atomic_update_def /=.
     iIntros (Heo) "HAU".
-    iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
+    iApply (greatest_fixpoint_coiter _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
     iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
     iApply make_laterable_intuitionistic_wand. iIntros "!>".
     iApply atomic_acc_mask_weaken. done.
@@ -299,7 +299,7 @@ Section lemmas.
   Proof.
     rewrite atomic_update_eq {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
-    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
+    iApply (greatest_fixpoint_coiter _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
     iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> HQ".
     iApply HAU. by iFrame.
   Qed.

iris/bi/lib/fixpoint.v

@@ -25,6 +25,11 @@ Definition bi_greatest_fixpoint {PROP : bi} {A : ofe}
   tc_opaque (∃ Φ : A -n> PROP, □ (∀ x, Φ x -∗ F Φ x) ∗ Φ x)%I.
 Global Arguments bi_greatest_fixpoint : simpl never.
 
+(* Both non-expansiveness lemmas do not seem to be interderivable.
+  FIXME: is there some lemma that subsumes both? *)
+Lemma least_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)):
+  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
+Proof. solve_proper. Qed.
 Global Instance least_fixpoint_ne {PROP : bi} {A : ofe} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
           dist n ==> dist n) bi_least_fixpoint.
@@ -58,25 +63,74 @@ Section least.
     apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
   Qed.
 
-  Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
+  (**
+    The basic induction principle for least fixpoints: as inductive hypothesis,
+    it allows to assume the statement to prove below exactly one application of [F].
+   *)
+  Lemma least_fixpoint_iter (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
   Proof.
     iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (OfeMor Φ) with "[#]").
   Qed.
+End least.
+
+Lemma least_fixpoint_strong_mono {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}
+    (G : (A → PROP) → (A → PROP)) `{!BiMonoPred G} :
+  □ (∀ Φ x, F Φ x -∗ G Φ x) -∗
+  ∀ x, bi_least_fixpoint F x -∗ bi_least_fixpoint G x.
+Proof.
+  iIntros "#Hmon". iApply least_fixpoint_iter.
+  iIntros "!>" (y) "IH". iApply least_fixpoint_unfold.
+  by iApply "Hmon".
+Qed.
+
+(**
+  In addition to [least_fixpoint_iter], we provide two derived, stronger induction principles.
+  - [least_fixpoint_ind] allows to assume [F (λ x, Φ x ∧ bi_least_fixpoint F x) y] when proving
+    the inductive step.
+    Intuitively, it does not only offer the induction hypothesis ([Φ] under an application of [F]),
+    but also the induction predicate [bi_least_fixpoint F] itself (under an application of [F]).
+  - [least_fixpoint_ind_wf] intuitively corresponds to a kind of well-founded induction.
+    It provides the hypothesis [F (bi_least_fixpoint (λ Ψ a, Φ a ∧ F Ψ a)) y] and thus allows
+    to assume the induction hypothesis not just below one application of [F], but below any
+    positive number (by unfolding the least fixpoint).
+    The unfolding lemma [least_fixpoint_unfold] as well as [least_fixpoint_strong_mono] can be useful
+    to work with the hypothesis.
+ *)
+Section least_ind.
+  Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+
+  Let wf_pred_mono `{!NonExpansive Φ} : BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∧ F Ψ a)%I.
+  Proof using Type*.
+    split; last solve_proper.
+    intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "Ha". iSplit; first by iDestruct "Ha" as "[$ _]".
+    iDestruct "Ha" as "[_ Hr]". iApply (bi_mono_pred with "[] Hr"). by iModIntro.
+  Qed.
+  Local Existing Instance wf_pred_mono.
 
-  Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
+  Lemma least_fixpoint_ind_wf (Φ : A → PROP) `{!NonExpansive Φ} :
+    □ (∀ y, F (bi_least_fixpoint (λ Ψ a, Φ a ∧ F Ψ a)) y -∗ Φ y) -∗
+    ∀ x, bi_least_fixpoint F x -∗ Φ x.
+  Proof using Type*.
+    iIntros "#Hmon" (x). rewrite least_fixpoint_unfold. iIntros "Hx".
+    iApply "Hmon". iApply (bi_mono_pred with "[] Hx").
+    iModIntro. iApply least_fixpoint_iter.
+    iIntros "!> %y Hy". rewrite least_fixpoint_unfold.
+    iSplit; last done. by iApply "Hmon".
+  Qed.
+
+  Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
     ∀ x, bi_least_fixpoint F x -∗ Φ x.
   Proof using Type*.
-    trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
-    { iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
-      iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
-      iApply least_fixpoint_unfold_2.
-      iApply (bi_mono_pred with "[#] H"); [solve_proper|].
-      by iIntros "!> * [_ ?]". }
-    by setoid_rewrite and_elim_l.
+    iIntros "#Hmon". iApply least_fixpoint_ind_wf. iIntros "!> %y Hy".
+    iApply "Hmon". iApply (bi_mono_pred with "[] Hy"). { solve_proper. }
+    iIntros "!> %x Hx". iSplit.
+    - rewrite least_fixpoint_unfold. iDestruct "Hx" as "[$ _]".
+    - iApply (least_fixpoint_strong_mono with "[] Hx"). iIntros "!>" (??) "[_ $]".
   Qed.
-End least.
+End least_ind.
+
 
 Lemma greatest_fixpoint_ne_outer {PROP : bi} {A : ofe}
     (F1 : (A → PROP) → (A → PROP)) (F2 : (A → PROP) → (A → PROP)):
@@ -87,6 +141,11 @@ Proof.
   do 3 f_equiv; last solve_proper. repeat f_equiv. apply HF.
 Qed.
 
+(* Both non-expansiveness lemmas do not seem to be interderivable.
+  FIXME: is there some lemma that subsumes both? *)
+Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)):
+  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
+Proof. solve_proper. Qed.
 Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofe} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
           dist n ==> dist n) bi_greatest_fixpoint.
@@ -122,7 +181,92 @@ Section greatest.
     apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
   Qed.
 
-  Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
+  (**
+    The following lemma provides basic coinduction capabilities,
+    by requiring to reestablish the coinduction hypothesis after exactly one step.
+   *)
+  Lemma greatest_fixpoint_coiter (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
   Proof. iIntros "#HΦ" (x) "Hx". iExists (OfeMor Φ). auto. Qed.
 End greatest.
+
+Lemma greatest_fixpoint_strong_mono {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}
+  (G : (A → PROP) → (A → PROP)) `{!BiMonoPred G} :
+  □ (∀ Φ x, F Φ x -∗ G Φ x) -∗
+  ∀ x, bi_greatest_fixpoint F x -∗ bi_greatest_fixpoint G x.
+Proof using Type*.
+  iIntros "#Hmon". iApply greatest_fixpoint_coiter.
+  iIntros "!>" (y) "IH". rewrite greatest_fixpoint_unfold.
+  by iApply "Hmon".
+Qed.
+
+(**
+  In addition to [greatest_fixpoint_coiter], we provide two derived, stronger coinduction principles.
+  - [greatest_fixpoint_coind] requires to prove [F (λ x, Φ x ∨ bi_greatest_fixpoint F x) y]
+    in the coinductive step instead of [F Φ y] and thus instead allows to prove the original
+    fixpoint again, after taking one step.
+  - [greatest_fixpoint_paco] allows for so-called parameterized coinduction, a stronger coinduction
+    principle, where [F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y] needs to be established in
+    the coinductive step. It allows to prove the hypothesis [Φ] not just after one step,
+    but after any positive number of unfoldings of the greatest fixpoint.
+    This encodes a way of accumulating "knowledge" in the coinduction hypothesis:
+      if you return to the "initial point" [Φ] of the coinduction after some number of
+      unfoldings (not just one), the proof is done.
+    (interestingly, this is the dual to [least_fixpoint_ind_wf]).
+    The unfolding lemma [greatest_fixpoint_unfold] and [greatest_fixpoint_strong_mono] may be useful
+    when using this lemma.
+
+    Example use case:
+      Suppose that [F] defines a coinductive simulation relation, e.g.,
+        [F rec '(e_t, e_s) :=
+          (is_val e_s ∧ is_val e_t ∧ post e_t e_s) ∨
+          (safe e_t ∧ ∀ e_t', step e_t e_t' → ∃ e_s', step e_s e_s' ∧ rec e_t' e_s')],
+      and [sim e_t e_s := bi_greatest_fixpoint F].
+      Suppose you want to show a simulation of two loops,
+        [sim (while ...) (while ...)],
+      i.e. [Φ '(e_t, e_s) := e_t = while ... ∧ e_s = while ...].
+      Then the standard coinduction principle [greatest_fixpoint_iter]
+      requires to establish the coinduction hypothesis [Φ] after precisely
+      one unfolding of [sim], which is clearly not strong enough if the
+      loop takes multiple steps of computation per iteration.
+      But [greatest_fixpoint_paco] allows to establish a fixpoint to which [Φ] has
+      been added as a disjunct.
+      This fixpoint can be unfolded arbitrarily many times, allowing to establish the
+      coinduction hypothesis after any number of steps.
+      This enables to take multiple simulation steps, before closing the coinduction
+      by establishing the hypothesis [Φ] again.
+ *)
+Section greatest_coind.
+  Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+
+  Let paco_mono `{!NonExpansive Φ} : BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∨ F Ψ a)%I.
+  Proof using Type*.
+    split; last solve_proper.
+    intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "[H1|H2]"; first by iLeft.
+    iRight. iApply (bi_mono_pred with "[] H2"). by iModIntro.
+  Qed.
+  Local Existing Instance paco_mono.
+
+  Lemma greatest_fixpoint_paco `{!NonExpansive Φ} :
+    □ (∀ y, Φ y -∗ F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y) -∗
+    ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
+  Proof using Type*.
+    iIntros "#Hmon" (x) "HΦ". iDestruct ("Hmon" with "HΦ") as "HF".
+    rewrite greatest_fixpoint_unfold. iApply (bi_mono_pred with "[] HF").
+    iIntros "!>" (y) "HG". iApply (greatest_fixpoint_coiter with "[] HG").
+    iIntros "!>" (z) "Hf". rewrite greatest_fixpoint_unfold.
+    iDestruct "Hf" as "[HΦ|$]". by iApply "Hmon".
+  Qed.
+
+  Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
+    □ (∀ y, Φ y -∗ F (λ x, Φ x ∨ bi_greatest_fixpoint F x) y) -∗
+    ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
+  Proof using Type*.
+    iIntros "#Ha". iApply greatest_fixpoint_paco. iModIntro.
+    iIntros (y) "Hy". iSpecialize ("Ha" with "Hy").
+    iApply (bi_mono_pred with "[] Ha"). { solve_proper. }
+    iIntros "!> %x [Hphi | Hgfp]".
+    - iApply greatest_fixpoint_unfold. eauto.
+    - iApply (greatest_fixpoint_strong_mono with "[] Hgfp"); eauto.
+  Qed.
+End greatest_coind.

iris/bi/lib/relations.v

@@ -57,7 +57,7 @@ Section bi_rtc.
     ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
  Proof.
     iIntros (?) "#IH". rewrite /bi_rtc.
-    by iApply (least_fixpoint_strong_ind (bi_rtc_pre R x2) with "IH").
+    by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
   Qed.
 
   Lemma bi_rtc_ind_l x2 Φ :
@@ -66,7 +66,7 @@ Section bi_rtc.
     ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
   Proof.
     iIntros (?) "#IH". rewrite /bi_rtc.
-    by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
+    by iApply (least_fixpoint_iter (bi_rtc_pre R x2) with "IH").
   Qed.
 
   Lemma bi_rtc_refl x : ⊢ bi_rtc R x x.

iris/program_logic/total_adequacy.v

@@ -43,7 +43,7 @@ Proof.
   iIntros "#IH" (t) "H".
   assert (NonExpansive Ψ).
   { by intros n ?? ->%(discrete_iff _ _)%leibniz_equiv. }
-  iApply (least_fixpoint_strong_ind _ Ψ with "[] H").
+  iApply (least_fixpoint_ind _ Ψ with "[] H").
   iIntros "!>" (t') "H". by iApply "IH".
 Qed.
 

iris/program_logic/total_weakestpre.v

@@ -88,7 +88,7 @@ Proof.
   assert (NonExpansive Ψ').
   { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
-  iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
+  iApply (least_fixpoint_ind _ Ψ' with "[] H").
   iIntros "!>" ([[??] ?]) "H". by iApply "IH".
 Qed.