From b22e6980a87a64b342f723540840e881cd4a621f Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Fri, 23 Dec 2016 23:30:03 +0100 Subject: [PATCH] Coinduction principle on fixpoints. --- theories/algebra/ofe.v | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 2d4d87dd..f5da06ee 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -231,6 +231,24 @@ Section fixpoint. Lemma fixpoint_proper (g : A → A) `{!Contractive g} : (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. + + Lemma fixpoint_ind (P : A → Prop) : + Proper ((≡) ==> iff) P → + (∃ x, P x) → (∀ x, P x → P (f x)) → + (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) → + P (fixpoint f). + Proof. + intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x). + assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n). + { intros n. induction n as [|n IH]=> -[|i] //= ?; try omega. + - apply (contractive_0 f). + - apply (contractive_S f), IH; auto with omega. } + set (fp2 := compl {| chain_cauchy := Hcauch |}). + rewrite -(fixpoint_unique fp2); first by apply Hlim; induction n; apply Hincr. + apply equiv_dist=>n. + rewrite /fp2 (conv_compl n) /= /chcar. + induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. + Qed. End fixpoint. (** Mutual fixpoints *) @@ -863,7 +881,7 @@ Section later. Program Definition later_chain (c : chain laterC) : chain A := {| chain_car n := later_car (c (S n)) |}. Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed. - Global Program Instance later_cofe `{Cofe A} : Cofe laterC := + Global Program Instance later_cofe `{Cofe A} : Cofe laterC := { compl c := Next (compl (later_chain c)) }. Next Obligation. intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))]. -- GitLab