From 557e604358b421a05f8532017b348033387c23e9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Sep 2017 01:31:41 +0200
Subject: [PATCH] A stronger induction principle for fixpoints.

---
 theories/base_logic/fixpoint.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/base_logic/fixpoint.v b/theories/base_logic/fixpoint.v
index 36a69473d..3d61e8629 100644
--- a/theories/base_logic/fixpoint.v
+++ b/theories/base_logic/fixpoint.v
@@ -52,6 +52,18 @@ Section least.
   Proof.
     iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
   Qed.
+
+  Lemma least_fixpoint_strong_ind (Φ : A → uPred M) `{!NonExpansive Φ} :
+    □ (∀ y, F (λ x, Φ x ∧ uPred_least_fixpoint F x) y → Φ y)
+    ⊢ ∀ x, uPred_least_fixpoint F x → Φ x.
+  Proof.
+    trans (∀ x, uPred_least_fixpoint F x → Φ x ∧ uPred_least_fixpoint F x)%I.
+    { iIntros "#HΦ". iApply least_fixpoint_ind; first solve_proper.
+      iIntros "!#" (y) "H". iSplit; first by iApply "HΦ".
+      iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[] H").
+      by iIntros "!# * [_ ?]". }
+    by setoid_rewrite and_elim_l.
+  Qed.
 End least.
 
 Section greatest.
-- 
GitLab