Commit 738d8bcc by Robbert Krebbers

### Prove uniqueness of Banach's fixpoint.

parent 3a8e6a91
 ... @@ -188,12 +188,23 @@ Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux. ... @@ -188,12 +188,23 @@ Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux. Section fixpoint. Section fixpoint. Context {A : cofeT} {Inhabited A} (f : A → A) {!Contractive f}. Context {A : cofeT} {Inhabited A} (f : A → A) {!Contractive f}. Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). Proof. Proof. apply equiv_dist=>n. apply equiv_dist=>n. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //. induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. Qed. Qed. Lemma fixpoint_unique (x : A) : x ≡ f x → x ≡ fixpoint f. Proof. rewrite !equiv_dist=> Hx n. rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //=. induction n as [|n IH]; simpl in *. - rewrite Hx; eauto using contractive_0. - rewrite Hx. apply (contractive_S _), IH. Qed. Lemma fixpoint_ne (g : A → A) {!Contractive g} n : Lemma fixpoint_ne (g : A → A) {!Contractive g} n : (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g. Proof. Proof. ... ...
 ... @@ -39,7 +39,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e ... @@ -39,7 +39,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e \end{defn} \end{defn} Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data. Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data. Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$. Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$. The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique}\footnote{Uniqueness is not proven in Coq.} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. \begin{defn} \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!