diff --git a/thys/Complete_Non_Orders/document/root.bib b/thys/Complete_Non_Orders/document/root.bib --- a/thys/Complete_Non_Orders/document/root.bib +++ b/thys/Complete_Non_Orders/document/root.bib @@ -1,289 +1,307 @@ %% This BibTeX bibliography file was created using BibDesk. %% http://bibdesk.sourceforge.net/ %% Created for Jeremy Dubut at 2019-03-29 18:38:21 +0900 %% Saved with string encoding Unicode (UTF-8) +@InProceedings{YamadaD2019, + author = {Akihisa Yamada and J{\'e}r{\'e}my Dubut}, + title = {{Complete Non-Orders and Fixed Points}}, + booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, + pages = {30:1--30:16}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-122-1}, + ISSN = {1868-8969}, + year = {2019}, + volume = {141}, + editor = {John Harrison and John O'Leary and Andrew Tolmach}, + publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, + address = {Dagstuhl, Germany}, + URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11085}, + URN = {urn:nbn:de:0030-drops-110852}, + doi = {10.4230/LIPIcs.ITP.2019.30}, + annote = {Keywords: Order Theory, Lattice Theory, Fixed-Points, Isabelle/HOL} +} @Inbook{Bergman2015, author="Bergman, George M.", title="Lattices, Closure Operators, and Galois Connections", bookTitle="An Invitation to General Algebra and Universal Constructions", year="2015", publisher="Springer International Publishing", address="Cham", pages="173--212", isbn="978-3-319-11478-1", doi="10.1007/978-3-319-11478-1_6", url="https://doi.org/10.1007/978-3-319-11478-1_6" } @book{Schmidt1993, author="Schmidt, Gunther and Str{\"o}hlein, Thomas", title="Relations and Graphs: Discrete Mathematics for Computer Scientists", year="1993", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="5--27", } @book{gierz03, Author = {G. Gierz and K. H. Hofmann and K. Keimel and J. D. Lawson and M. W. Mislove and D. S. Scott}, Date-Added = {2019-03-29 18:36:56 +0900}, Date-Modified = {2019-03-29 18:38:15 +0900}, Publisher = {Cambridge University Press}, Title = {Continuous Lattices and Domains}, Year = {2003}} @book{abramski94, Author = {Samson Abramsky and Achim Jung}, Date-Added = {2019-03-29 18:27:24 +0900}, Date-Modified = {2019-03-29 18:30:21 +0900}, Number = {III}, Publisher = {Oxford University Press}, Series = {Handbook of Logic in Computer Science}, Title = {Domain Theory}, Year = {1994}} @book{davey02, Author = {B. A. Davey and H. A. Priestley}, Date-Added = {2019-03-29 18:24:39 +0900}, Date-Modified = {2019-03-29 18:25:37 +0900}, Publisher = {Cambridge University Press}, Title = {Introduction to Lattices and Order}, Year = {2002}} @article{mashburn83, Author = {J. D. Mashburn}, Date-Added = {2019-03-27 22:36:00 +0900}, Date-Modified = {2019-03-27 22:38:19 +0900}, Journal = {Houston Journal of Mathematics}, Number = {2}, Pages = {231--244}, Title = {The least fixed point property for omega-chain continuous functions}, Volume = {9}, Year = {1983}} @article{tarski55, Author = {Alfred Tarski}, Date-Added = {2019-03-27 11:16:30 +0900}, Date-Modified = {2019-03-27 11:17:45 +0900}, Journal = {Pacific Journal of Mathematics}, Number = {2}, Pages = {285--309}, Title = {A lattice-theoretical fixpoint theorem and its applications}, Volume = {5}, Year = {1955}} @article{trellis, Author = {Skala, H.L.}, Doi = {10.1007/BF02944982}, Issue = 1, Journal = {Algebra Univ.}, Pages = {218--233}, Title = {Trellis theory}, Volume = 1, Year = 1971, Bdsk-Url-1 = {https://doi.org/10.1007/BF02944982}} @article{SM13, Author = {Stouti, Abdelkader and Maaden, Abdelhakim}, Doi = {10.4067/S0716-09172013000400008}, Journal = {Proyecciones. Revista de Matem{\'a}tica}, Number = {4}, Pages = {409-418}, Title = {Fixed points and common fixed points theorems in pseudo-ordered sets}, Volume = {32}, Year = {2013}, Bdsk-Url-1 = {https://doi.org/10.4067/S0716-09172013000400008}} @article{LN83, Author = {Leutola, K and Nieminen, J}, Journal = {Algebra Universalis}, Number = {1}, Pages = {344--354}, Publisher = {Springer}, Title = {Posets and generalized lattices}, Volume = {16}, Year = {1983}} @article{Bhatta05, Author = {Bhatta, S Parameshwara}, Journal = {Czechoslovak Mathematical Journal}, Number = {2}, Pages = {365--369}, Publisher = {Springer}, Title = {Weak chain-completeness and fixed point property for pseudo-ordered sets}, Volume = {55}, Year = {2005}} @article{PG11, Author = {Parameshwara Bhatta, S and George, Shiju}, Journal = {Algebra and Discrete Mathematics}, Number = {1}, Pages = {17--22}, Publisher = {Луганский национальный университет им. Т. Шевченко}, Title = {Some fixed point theorems for pseudo ordered sets}, Volume = {11}, Year = {2011}} @article{flyspeck, Author = {Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat Dat and Harrison, John and Le Truong, Hoang and Kaliszyk, Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat Thang and others}, Journal = {Forum of Mathematics, Pi}, Publisher = {Cambridge University Press}, Title = {A formal proof of the {K}epler conjecture}, Volume = {5}, Year = {2017}} @article{4color, Author = {Gonthier, Georges}, Journal = {Notices of the AMS}, Number = {11}, Pages = {1382--1393}, Title = {Formal proof -- the four-color theorem}, Volume = {55}, Year = {2008}} @inproceedings{sel4, Author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and others}, Booktitle = {Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems principles}, Organization = {ACM}, Pages = {207--220}, Title = {se{L}4: Formal verification of an {OS} kernel}, Year = {2009}} @inproceedings{isabelle/jedit, Author = {Wenzel, Makarius}, Booktitle = {International Conference on Intelligent Computer Mathematics}, Organization = {Springer}, Pages = {468--471}, Title = {{I}sabelle/j{E}dit--a Prover {IDE} within the {PIDE} framework}, Year = {2012}} @inproceedings{quickcheck, Acmid = {1030056}, Address = {Washington, DC, USA}, Author = {Berghofer, Stefan and Nipkow, Tobias}, Booktitle = {Proceedings of the Software Engineering and Formal Methods, Second International Conference}, Doi = {10.1109/SEFM.2004.36}, OPIsbn = {0-7695-2222-X}, Numpages = {10}, Pages = {230--239}, Publisher = {IEEE Computer Society}, Series = {SEFM '04}, Title = {Random Testing in {I}sabelle/{HOL}}, Year = {2004}, Bdsk-Url-1 = {http://dx.doi.org/10.1109/SEFM.2004.36}} @inproceedings{nitpick, Address = {Berlin, Heidelberg}, Author = {Blanchette, Jasmin Christian and Nipkow, Tobias}, Booktitle = {Interactive Theorem Proving}, Editor = {Kaufmann, Matt and Paulson, Lawrence C.}, OPIsbn = {978-3-642-14052-5}, Pages = {131--146}, Publisher = {Springer Berlin Heidelberg}, Title = {Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder}, Year = {2010}} @inproceedings{codegen, Author = {Haftmann, Florian and Nipkow, Tobias}, Booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2007)}, Pages = {128--143}, Series = {Lecture Notes in Computer Science}, Title = {A code generator framework for {I}sabelle/{HOL}}, Volume = {4732}, Year = {2007}} @inproceedings{locale, Address = {Berlin, Heidelberg}, Author = {Ballarin, Clemens}, Booktitle = {Mathematical Knowledge Management}, Doi = {10.1007/11812289_4}, Editor = {Borwein, Jonathan M. and Farmer, William M.}, OPIsbn = {978-3-540-37106-9}, Pages = {31--43}, Publisher = {Springer Berlin Heidelberg}, Title = {Interpretation of Locales in {I}sabelle: Theories and Proof Contexts}, Year = {2006}, Bdsk-Url-1 = {https://doi.org/10.1007/11812289_4}} @inproceedings{Kammuller00, Address = {Berlin, Heidelberg}, Author = {Kamm{\"u}ller, Florian}, Booktitle = {Automated Deduction - CADE-17}, Doi = {10.1007/10721959_7}, Editor = {McAllester, David}, OPIsbn = {978-3-540-45101-3}, Pages = {99--114}, Publisher = {Springer Berlin Heidelberg}, Title = {Modular Reasoning in {I}sabelle}, Year = {2000}, Bdsk-Url-1 = {https://doi.org/10.1007/10721959_7}} @inproceedings{isafor, title={Certification of termination proofs using {CeTA}}, author={Thiemann, Ren{\'e} and Sternagel, Christian}, booktitle={International Conference on Theorem Proving in Higher Order Logics}, pages={452--468}, year={2009}, organization={Springer} } @book{Isabelle, Author = {T.~Nipkow and L.C.~Paulson and M.~Wenzel}, Publisher = {Springer}, Series = {LNCS}, Title = {{Isabelle/HOL} -- A Proof Assistant for Higher-Order Logic}, Volume = 2283, Year = 2002 } @inproceedings{hol4, title={A brief overview of {HOL4}}, author={Slind, Konrad and Norrish, Michael}, booktitle={International Conference on Theorem Proving in Higher Order Logics}, pages={28--32}, year={2008}, organization={Springer} } @inproceedings{hol-light, title={{HOL} light: An overview}, author={Harrison, John}, booktitle={International Conference on Theorem Proving in Higher Order Logics}, pages={60--66}, year={2009}, organization={Springer} } @inproceedings{agda, title={A brief overview of {A}gda -- a functional language with dependent types}, author={Bove, Ana and Dybjer, Peter and Norell, Ulf}, booktitle={International Conference on Theorem Proving in Higher Order Logics}, pages={73--78}, year={2009}, organization={Springer} } @book{coq, title={Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant}, author={Chlipala, Adam}, year={2013}, publisher={MIT Press} } @inproceedings{compcert, title={Formal {C} semantics: {C}omp{C}ert and the {C} standard}, author={Krebbers, Robbert and Leroy, Xavier and Wiedijk, Freek}, booktitle={International Conference on Interactive Theorem Proving}, pages={543--548}, year={2014}, organization={Springer} } @inproceedings{sledgehammer, title={Sledgehammer: judgement day}, author={B{\"o}hme, Sascha and Nipkow, Tobias}, booktitle={International Joint Conference on Automated Reasoning}, pages={107--121}, year={2010}, organization={Springer} } diff --git a/thys/Complete_Non_Orders/document/root.tex b/thys/Complete_Non_Orders/document/root.tex --- a/thys/Complete_Non_Orders/document/root.tex +++ b/thys/Complete_Non_Orders/document/root.tex @@ -1,193 +1,195 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb,amsmath,stmaryrd} \usepackage{tikz} \usetikzlibrary{backgrounds} \usetikzlibrary{positioning} \usetikzlibrary{shapes} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \newcommand\SLE{\sqsubseteq} \newcommand\Nat{\mathbb{N}} \makeatletter \def\tp@#1#2{\@ifnextchar[{\tp@@{#1}{#2}}{\tp@@@{#1}{#2}}} \def\tp@@#1#2[#3]#4{#3#1\def\mid{\mathrel{#3|}}#4#3#2} \def\tp@@@#1#2#3{\bgroup\left#1\def\mid{\;\middle|\;}#3\right#2\egroup} \def\pa{\tp@()} \def\tp{\tp@\langle\rangle} \def\set{\tp@\{\}} \makeatother \begin{document} \title{Complete Non-Orders and Fixed Points} \author{Akihisa Yamada and Jérémy Dubut} \maketitle \begin{abstract} We develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any properties of ordering, thus complete non-orders. In particular, we generalize the Knaster--Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition---% attractivity---which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene's fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene's fixed points are least quasi-fixed points. \end{abstract} \tableofcontents \section{Introduction} The main driving force towards mechanizing mathematics using proof assistants has been the reliability they offer, exemplified prominently by~\cite{4color},~\cite{flyspeck},~\cite{sel4}, etc. In this work, we utilize another aspect of Isabelle/JEdit~\cite{isabelle/jedit} as engineering tools for developing mathematical theories. We formalize order-theoretic concepts and results, adhering to an \emph{as-general-as-possible} approach: most results concerning order-theoretic completeness and fixed-point theorems are proved without assuming the underlying relations to be orders (non-orders). In particular, we provide the following: \begin{itemize} \item A locale-based library for binary relations, as partly depicted in Figure~\ref{fig:non-orders}. \item Various completeness results that generalize known theorems in order theory: Actually most relationships and duality of completeness conditions are proved without \emph{any} properties of the underlying relations. \item Existence of fixed points: We show that a relation-preserving mapping $f : A \to A$ over a complete non-order $\tp{A,\SLE}$ admits a \emph{quasi-fixed point} $f(x) \sim x$, meaning $x \SLE f(x) \wedge f(x) \SLE x$. Clearly if $\SLE$ is antisymmetric then this implies the existence of fixed points $f(x) = x$. \item Completeness of the set of fixed points: We further show that if $\SLE$ satisfies a mild condition, which we call \emph{attractivity} and which is implied by either transitivity or antisymmetry, then the set of quasi-fixed points is complete. Furthermore, we also show that if $\SLE$ is antisymmetric, then the set of \emph{strict} fixed points $f(x) = x$ is complete. \item Kleene-style fixed-point theorems: For an $\omega$-complete non-order $\tp{A,\SLE}$ with a bottom element $\bot \in A$ (not necessarily unique) and for every $\omega$-continuous map $f : A \to A$, a supremum exists for the set $\set{ f^n(\bot) \mid n \in \Nat}$, and it is a quasi-fixed point. If $\SLE$ is attractive, then the quasi-fixed points obtained this way are precisely the least quasi-fixed points. \end{itemize} We remark that all these results would have required much more effort than we spent (if possible at all), if we were not with the smart assistance by Isabelle. Our workflow was often the following: first we formalize existing proofs, try relaxing assumptions, see where proof breaks, and at some point ask for a counterexample. \begin{figure} \small \centering \def\isa#1{\textsf{#1}} \def\t{-1.8} \def\a{3.6} \def\at{1.8} \def\s{-3.6} \def\st{-5.4} \begin{tikzpicture} \tikzstyle{every node}=[draw,ellipse] \tikzstyle{every edge}=[draw] \draw (0,0) node[fill] (rel) {} (\t,1) node (trans) {\isa{transitive}} (0,-2) node (refl) {\isa{reflexive}} (0,2) node (irr) {\isa{irreflexive}} (\s,0) node (sym) {\isa{symmetric}} (\a,0) node (anti) {\isa{antisymmetric}} (\at,1) node (near) {\isa{near\_order}} (\a,2) node (asym) {\isa{asymmetric}} (\a,-2) node (pso) {\isa{pseudo\_order}} (\at,-1) node (po) {\isa{partial\_order}} (\t,-1) node (qo) {\isa{quasi\_order}} (0,3) node (str) {\hspace{3em}\isa{strict\_order}\mbox{\hspace{3em}}} (\st,-1) node (equiv) {\isa{equivalence}} (\st,1) node (peq) {\hspace{-.8em}\isa{partial\_equivalence}\mbox{\hspace{-.8em}}} (\st,3) node (emp) {$\emptyset$} (\s,-2) node (tol) {\isa{tolerance}} (\s,2) node (ntol) {$\neg$\isa{tolerance}} ; \draw[->] (near) edge[color=blue] ([xshift=51,yshift=-7]str) (irr) edge[color=red] ([xshift=-46,yshift=-8]str) (trans) edge[color=blue] ([xshift=-51,yshift=-7]str) (asym) edge[color=red] ([xshift=55,yshift=-7]str) (trans) edge[color=green] (near) (anti) edge[color=red] (near) (irr) edge[color=green] (asym) (anti) edge[color=blue] (asym) (anti) edge[color=blue] (pso) (near) edge[color=blue] (po) (pso) edge[color=red] (po) (refl) edge[color=green] (pso) (trans) edge[color=blue] (qo) (refl) edge[color=red] (qo) (qo) edge[color=green] (po) (qo) edge[color=green] (equiv) (peq) edge[color=blue] (equiv) (trans) edge[color=green] (peq) (peq) edge[color=blue] (emp) (str) edge[color=green] (emp) (sym) edge[color=red] (peq) (sym) edge[color=blue] (tol) (sym) edge[color=blue] (ntol) (irr) edge[color=green] (ntol) (refl) edge[color=green] (tol) (ntol) edge[color=red] (emp) (tol) edge[color=red] (equiv) (rel) edge[color=red, line width=1.5pt] (trans) (rel) edge[color=blue, line width=1.5pt] (irr) (rel) edge[color=blue, line width=1.5pt] (refl) (rel) edge[color=green, line width=1.5pt] (sym) (rel) edge[color=green, line width=1.5pt] (anti) ; \end{tikzpicture} \caption{\label{fig:non-orders} Combinations of basic properties. The black dot around the center represents arbitrary binary relations, and the five outgoing arrows indicate atomic assumptions. We do not present the combination of \isa{reflexive} and \isa{irreflexive}, which is empty, and one of \isa{symmetric} and \isa{antisymmetric}, which is a subset of equality. Node ``$\neg$\isa{tolerance}'' indicates the negated relation is \isa{tolerance}, and ``$\emptyset$'' is the empty relation. } \end{figure} \paragraph*{Related Work} Many attempts have been made to generalize the notion of completeness for lattices, conducted in different directions: by relaxing the notion of order itself, removing transitivity (pseudo-orders \cite{trellis}); by relaxing the notion of lattice, considering minimal upper bounds instead of least upper bounds ($\chi$-posets \cite{LN83}); by relaxing the notion of completeness, requiring the existence of least upper bounds for restricted classes of subsets (e.g., directed complete and $\omega$-complete, see \cite{davey02} for a textbook). Considering those generalizations, it was natural to prove new versions of classical fixed-point theorems for maps preserving those structures, e.g., existence of least fixed points for monotone maps on (weak chain) complete pseudo-orders \cite{Bhatta05, SM13}, construction of least fixed points for $\omega$-continuous functions for $\omega$-complete lattices \cite{mashburn83}, (weak chain) completeness of the set of fixed points for monotone functions on (weak chain) complete pseudo-orders \cite{PG11}. Concerning Isabelle formalization, one can easily find several formalizations of complete partial orders or lattices in Isabelle's standard library. They are, however, defined on partial orders, either in form of classes or locales, and thus not directly reusable for non-orders. Nevertheless we tried to make our formalization compatible with the existing ones, and various correspondences are ensured. +This work has been published in the conference paper \cite{YamadaD2019}. + % include generated text of all theories \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document}