From 94861f1df3a37a26a16401da99e40ccd59329610 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 21 Feb 2017 16:37:54 +0100
Subject: [PATCH] fixpointK_ind

---
 theories/algebra/ofe.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 58c004091..beddd2adc 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -330,6 +330,16 @@ Section fixpointK.
     Lemma fixpointK_proper : (∀ z, f z ≡ g z) → fixpointK k f ≡ fixpointK k g.
     Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpointK_ne. Qed.
   End fixpointK_ne.
+
+  Lemma fixpointK_ind (P : A → Prop) :
+    Proper ((≡) ==> impl) P →
+    (∃ x, P x) → (∀ x, P x → P (f x)) →
+    (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) →
+    P (fixpointK k f).
+  Proof.
+    intros ? Hst Hincr Hlim. rewrite /fixpointK. eapply fixpoint_ind; [done..| |done].
+    clear- Hincr. intros. induction k; first done. simpl. auto.
+  Qed.
 End fixpointK.
 
 (** Mutual fixpoints *)
-- 
GitLab