From 738d8bcc90f41dc05434609e4d35d0976a7c39dc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 21 Aug 2016 23:32:12 +0200
Subject: [PATCH] Prove uniqueness of Banach's fixpoint.

---
 algebra/cofe.v   | 11 +++++++++++
 docs/algebra.tex |  2 +-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 9742a0915..d2f120f50 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -188,12 +188,23 @@ Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
 
 Section fixpoint.
   Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
+
   Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
   Proof.
     apply equiv_dist=>n.
     rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
     induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
   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 :
     (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
   Proof.
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 494fb54c7..e9b3208e4 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -39,7 +39,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e
 \end{defn}
 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$.
-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}
   The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
-- 
GitLab