From 1b4ded4d55cff2a09a35f716e4d0732d4c006551 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 25 Jan 2017 12:52:09 +0100 Subject: [PATCH] Prove fixpointK stuff without unfolding the definition of fixpoint. Also, give names to hypotheses that we refer to. --- theories/algebra/ofe.v | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 305c0f7e..28ecdb3a 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -267,34 +267,35 @@ Definition fixpointK `{Cofe A, Inhabited A} k (f : A → A) Section fixpointK. Local Set Default Proof Using "Type*". - Context `{Cofe A, Inhabited A} (f : A → A) k `{!Contractive (Nat.iter k f)}. + Context `{Cofe A, Inhabited A} (f : A → A) (k : nat). + Context `{f_contractive : !Contractive (Nat.iter k f)}. (* TODO: Can we get rid of this assumption, derive it from contractivity? *) - Context `{!∀ n, Proper (dist n ==> dist n) f}. + Context `{f_ne : !∀ n, Proper (dist n ==> dist n) f}. + + Let f_proper : Proper ((≡) ==> (≡)) f := ne_proper f. + Existing Instance f_proper. Lemma fixpointK_unfold : fixpointK k f ≡ f (fixpointK k f). Proof. - apply equiv_dist=>n. - rewrite /fixpointK fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain _)) //. - induction n as [|n IH]; simpl. - - rewrite -Nat_iter_S Nat_iter_S_r. eapply contractive_0; first done. - - rewrite -[f _]Nat_iter_S Nat_iter_S_r. eapply contractive_S; first done. eauto. + symmetry. rewrite /fixpointK. apply fixpoint_unique. + by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold. Qed. Lemma fixpointK_unique (x : A) : x ≡ f x → x ≡ fixpointK k f. Proof. - intros Hf. apply fixpoint_unique, equiv_dist=>n. - (* Forward reasoning is so annoying... *) - assert (x ≡{n}≡ f x) by by apply equiv_dist. - clear Contractive0. induction k; first done. by rewrite {1}Hf {1}IHn0. + intros Hf. apply fixpoint_unique. clear f_contractive. + induction k as [|k' IH]=> //=. by rewrite -IH. Qed. Section fixpointK_ne. - Context (g : A → A) `{!Contractive (Nat.iter k g), !∀ n, Proper (dist n ==> dist n) g}. + Context (g : A → A) `{g_contractive : !Contractive (Nat.iter k g)}. + Context {g_ne : ∀ n, Proper (dist n ==> dist n) g}. Lemma fixpointK_ne n : (∀ z, f z ≡{n}≡ g z) → fixpointK k f ≡{n}≡ fixpointK k g. Proof. - rewrite /fixpointK=>Hne /=. apply fixpoint_ne=>? /=. clear Contractive0 Contractive1. - induction k; first by auto. simpl. rewrite IHn0. apply Hne. + rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z. + clear f_contractive g_contractive. + induction k as [|k' IH]=> //=. by rewrite IH Hfg. Qed. Lemma fixpointK_proper : (∀ z, f z ≡ g z) → fixpointK k f ≡ fixpointK k g. -- GitLab