Commit 38b6c303 authored by Ralf Jung's avatar Ralf Jung
Browse files

more CHANGELOG

parent 2708e2c5
...@@ -9,10 +9,10 @@ Changes in and extensions of the theory: ...@@ -9,10 +9,10 @@ Changes in and extensions of the theory:
* [#] Add new modality: ■ ("plainly"). * [#] Add new modality: ■ ("plainly").
* [#] Camera morphisms have to be homomorphisms, not just monotone functions. * [#] Camera morphisms have to be homomorphisms, not just monotone functions.
* [#] Add a proof that `f` has a fixed point if `f^k` is contractive. * Add a proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates * Constructions for least and greatest fixed points over monotone predicates
(defined in the logic of Iris using impredicative quantification). (defined in the logic of Iris using impredicative quantification).
* A proof of the inverse of `wp_bind`. * Add a proof of the inverse of `wp_bind`.
Changes in Coq: Changes in Coq:
......
...@@ -75,6 +75,7 @@ The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the d ...@@ -75,6 +75,7 @@ The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the d
Completeness is necessary to take fixed-points. Completeness is necessary to take fixed-points.
For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$. For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
This also holds if $f^k$ is contractive for an arbitrary $k$.
Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point. Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment