diff --git a/ch15_general_recursion/SRC/log2_function.v b/ch15_general_recursion/SRC/log2_function.v index f920fbe..cf9b919 100644 --- a/ch15_general_recursion/SRC/log2_function.v +++ b/ch15_general_recursion/SRC/log2_function.v @@ -83,7 +83,8 @@ Proof. intro H. case_eq (exp2 p). * intro H0; destruct (exp2_positive p);auto. - * intros n H0; rewrite H0 in H; elimtype False; lia. + * intros n H0; rewrite H0 in H. assert (H1:False) by lia. + destruct H1. - intros p H; destruct p. + simpl in H; subst n; contradiction. + simpl in H; rewrite (IHn0 p); auto. diff --git a/ch16_proof_by_reflection/SRC/prime_sqrt.v b/ch16_proof_by_reflection/SRC/prime_sqrt.v index d860638..3d169e9 100644 --- a/ch16_proof_by_reflection/SRC/prime_sqrt.v +++ b/ch16_proof_by_reflection/SRC/prime_sqrt.v @@ -122,7 +122,7 @@ Theorem test_odds_correct : Proof. induction n. - intros x p Hp1 H1ltx Hn q Hint. - elimtype False; lia. + assert (FF: False) by lia; destruct FF. - intros x p Hp H1ltx; simpl (test_odds (S n) p (Z_of_nat x)); intros Htest q (H1ltq, Hqle). case_eq (test_odds n (p -2) (Z_of_nat x)). diff --git a/doc/typeClassesTut/.gitignore b/doc/typeClassesTut/.gitignore new file mode 100644 index 0000000..994b719 --- /dev/null +++ b/doc/typeClassesTut/.gitignore @@ -0,0 +1,6 @@ +*.pdf +*.log +*.aux +*.blg +*.out +*.bbl \ No newline at end of file diff --git a/doc/typeClassesTut/Makefile b/doc/typeClassesTut/Makefile new file mode 100644 index 0000000..4a90d47 --- /dev/null +++ b/doc/typeClassesTut/Makefile @@ -0,0 +1,18 @@ +DEP_Files = typeclassestut.tex \ + morebiblio.bib \ + biblio.bib + +.PHONY:all +all: typeclassestut.pdf + +typeclassestut.pdf: ${DEP_Files} + lualatex typeclassestut.tex + bibtex typeclassestut + lualatex typeclassestut.tex + lualatex typeclassestut.tex + lualatex typeclassestut.tex + + +.PHONY:clean +clean: + @${RM} typeclassestut.pdf *.aux *.ind *.bbl *.blg *.log *.out diff --git a/doc/typeClassesTut/biblio.bib b/doc/typeClassesTut/biblio.bib new file mode 100644 index 0000000..a7f4910 --- /dev/null +++ b/doc/typeClassesTut/biblio.bib @@ -0,0 +1,987 @@ +\bibliographystyle{plain} + +@book{luo94, + author = {Zhaohui Luo}, + publisher = "Oxford University Press", + year =1994, + title = {{Computation and Reasoning -- A Type Theory for Computer Science}} +} + +@ARTICLE{PaulinWerner93, + author = {Christine Paulin-Mohring and Benjamin Werner}, + journal = {Journal of Symbolic Computation}, + title = {{Synthesis of ML programs in the system Coq}}, + publisher = {Academic Press}, + volume = {15}, + year = {1993}, + pages = {607--640} +} + +@ARTICLE{mizar78, + author={Andrzej Trybulec}, + journal={ALLC Bulletin}, + title={The {M}izar-QC/6000 Logic Information Language}, + volume={6}, + number={2}, + pages={136--140}, + year={1978} +} + +@inproceedings{floyd67, + title = "Assigning Meanings to Programs", + author = "Robert W. Floyd", + editor = "J. T. Schwartz", + booktitle = "Mathematical Aspects of Computer Science: 19th + Symposium on Applied Mathematics", + pages = "19--31", + location = "Providence, United States", + year = 1967 +} + +@book{dijkstra76, + title = "A discipline of Programming", + author = "Edsger W. Dijkstra", + publisher = "Prentice Hall", + year = 1976 +} + +@INPROCEEDINGS{tphols2000-Balaa, + crossref = "tphols2000", + title = "Fix-point Equations for Well-Founded Recursion in Type Theory", + author = "Antonia Balaa and Yves Bertot", + pages = "1--16"} + +@book{fourier1890, +title = "Oeuvre de Fourier", +author = "Jean-Baptiste-Joseph Fourier", +note = "PubliÈ par les soins de Gaston Darboux", +year = 1890, +publisher = "Gauthier-Villars", +} + +@inproceedings{Hilbert1925, + crossref = "FregeGodel", + author = "David Hilbert", + title = "On the infinite", + pages = "367--392", + year = 1925 +} + +@inproceedings{Ackermann1928, + crossref = "FregeGodel", + author = "Wilhelm Ackermann", + title = "On {H}ilbert's construction of the real numbers", + pages = "493--507", + year = 1925 +} + +@inproceedings{Thery98, + title = "A certified version of {B}uchberger's algorithm", + author = "Laurent ThÈry", + booktitle = "Automated Deduction---CADE-15", + publisher="Springer-Verlag", + volume ="1421", + series="Lecture Notes in Artificial Intelligence", + pages={349--364}, + year = "1998" +} +@inproceedings{BuraliForti1897, + crossref = "FregeGodel", + author = "Wilhelm Ackermann", + title = "A question on transfinite numbers", + pages = "104--112", + year = 1925 +} + + + +@book{Dedekind1888, + title = "Was sind und was sollen die Zahlen?", + author = "Richard Dedekind", + publisher = "Vieweg", + year = "1988" +} + + +@article{BoveUnif, + title = "Simple General Recursion in Type Theory", + author = "Ana Bove", + journal = "Nordic Journal of Computing", + volume = 8, + number = 1, + pages = "22-42", + year = 2001 +} + +@inproceedings{tphols2002-BertotCaprettaDasBarman, + author= "Yves Bertot and Venanzio Capretta and Kuntal Das Barman", + title = "Type-theo\-re\-tic functional semantics", + booktitle = {Theorem Proving in Higher Order Logics (TPHOLS'02)}, + year = 2002, + location = "Hampton, Va", + series = "Lecture Notes in Computer Science", + publisher = "Springer-Verlag", + volume = 2410 +} + +@article{viewleft, + title = "The view from the left", + author = "Conor McBride and James McKinna", + journal = "Journal of Functional Programming", + volume = 14, + number = 1, + year = 2004 +} + +@inproceedings{Natural, + author = "Gilles Kahn", + title = "{N}atural semantics", + booktitle = "{P}rogramming of {F}uture {G}eneration {C}omputers", + editor = "K. Fuchi and M. Nivat", + publisher = "North-Holland", + year = 1988, +} + + +@article{hoare69, + title ="An Axiomatic Basis for Computer Programming", + author = "Charles Anthony Richard Hoare", + journal = "Communications of the ACM", + volume=12, + number=10, + pages ={576-580}, + year = 1969, +} + +%%% no point after "J" in "J Strother Moore" + +@Article{boyermoore, + author = {Robert S. Boyer and J Strother Moore}, + title = {Proving Theorems about LISP Functions}, + journal = {Journal of the ACM}, + year = {1975}, + volume = {22}, + number = {1}, + pages = {129-144}, +} + +%%% no point after "J" in "J Strother Moore" + +@Book{nqthm, + author = {Robert S. Boyer and J Strother Moore}, + title = {A Computational Logic Handbook}, + publisher = {Academic Press}, + year = {1988}, +} + +@Book{nuprl, + author = {Robert L. Constable and others}, + title = {Implementing Mathematics with the Nuprl Development System}, + publisher = {Prentice Hall}, + year = {1986}, +} + + +@article{induction-recursion, + author={Peter Dybjer}, + title = {A general formulation of simultaneous inductive-recursive definitions in type theory}, + journal = {Journal of Symbolic Logic}, + publisher={Association for Symbolic Logic}, + volume = 65, + number = 2, + year = 2000, +} + +@TechReport{lego92, + author = {Zhaohui Luo and Randy Pollack}, + title = {LEGO Proof Development System: user's manual}, + institution = { LFCS (Edinburgh University)}, + year = {1992}, + number = {ECS-LFCS-92-211}, +} + + +@inproceedings{Luo89, + title = "An extended Calculus of Constructions", + author = "Zhaohui Luo", + booktitle = "Proceedings of the 4th annual symposium on Logic In Computer Science (LICS'89)", + year = 1989 +} + +@book{ProofTypes, + author = "Jean-Yves Girard and Yves Lafont and Paul Taylor", + title = "Proofs and types", + publisher = "Cambridge University Press", + year = 1989, +} + +@book{FregeGodel, + editor = "Jean van Heijenoort", + title = "From Frege to G{\"o}del: a source book in mathematical logic, 1879-1931", + publisher = "Harvard University Press", + year = 1981, +} + + + +@inproceedings{huet88, + title="Induction principles formalized in the calculus of constructions", + booktitle="Programming of Future Generation Computers", + author = "GÈrard Huet", + year=1988, + editor="K. Fuchi and M. Nivat", + publisher="North-Holland", + pages = "205--216" +} +@inproceedings{Aczel77, +title = "An introduction to inductive definitions", +year= 1977, +editor = "J. Barwise", +author = "Peter Aczel", +publisher = "North-Holland", +volume = "90", +series = "Studies in Logic and the Foundations of Mathematics", +booktitle = "{H}andbook of {M}athematical {L}ogic" +} + +@book{Burge, +title="Recursive Programming Techniques", +author="William H. Burge", +publisher="Addison-Wesley", +year=1975, +} + +@Incollection{Mitchell, + author = {John C. Mitchell}, + editor = {J. van Leeuwen}, + booktitle = {Handbook of Theoretical Computer Science, Volume B~:Formal Models and Semantics}, + title = "Type Systems for Programming Languages", + publisher = {MIT Press and Elsevier}, + year = {1994}, +} + +@article{barendregt, + author = {Henk Barendregt}, + title = {Introduction to generalized type systems}, + journal = {Journal of Functional Programming}, + pages = "125-154", + volume="1(2)", + month = "April", + year = {1991}, +} +@article{RacineCarreeGMP, + author = {Yves Bertot and Nicolas Magaud and Paul Zimmermann}, + title = {A proof of {GMP} square root}, + journal = {Journal of Automated Reasoning}, + publisher = {Kluwer Academic Publishers}, + volume = "29", + pages = "225-252", + year = 2002} + + + +@Article{wand, + author = {Mitchell Wand}, + title = {Continuation-Based Program Transformation Strategies}, + journal = {Journal of the ACM}, + year = {1980}, + volume = {27}, + number = {1}, + pages = {164-180}, + month = {January}, +} + +@InProceedings{dr1, + author ="Pierre Cast\'eran and Davy Rouillard", + title = "Reasoning about Parametrized Automata", + booktitle = "Proceedings, 8-th International Conference on Real-Time System", + volume = "8", + pages = "107-119", + year = "2000", +} + + +@InProceedings{conor:motive, + author ="Conor McBride", + title = "Elimination with a motive", + booktitle = "Types for Proofs and Programs'2000", + volume = 2277, + pages = "197-217", + year = "2002", +} + +@article{coupet2, + author="Solange Coupet-Grimal", + title="An axiomatization of Linear Temporal Logic in The Calculus of Inductive Constructions", + journal="Journal of Logic and Computation", + publisher = "Oxford University Press", + year="2003", + volume = 13, + number = 6, + pages = "801--813" +} + + +@inproceedings {coupet3, + author = {{Coupet-Grimal}, Solange and {Jakubiec}, Line}, + title = {Hardware Verification using co-induction in COQ}, + booktitle = {TPHOLs'99}, + series = {Lecture Notes in Computer Science}, + volume = {1690}, + year = {1999}, + publisher = {Springer-Verlag} +} + +@book{CurryFeys58, + author="Haskell B. Curry and Robert Feys", + title= "Combinatory Logic I", + publisher="North- Holland", + year="1958", +} + +@ARTICLE{Filliatre00a, + AUTHOR = {Jean-Christophe Filli\^atre}, + TITLE = {{Verification of non-functional programs + using interpretations in type theory}}, + JOURNAL = {Journal of Functional Programming}, + publisher ={Cambridge University Press}, +YEAR = 2003, + pages = {709-745}, + volume={13}, + number={4}, + URL = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, + ABSTRACT = {We study the problem of certifying programs combining imperative and + functional features within the general framework of type theory. + + Type theory constitutes a powerful specification language, which is + naturally suited for the proof of purely functional programs. To + deal with imperative programs, we propose a logical interpretation + of an annotated program as a partial proof of its specification. The + construction of the corresponding partial proof term is based on a + static analysis of the effects of the program, and on the use of + monads. The usual notion of monads is refined in order to account + for the notion of effect. The missing subterms in the partial proof + term are seen as proof obligations, whose actual proofs are left to + the user. We show that the validity of those proof obligations + implies the total correctness of the program. + We also establish a result of partial completeness. + + This work has been implemented in the Coq proof assistant. + It appears as a tactic taking an annotated program as argument and + generating a set of proof obligations. Several nontrivial + algorithms have been certified using this tactic.} +} + +@inproceedings{Gimenez, +title = "An Application of Co-Inductive Types in {C}oq: Verification of the Alternating Bit Protocol", +author = "Eduardo Gimenez", +booktitle = {\sl Proceedings of the 1995 Workshop on Types for Proofs and Programs}, +series= {Lecture Notes in Computer Science}, +volume= {1158}, +pages= {135-152}, +year = 1995, +publisher= {Springer-Verlag}, +} + + +@Book{Heyting, + author = {Arend Heyting}, + title = {Intuitionism - an Introduction}, + publisher = {North-Holland}, + year = {1971}, +} + +@inproceedings{Scott-constructions, + title="Constructive Validity", + author="Dana Scott", + booktitle = "Proceedings of Symposium on Automatic Demonstration", + volume =125, + Series = "Lecture Notes in Mathematics", + pages = "237-275", + publisher = "Springer-Verlag", + year = 1970 +} + +@incollection{Howard, +title="The formulae-as-types notion of construction", +author="William A. Howard", +booktitle= "To H. B. Curry: Essays on combinatory logic, Lambda Calculus and +Formalism", +year = 1980, +pages = "479-490", +editor="J. P. Seldin and J. R. Hindley", +publisher = "Academic Press", +} + +@book{martin-lof:typetheory, + title = "Intuitionistic type theories", + author = "Per Martin-L{\"o}f", + publisher = "Bibliopolis", + year = 1984 +} + +@inproceedings{Parent, +title = "Synthesizing Proofs from Programs in the Calculus of Inductive Constructions", +author = "Catherine Parent", +booktitle = {\sl Proceedings of MPC'1995}, +series = {Lecture Notes in Computer Science}, +volume = 947, +pages = {351-379}, +year = 1995, +} + +@booklet{GimenezTut, +title="A tutorial on recursive types in {C}oq", +author="Eduardo Gimenez", +note="Documentation of the {C}oq system", +} + +@inproceedings{martinloftheory, +title = "Martin-L{\"o}f's Type Theory", +author = "Bengt Nordstrom and Kent Petersson and Jan Smith", +booktitle="Handbook of Logic in Computer Science, Vol. 5", +publisher="Oxford University Press", +year=1994, +} + +@book{Monin2002, +title="Understanding Formal Methods", +author="Jean-FranÁois Monin", +publisher="Springer-Verlag", +year=2002, +} + +@book{ACL2book, +title="Computer-aided reasoning: an approach", +author="Matt Kaufmann and Panagiotis Manolios and J. Strother Moore", +publisher="Kluwer Academic Publishing", +year=2000, +isbn="0-7923-7744-3", +url="http://www.cs.utexas.edu/users/moore/acl2" +} + +@inproceedings{Pons00, +title = "Ing{\'e}ni{\'e}rie de preuve", +author = "Olivier Pons", +booktitle = {\sl Journ{\'e}es Francophones pour les Langages Applicatifs}, +month = jan, +year = 2000, +} + +@InProceedings{automath, + author = {Nicolaas G. de Bruijn}, + title = {The Mathematical Language AUTOMATH, Its Usage and Some of its Extensions}, + booktitle = {Symposium on Automatic Demonstration}, + year = {1970}, + volume= {125}, + series = {Lectur Notes in Mathematics}, + publisher = {Springer-Verlag}, +} + + +@inproceedings{BoveCapretta01, +crossref = "tphols2001", +title = "Nested General Recursion and Partiality in Type Theory", +author = "Ana Bove and Venanzio Capretta", +pages = "121--135" +} + +@inproceedings{capretta01, + crossref = "tphols2001", + author = "Venanzio Capretta", + title = "Certifying the Fast {F}ourier Transform with {C}oq", + pages = "154--168" +} + +@PROCEEDINGS{tphols2001, + editor = "Richard J. Boulton and Paul B. Jackson", + booktitle = "Theorem Proving in Higher Order Logics: + 14th International Conference, TPHOLs 2001", + title = "Theorem Proving in Higher Order Logics: + 14th International Conference, TPHOLs 2001", + series = "Lecture Notes in Computer Science", + volume = 2152, + year = 2001, + publisher = "Springer-Verlag"} + +@PHDTHESIS{Pau96b, + AUTHOR = {Christine Paulin-Mohring}, + TITLE = {DÈfinitions Inductives en ThÈorie des Types d'Ordre SupÈrieur}, + SCHOOL = {UniversitÈ Claude Bernard Lyon I}, + YEAR = 1996, + MONTH = DEC, + TYPE = {Habilitation ‡ diriger les recherches}, + URL = {http://www.lri.fr/~paulin/habilitation.ps.gz} +} + +@inproceedings{courtieu-barthe, + author = {Gilles Barthe and Pierre Courtieu}, + title = {{Efficient reasoning about executable specifications in Coq}}, + booktitle={Proceedings of TPHOLs'02}, + editor={V. CarreÒo and C. MuÒoz and S. Tahar}, + series="Lecture Notes in Computer Science", + year = {2002}, + Publisher="Springer-Verlag", + volume={2410}, + pages={31--46}} + +@PhdThesis{Alvarado02, + author = {Cuihtlauac Alvarado}, + title = {RÈflexion pour la rÈÈcriture dans le calcul des constructions inductives}, + school = {UniversitÈ de Paris XI}, + year = {2002}, + note = {\texttt{http://perso.rd.francetelecom.fr/alvarado/publi/these.ps.gz}}, +} + +@INPROCEEDINGS{Moh93, + author = {Christine Paulin-Mohring}, + booktitle = {Proceedings of the conference Typed Lambda Calculi and + Applications}, + editor = {M. Bezem and J.-F. Groote}, + institution = {LIP-ENS Lyon}, + note = {LIP research report 92-49}, + volume = {664}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag}, + title = {{Inductive definitions in the system {Coq} - rules and + properties}}, + type = {research report}, + year = {1993}, +} + + +@Article{Leroy, + author = {Xavier Leroy}, + title = {A modular module system}, + journal = {Journal of Functional Programming}, + publisher = {Cambridge University Press}, + year = {2000}, + volume = {10}, + number = {3}, +} + + + +@InProceedings{LeroyManifeste, + author = {Xavier Leroy}, + title = {Manifest types, modules, and separate compilation}, + booktitle = {Proceedings of the 21st Symposium on Principles of Programming Languages}, + pages = {109-122}, + year = {1994}, + organization = {ACM}, +} + +@ARTICLE{Church, + author = "Alonzo Church", + journal = "Journal of Symbolic Logic", + pages = "56--68", + title = "A formulation of the simple theory of types", + volume="5(1)", + year = {1940}, +} + +@phdthesis{DelahayePhd, + author = {David Delahaye}, + title = {Conception de langages pour d{\'e}crire les preuves et + les automatisations dans les outils d'aide {\`a} la preuve, + Une {\'e}tude dans le cadre du syst{\`e}me Coq}, + school={Universit{\'e} de {Paris} {VI}, {Pierre} et {Marie} + {Curie}}, + year = 2001 +} + + +@Article{Coquand:Huet, + author = {Thierry Coquand and GÈrard Huet}, + title = {The Calculus of Constructions}, + journal = {Information and Computation}, + year = {1988}, + volume = {76}, +} + +@INPROCEEDINGS{Coquand:girard, + author = "Thierry Coquand", + title = "An Analysis of {G}irard's Paradox", + booktitle="Symposium on Logic in Computer Science", + year = {1986}, + series = "IEEE Computer Society Press", +} + + +@PhdThesis{Girard72, + author = {Jean-Yves Girard}, + title = {InterprÈtation fonctionnelle et Èlimination des coupures de + l'arithmÈtique d'ordre supÈrieur}, + school = {Paris VII}, + year = {1972}, + type = {ThËse d'…tat} +} + +@INcollection{Coquand:metamathematical, + author = "Thierry Coquand", + title = "Metamathematical Investigations on a Calculus of Constructions", + booktitle="Logic and Computer Science", + year = {1990}, + editor="P. Odifreddi", + publisher = "Academic Press", +} +@inproceedings{Pnueli, + title="The Temporal Logic of Programs", + author="Amir Pnueli", + booktitle="Proceedings of the 18th Annual IEEE Symposium on Foundations of Computer Science", + year=1977, +} + +@article{Caprotti_Oostdijk:01pockjsc, + author = {Olga Caprotti and + Martijn Oostdijk}, + title = {Formal and efficient primality proofs + by use of Computer Algebra oracles}, + journal = {Journal of Symbolic Computation}, + publisher = {Academic Press}, + volume = 32, + number = {1/2}, + editor = {T. Recio and M. Kerber}, + pages = {55--70}, + month = jul, + year = 2001 +} + +@inproceedings{PVS, + author = "Sam Owre and Sreeranga P. Rajan and John M. Rushby and Natarajan Shankar and Mandayam K. Srivas", + title="{PVS}: Combining specifications, proof checking and model checking", + editor="Rajeev Alur and Thomas A. Henzinger", + booktitle="{C}omputer {A}ided {V}erification, {CAV}'96", + volume=1102, + series = "Lecture Notes in Computer Science", + pages="411--414", + location="New Brunswick, N. J.", + year = 1996 +} + + +@inproceedings{reasoningexecutable, + title = "Reasoning with executable specifications", + author = "Yves Bertot and Ranan Fraer", + volume = 915, + pages = "531--545", + location = "Aarhus, Denmark", + year = 1995, + series = "Lecture Notes in Computer Science", + journal = "Springer-Verlag LNCS", + booktitle = "Proceedings of the International Joint Conference on Theory + and Practice of Software Development (TAPSOFT'95)" +} + +@TechReport{coupet, + author = "Solange Coupet-Grimal", + title = "{LTL} in {C}oq", + institution = "Contributions to the Coq System", + year = "2002" +} + +@inproceedings{Prawitz, +title="Ideas and results in proof theory", +author="Dag Prawitz", +booktitle= "Proceedings of the second Scandinavian logic symposium", +year = 1971, +publisher = "North-Holland" +} + + +@article{Tarski, + author = "Alfred Tarski", + title = "The semantic conception of truth + and the foundations of semantics", + journal="Philosophy and Phenomenological Research", + volume = 4, + year = 1944, +note="Transcription available at \texttt{www.ditext.com/tarski/tarski.html}", +} + + +@book{Gordon, + author = "Gordon, Michael and Melham, Tony", + title = "Introduction to HOL", + publisher = "Cambridge University Press", + year = 1993, +} +@Article{Paulson89, + author = "Lawrence C. Paulson", + title = "The Foundation of a Generic Theorem Prover", + journal = "Journal of Automated Reasoning", + volume = 5, + number = 3, + pages = "363--397", + year = 1989, + urldvi = "http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz", + keywords = "Isabelle" +} + + +@Book{PaulsonML, + author = {Lawrence C. Paulson}, + title = {ML for the Working Programmer}, + publisher = {Cambridge University Press}, + year = {1996}, +} + +@book{LCFBook, + author = "Gordon, Michael and Milner, Robin and Wadsworth, Christopher", + title = {Edinburgh LCF: A mechanized logic of computation}, + publisher = "Springer-Verlag", + series = {Lecture Notes in Computer Science}, + volume = 78, + year = 1979, +} + + + +@Misc{coqsite, + author= "{D}evelopment team", + title = {The \emph{Coq} proof assistant}, + note = {Documentation, system download. {C}ontact: \texttt{http://coq.inria.fr/}}, +} + + +@Misc{contribs, + author={Various Users}, + title = {Users contributions to the \emph{Coq} system}, + note = {\texttt{http://coq.inria.fr/}}, +} + +@Misc{coqrefman, + title = {The {C}oq reference manual}, + author={Coq Development Team}, + note= {LogiCal Project, \texttt{http://coq.inria.fr/}} + } + + +@incollection{ danvy92back, + author = "Olivier Danvy", + title = "Back to Direct Style", + booktitle = "{ESOP} '92, 4th European Symposium on Programming, Rennes, France, February 1992, Proceedings", + volume = "582", + publisher = "Springer-Verlag", + editor = "Bernd Krieg-Bruckner", + pages = "130-150", + year = "1992", + url = "citeseer.nj.nec.com/danvy94back.html" } + +@Article{Pugh92, + author = "William Pugh", + title = "The Omega Test: a fast and practical integer + programming algorithm for dependence analysis", + journal = "CACM", + year = 1992, + volume = 8, + pages = "102-114", +} + + + +@Book{ocamlbook, + author = {Emmanuel Chailloux and Pascal Manoury and Bruno Pagano}, + title = {DÈveloppement d'applications avec Objective CAML}, + publisher = {O'Reilly}, + year = {2000} + +} + + +@INPROCEEDINGS{field, + author = {Delahaye, David and Mayero, Micaela}, + title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres + r\'eels en {C}oq}, + booktitle = {{J}ourn\'ees {F}rancophones des {L}angages {A}pplicatifs, + Pontarlier}, + publisher = {INRIA}, + month = {Janvier}, + year = {2001}, + note = {\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/Micaela.Mayero/papers/field.ps.gz}}, +} + +@inproceedings{MahboubiPottier2002, + title = "…limination des quantificateurs sur les rÈels en {C}oq", + author = "Assia Mahboubi and LoÔc Pottier", + booktitle = {{J}ourn\'ees {F}rancophones des {L}angages {A}pplicatifs, + Anglet}, + month = {Jan}, + year = {2002} +} + + +@inproceedings{boutin97, +title= "Using reflection to build efficient and certified decision procedures", +author="Samuel Boutin", +booktitle = "Theoretical Aspects of Computer Science", +editors = "T. Ito and M. Abadi", +series = "Lecture Notes in Computer Science", +volume = 1281, +publisher = "Springer-Verlag", +year = 1997 +} + +@Misc{Why, + author = {Jean-Christophe Filli‚tre}, + title = {{L'outil de v\'erification \textsf{Why}}}, + note = {\url{http://why.lri.fr/}} +} + +@Misc{Booksite, + author = {Yves Bertot and Pierre Cast\'eran}, + title = {Coq'{A}rt: examples and exercises}, + note = {\url{http://www.labri.fr/Perso/~casteran/CoqArt}} +} + +@inproceedings{BalaaBertot02, +title = "Fonctions r\'ecursives g\'en\'erales par it\'eration en th\'eorie +des +types", +author = "Antonia Balaa and Yves Bertot", +booktitle = {\sl Journ{\'e}es Francophones pour les Langages Applicatifs}, +month = jan, +year = 2002, +} + +@proceedings{tphols2000, + editor = "J. Harrison and M. Aagaard", + booktitle = "Theorem Proving in Higher Order Logics: + 13th International Conference, TPHOLs 2000", + series = "Lecture Notes in Computer Science", + volume = 1869, + year = 2000, + publisher = "Springer-Verlag"} + +@INPROCEEDINGS{letouzey2002types, + AUTHOR = {Pierre Letouzey}, + TITLE = {A New Extraction for {Coq}}, + TOPICS = {team}, + CROSSREF = {types02} +} + +@PROCEEDINGS{types02, + TITLE = {Types for Proofs and Programs +Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers}, + BOOKTITLE = {TYPES 2002}, + YEAR = 2003, + EDITOR = {Herman Geuvers and Freek Wiedijk}, + VOLUME = 2646, + SERIES = {Lecture Notes in Computer Science}, + PUBLISHER = {Springer-Verlag} +} + +@article{Spitters2011, + Author = {Bas Spitters and Eelis van der Weegen}, + Bibsource = {DBLP, http://dblp.uni-trier.de}, + Date-Added = {2012-05-21 11:58:30 +0200}, + Date-Modified = {2012-05-21 11:58:30 +0200}, + Ee = {http://dx.doi.org/10.1017/S0960129511000119}, + Journal = {Mathematical Structures in Computer Science}, + Number = {4}, + Pages = {795-825}, + Title = {Type classes for mathematics in type theory}, + Volume = {21}, + Year = {2011}} + +@article{math-classes, + author = {Bas Spitters and Eelis van der Weegen}, + title = {Type Classes for Mathematics in Type Theory}, + journal = "{MSCS, special issue on `Interactive theorem proving and +the formalization of mathematics'}", + volume = 21, + pages = {1--31}, + doi = {10.1017/S0960129511000119}, + publisher = {Cambridge University Press}, + year = {2011} +} + + + + + +@Misc{Ahrens, + author = {Benedikt Ahrens}, + title = {Coq library on categories, categorical syntax and semantics}, + howpublished = {http://math.unice.fr/\(\sim\)ahrens/publications/index.html}, +} + +@inproceedings{DBLP:conf/tphol/SozeauO08, + author = {Matthieu Sozeau and + Nicolas Oury}, + title = {First-Class Type Classes}, + booktitle = {TPHOLs}, + year = {2008}, + pages = {278-293}, + ee = {http://dx.doi.org/10.1007/978-3-540-71067-7_23}, + crossref = {DBLP:conf/tphol/2008}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@proceedings{DBLP:conf/tphol/2008, + editor = {Otmane A\"{\i}t Mohamed and + C{\'e}sar Mu{\~n}oz and + Sofi{\`e}ne Tahar}, + title = {Theorem Proving in Higher Order Logics, 21st International + Conference, TPHOLs 2008, Montreal, Canada, August 18-21, + 2008. Proceedings}, + booktitle = {TPHOLs}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {5170}, + year = {2008}, + isbn = {978-3-540-71065-3}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@MISC{Magnusson95theimplementation, + author = {Lena Magnusson}, + title = {The Implementation of ALF - a Proof Editor based on Martin-Lˆf's Monomorphic Type Theory with Explicit Substitution}, + year = {1995} +} + + +@article{DBLP:journals/ita/BrlekCHM95, + author = {Srecko Brlek and + Pierre Cast{\'e}ran and + Laurent Habsieger and + Richard Mallette}, + title = {On-Line Evaluation of Powers Using Euclid's Algorithm}, + journal = {ITA}, + volume = {29}, + number = {5}, + year = {1995}, + pages = {431-450}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + + +@inproceedings{DBLP:conf/tapsoft/BrlekCS91, + author = {Srecko Brlek and + Pierre Cast{\'e}ran and + Robert Strandh}, + title = {On Addition Schemes}, + booktitle = {TAPSOFT, Vol.2}, + year = {1991}, + pages = {379-393}, + ee = {http://dx.doi.org/10.1007/3540539816_77}, + crossref = {DBLP:conf/tapsoft/1991-2}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@proceedings{DBLP:conf/tapsoft/1991-2, + editor = {Samson Abramsky and + T. S. E. Maibaum}, + title = {TAPSOFT'91: Proceedings of the International Joint Conference + on Theory and Practice of Software Development, Brighton, + UK, April 8-12, 1991, Volume 2: Advances in Distributed + Computing (ADC) and Colloquium on Combining Paradigms for + Software Developmemnt (CCPSD)}, + booktitle = {TAPSOFT, Vol.2}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {494}, + year = {1991}, + isbn = {3-540-53981-6}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} diff --git a/doc/typeClassesTut/marginote.sty b/doc/typeClassesTut/marginote.sty new file mode 100644 index 0000000..9fc463b --- /dev/null +++ b/doc/typeClassesTut/marginote.sty @@ -0,0 +1,89 @@ +%%% ====================================================================== +%%% @LaTeX-style-file{ +%%% filename = "marginote.sty", +%%% version = "2.0", +%%% date = "1 July 1993", +%%% time = "09:07:08 CDT", +%%% author = "George D. Greenwade", +%%% address = "Department of Economics and Business Analysis +%%% College of Business Administration +%%% P. O. Box 2118 +%%% Sam Houston State University +%%% Huntsville, Texas, USA 77341-2118", +%%% email = "bed_gdg@SHSU.edu (Internet) +%%% BED_GDG@SHSU (BITNET) +%%% SHSU::BED_GDG (THENET)", +%%% telephone = "(409) 294-1266", +%%% FAX = "(409) 294-3712", +%%% supported = "yes", +%%% archived = "SHSU*", +%%% keywords = "LaTeX, marginal notes", +%%% codetable = "ISO/ASCII", +%%% abstract = "Create command \marginote{text} to use marginal +%%% notes in a document. Each marginal note is +%%% denoted by the fnsymbol sequence and does not +%%% alter any know counters other than those created. +%%% Original version September 12, 1989.", +%%% modifications = "Modified 1 July 1993 in response to report from +%%% Bradley C. Kuszmaul +%%% via David M. Jones +%%% that a `gratuitous space' was introduced in the +%%% \stepcounter{marginalnote} (dumb mistake on my +%%% part!). Also added this file header and added +%%% \endinput at the end of the file.", +%%% checksum = "11442 75 385 3712", +%%% docstring = "The checksum field above contains a CRC-16 +%%% checksum as the first value, followed by the +%%% equivalent of the standard UNIX wc (word +%%% count) utility output of lines, words, and +%%% characters. This is produced by Robert +%%% Solovay's checksum utility." +%%% } +%%% ====================================================================== +\typeout{LaTeX document substyle 'marginote.sty' July 1, 1993 (GDG)} + +\DeclareOption{nonote}{ % pierre option pour ne pas afficher les notes +\typeout{Option 'nonote'} +\newcommand{\marginote}[1]{} +} + +\DeclareOption{note}{ % pierre: option pour afficher les notes +\typeout{Option 'marginote'} +\topmargin 0pt %% this code from FULLPAGE.STY +\advance \topmargin by -\headheight %% +\advance \topmargin by -\headsep %% + +%\textheight 8.9in %% + +%%\oddsidemargin 0pt %% +%%\evensidemargin \oddsidemargin %% +%%\oddsidemargin 15pt +\evensidemargin 10pt %% Pierre +\marginparwidth .9in %% changed (+.6in) to allow for notes + +%%\textwidth 5.9in %% changed (-.6in) to allow for notes +%\textwidth 15.5cm %% Pierre +% %% end of FULLPAGE.STY + +\newcounter{marginalnote} +\def\themarginalnote{\fnsymbol{marginalnote}} +\newcount\marginalnotecounter +\marginalnotecounter=0 + +\def\marginote#1{\ifmmode %% Can't use \marginpar in math mode, thus ... +\typeout{ } +\typeout{\string \marginote \space error. Cannot use \string \marginote \space +in math mode. Ignoring text.} +\typeout{ } +\else \ifnum \marginalnotecounter=9 \setcounter{marginalnote}{0} +\marginalnotecounter= 0 \fi %% fnsymbol only goes to 9 +\stepcounter{marginalnote}% -- line split -- GDG 1-JUL-1993 +\global\advance\marginalnotecounter 1 %patch Pierre bug sinon +{$^{\themarginalnote}\!\!$\marginpar{\raggedright + %pierre:\!\!%pour moins d'espace aprs le signe + +\footnotesize $\themarginalnote~$ #1}} %% better in such a small space +\fi} +} +\ProcessOptions +\endinput % -- added -- GDG 1-JUL-1993 \ No newline at end of file diff --git a/doc/typeClassesTut/morebiblio.bib b/doc/typeClassesTut/morebiblio.bib new file mode 100644 index 0000000..46c242f --- /dev/null +++ b/doc/typeClassesTut/morebiblio.bib @@ -0,0 +1,395 @@ + + + + + + + + + + + +@Misc{Vis06, +TITLE = {The {V}isidia project}, +howpublished = {http://www.labri.fr/visidia}, +AUTHOR = {LaBRI Distributed Algorithms Group}, +} + + +@Misc{LocoPage, +AUTHOR = {P. Cast\'eran and V. Filou}, +TITLE = {Loco: A {C}oq {L}ibrary on {L}ocal {C}omputation {S}ystems}, +howpublished = {http://www.labri.fr/$\sim$casteran/Loco}, +} + + + +@Book{coqart, + author = "Bertot, Y. and Cast\'eran, P.", + title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions", + series = "Texts in Theoretical Computer Science", + year = "2004", + publisher = "Springer Verlag", + url = "http://www.labri.fr/publications/l3a/2004/BC04" +} + + +@inproceedings{filliatre07cav, + author = {J.C. Filli\^atre and C. March\'e}, + title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program + Verification}, + topics = {team, lri}, + year=2007, + url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf} +} + + +@Manual{Coq, + title = {The Coq Proof Assistant Reference Manual}, + year = 2012, + author = {{Coq Development Team}}, + address = {coq.inria.fr}, +} + +@InBook{EventB, + author = {D. Cansell and D. M\'ery}, + ALTeditor = {Dines Bjorner and Martin Henson}, + title = {Logics of Specification Languages}, + chapter = {The Event-B Modelling Method: Concepts and Case Studies}, + publisher = {Springer Verlag}, + year = {2007}, + pages = {47-152} + +} + + + + +@Unpublished{Spanning-Cansell, + author = {D. Cansell}, + title = {A development in {Event-B} of a distributed algorithm for building a spanning tree }, + note = {Personnal communication}, + OPTkey = {}, + OPTmonth = {}, + OPTyear = {}, + OPTannote = {} +} + +@Manual{Rodin, + organization = {Deploy European Community Project}, + title = {Event-B and the Rodin Platform}, + address = {www.event-b.org}, +} + + + + +@Article{Chou95, + author = {Chin-Tsun Chou}, + title = {Mechanical Verification of Distributed Algorithms in Higher-Order Logic}, + journal = {The Computer Journal}, + year = {1995}, + volume = {38}, + number = {2}, +pages={152-161} +} + + +@InProceedings{Thirioux97, +Author = {X. Thirioux and G. Padiou}, +Title = {Etude Comparative de deux techniques de preuves de programmes UNITY}, +BookTitle = {AFADL'97}, +Year = 1997 +} + + +@Article{urbain04jar, + author = {X. Urbain}, + title = {Modular and Incremental Automated Termination Proofs}, + journal = "Journal of Automated reasoning", + year = {2004}, + volume = 32, + pages = {315--355}, + topics = {team}, + type_publi = "irevcomlec", + url = {http://www.lri.fr/~urbain/textes/jar.ps.gz} +} + + + +@Article{mecaterm, + author = {Evelyne Cont\'ejean and Claude March\'e and +Ana Paula Tom\'as and Xavier Urbain}, + title = {Mechanically proving termination using polynomial interpretations}, + journal = {Journal of Automated Reasoning}, + year = {2005}, + volume = {34}, + number = {4}, + pages = {325--363} +} + + + +@@TechReport{CFM09, +title={{F}ormal {P}roofs of {L}ocal {C}omputati 1 + | S p => x * power x p + end. + +Compute power 2 40.\it\color{answercolor} + = 1099511627776 + : Z +\end{alltt} + +This definition can be considered as a very na\"{\i}ve way of programming, +since computing $x^n$ requires $n$ multiplications. + Nevertheless, this definition is +very simple to read, and everyone can admit that it is correct +with respect to the mathematical definition of raising $x$ to the $n$-th power. +Thus, we can consider it as a \emph{specification}: when we write +more efficient but less readable functions for exponentiation, +% \cite{DBLP:journals/ita/BrlekCHM95}, + we should be able +to prove their correctness by proving in \coq{} their equivalence\footnote{\emph{i.e.} extensional equality} +with the na\"{\i}ve \texttt{power} function. + +For instance the following function allows one to compute $x^n$, +with a number of multiplications proportional to $\textrm{log}_2(n)$: + + + \begin{alltt} +{Function} binary_power_mult (acc x:Z){(n:nat)} + \{measure (fun i=>i) n\} : Z +{(* acc * (power x n) *)} := + match {{n}} with 0\%nat => acc + | _ => if Even.even_odd_dec n + then binary_power_mult + acc (x * x) {(div2 n)} + else binary_power_mult + (acc * x) (x * x) {(div2 n)} + end.{ +Proof. + intros;apply lt_div2; auto with arith. + intros;apply lt_div2; auto with arith.} +Defined. + +Definition binary_power (x:Z)(n:nat) := + binary_power_mult 1 x n. + +Compute binary_power 2 40.\color{answercolor}\it +1099511627776: Z +\end{alltt} + +We want now to \emph{prove} \texttt{binary\_power}'s correctness, \emph{i.-e.} +that this function and the naive \texttt{power} function are pointwise +equivalent. + +Proving this equivalence in {\coq} may require a lot of work. +Thus it is not worth at all writing a proof dedicated only to powers of +integers. In fact, the correctness of \texttt{binary\_power} with respect to +\texttt{power} holds in any structure composed of an associative binary +operation on some†domain, that admits a neutral element. +For instance, we can compute powers of square matrices using the most efficient of both algorithms. + + +Thus, let us throw away our previous definition, and try do define them +in a more generic framework. + +\begin{alltt} +Reset power. +\end{alltt} + + +\section{On Monoids}\label{on-monoids} + +\begin{definition} +A \emph{monoid} is a mathematical structure composed of: +\begin{itemize} +\item A carrier $A$ +\item A binary, associative operation $\circ$ on $A$ +\item A neutral element $1\in A$ for $\circ$ +\end{itemize} +\end{definition} + +Such a mathematical structure can be defined in {\coq} as +a \emph{type class}~\citep{DBLP:conf/tphol/SozeauO08, math-classes, DBLP:journals/corr/abs-1106-3448}. In the following definition, parameterized by +a type $A$ (implicit), a binary operation \texttt{dot} and a neutral element +\texttt{unit}, three fields describe the properties that \texttt{dot} and +\texttt{unit} must satisfy. + + +\begin{alltt} +Class Monoid \{A:Type\}(dot : A -> A -> A)(one : A) : Prop := \{ + dot_assoc : forall x y z:A, + dot x (dot y z) = dot (dot x y) z; + unit_left : forall x, dot one x = x; + unit_right : forall x, dot x one = x \}. +\end{alltt} + + +Note that other definitions could have been given for representing this mathematical structure. See Sect~\ref{alternate} for more details. + + +From an implementational point of view, such a type class is just a record type, +\emph{i.e.} an inductive type with a single constructor \texttt{Build\_Monoid}. + +\begin{alltt} +Print Monoid.\it\color{red} + +Record Monoid (A : Type) (dot : A -> A -> A) (one : A) : Prop := Build_Monoid + \{ dot_assoc : forall x y z : A, dot x (dot y z) = dot (dot x y) z; + one_left : forall x : A, dot one x = x; + one_right : forall x : A, dot x one = x \} + +For Monoid: Argument A is implicit and maximally inserted +For Build_Monoid: Argument A is implicit +For Monoid: Argument scopes are [type_scope _ _] +For Build_Monoid: Argument scopes are [type_scope _ _ _ _ _] +\end{alltt} +\label{ClassVsRecords} +Nevertheless, the implementation of type classes by M. Sozeau provides several specific tools +---dedicated tactics for instance ---, and we advise the reader not to replace +the \texttt{Class} keyword with \texttt{Record} or \texttt{Inductive}. + + +With the command \texttt{About}, we can see the polymorphic type of +the fields of the class \texttt{Monoid}: + +\begin{alltt} +About one_left.\it\color{red} +one_left : +forall (A : Type) (dot : A -> A -> A) (one : A), +Monoid dot one -> forall x : A, dot one x = x + +Arguments A, dot, one, Monoid are implicit and maximally inserted +Argument scopes are [type_scope _ _ _ _] +one_left is transparent +\end{alltt} + +\subsection{Classes and Instances} +Members of a given class are called \emph{instances} of this class. +Instances are defined to the {\coq} system through the \texttt{Instance} keyword. Our first example is a definition of the monoid structure on the set +$\mathbb{Z}$ of integers, provided with integer multiplication, with $1$ as +a neutral element. Thus we give these parameters to the \texttt{Monoid} class +(note that \texttt{Z} is implicitely given). + +\begin{alltt} +Instance ZMult : Monoid Zmult 1. +\end{alltt} + +For this instance to be created, we need to prove that the binary operation +\texttt{Zmult} is associative and admits $1$†as neutral element. +Applying the constructor \texttt{Build\_Monoid} --- for instance with the tactic \texttt{split} --- generates three subgoals. + + +\begin{alltt} +split.\it\color{answercolor} +3 subgoals + ============================ + forall x y z : Z, x * (y * z) = x * y * z + +subgoal 2 is: + forall x : Z, 1 * x = x +subgoal 3 is: + forall x : Z, x * 1 = x\tt\color{black} +\end{alltt} + + Each subgoal is easily solved by \textcolor{taccolor}{intros; ring}. + +When the proof is finished, we register our instance with a simple \texttt{Qed}. +Note that we used \texttt{Qed} because we consider a class of sort \texttt{Prop}. In some cases where instances must store some informative constants, ending +an instance construction with \texttt{Defined} may be necessary. + +%We can look at the type of \texttt{ZMult}: + +\begin{alltt} +Check Zmult.\it\color{red} +ZMult : Monoid Zmult 1 +\end{alltt} + + We explained \vpageref{ClassVsRecords} why it is better to use +the \texttt{Class} keyword than \texttt{Record} or \texttt{Inductive}. +For the same reason, the definition of an instance of some class should +be written using \texttt{Instance} and not \texttt{Lemma}, \texttt{Theorem}, +\texttt{Example}, etc., nor \texttt{Definition}. + +\subsection{A generic definition of \texttt{power}} + +We are now able to give a definition of the function \texttt{power} that +can be applied with any instance of class \texttt{Monoid}: + +A first definition could be: + +\begin{alltt} +Fixpoint power \{A:Type\}\{dot:A->A->A\}\{one:A\}\{M: Monoid dot one\} + (a:A)(n:nat) := + match n with 0%nat => one + | S p => dot a (power a p) + end. + +Compute power 2 10.\it\color{red} += 1024 : Z +\end{alltt} + +Happily, we can make the declaration of the three first arguments implicit, by using the +\texttt{Generalizable Variables} command: + +\begin{alltt} +Reset power. + +Generalizable Variables A dot one. + +Fixpoint power `\{M: Monoid A dot one\}(a:A)(n:nat) := + match n with 0%nat => one + | S p => dot a (power a p) + end. + +Compute power 2 10.\it\color{red} += 1024 : Z +\end{alltt} + +The variables \texttt{A dot one} appearing in the binder for \texttt{M} +are implicitly bound before the binder for \texttt{M} and their types +are infered from the \texttt{Monoid A dot one} type. This syntactic sugar +helps abbreviate bindings for classes with parameters. The resulting +internal {\coq} term is exactly the same as the first definition above. + +\subsection{Instance Resolution} + +The attentive reader has certainly noticed that in the last computation, the +the binary operation \texttt{Zmult} and the neutral element $1$ need not to be +given explicitely\footnote{This is quite different from the basic implicit arguments mechanism, already able to infer the type \texttt{Z} from the type of $2$.}. +The mechanism that allows {\coq} to infer all the arguments needed by the \texttt{power} function to be applied is called \emph{instance resolution}. + + + +In order to understand how it operates, let's have a look at \texttt{power}'s type: + \begin{alltt} +About power.\it\color{answercolor} +power : +forall (A : Type) (dot : A -> A -> A) (one : A), +Monoid dot one -> A -> nat -> A + +Arguments A, dot, one, M are implicit and maximally inserted +\tt\color{black} +Compute power 2 100.\it\color{answercolor} + = 1267650600228229401496703205376 : Z\tt\color{black} + +Set Printing Implicit. +Check power 2 100.\it\color{answercolor} +@power Z Zmult 1 {\color{blue}ZMult} 2 100 : Z \tt\color{black} +Unset Printing Implicit. +\end{alltt} + +We see that the \emph{instance} \texttt{ZMult} has been +inferred from the type of $2$. We are in the simple case where only one monoid +of carrier \texttt{Z} has been declared as an instance of the \texttt{Monoid} class. + +The implementation of type classes in {\coq} can retrieve the instance \texttt{ZMult} +from the type \texttt{Z}, then filling the arguments \texttt{Zmult} and $1$ from +\texttt{ZMult}'s definition. + + + +\subsection{More Monoids} +\subsubsection{Matrices over some ring}\label{matring} +We all know that multiplication of square matrices is associative and admits +identity matrices as neutral elements. For simplicity's sake let us restrict our study +to $2 \times 2$ matrices over some ring. + +We first load the \texttt{Ring} library, the open a section with some useful declarations and notations. The reader may consult \coq's documentation about the \texttt{Ring} library. + +\begin{alltt} +Require Import Ring. + +Section matrices. + Variables (A:Type) + (zero one : A) + (plus mult minus : A -> A -> A) + (sym : A -> A). + Notation "0" := zero. Notation "1" := one. + Notation "x + y" := (plus x y). + Notation "x * y " := (mult x y). + + Variable rt : ring_theory zero one plus mult minus sym (@eq A). + + Add Ring Aring : rt. +\end{alltt} + + +We can now define a carrier type for $2\times 2$-matrices, as well as matrix multiplication and the identity matrix: + +\begin{alltt} +Structure M2 : Type := \{c00 : A; c01 : A; + c10 : A; c11 : A\}. + +Definition Id2 : M2 := Build_M2 1 0 0 1. + +Definition M2_mult (m m':M2) : M2 := + Build_M2 (c00 m * c00 m' + c01 m * c10 m') + (c00 m * c01 m' + c01 m * c11 m') + (c10 m * c00 m' + c11 m * c10 m') + (c10 m * c01 m' + c11 m * c11 m'). +\end{alltt} + +As for multiplication of integers, we can now define an instance of +\texttt{Monoid} for the type \texttt{M2}. + +\begin{alltt} +Global Instance M2_Monoid : Monoid M2_mult Id2. \it\color{red} +(* Proof skipped *) \tt\color{black} +Qed. + +End matrices. +\end{alltt} + + +We want now to play with $2\times 2$ matrices over $\mathbb{Z}$. +We declare an instance \texttt{M2Z} for this purpose, and can use directly +the function \texttt{power}. + +\begin{alltt} +Instance M2Z : Monoid _ _ := M2_Monoid Zth. + +Compute power (Build_M2 1 1 1 0) 40.\it\color{red} + = \{| + c00 := 165580141; + c01 := 102334155; + c10 := 102334155; + c11 := 63245986 |\} + : M2 Z\tt\color{black} + +Definition fibonacci (n:nat) := + c00 (power (Build_M2 1 1 1 0) n). + +Compute fibonacci 20.\it\color{red} += 10946 + :Z +\end{alltt} + + +\section{Reasoning within a Type Class} + +We are now able to consider again the equivalence between two functions for computing +powers. +Let us define the binary algorithm for any monoid: + +First, we define an auxiliary function. We use the \texttt{Program} +extension to define an efficient version of exponentiation using an +accumulator. The function is defined by well-founded recursion on the +exponent \texttt{n}: + +% \begin{alltt} +% Program +% Fixpoint binary_power_mult (A:Type) (dot:A->A->A) (one:A) +% (M: @Monoid A dot one) +% (acc x:A)(n:nat){measure n} : A +% (* acc * (x ** n) *) := +% match n with 0%nat => acc +% | _ => +% if Even.even_odd_dec n +% then binary_power_mult _ acc (dot x x) (div2 n) +% else binary_power_mult _ (dot acc x) (dot x x) (div2 n) +% end. + + +% Solve Obligations using program_simpl; intros; apply lt_div2; auto with arith. +% \end{alltt} +\begin{alltt} +Function binary_power_mult (A:Type) (dot:A->A->A) (one:A) (M: @Monoid A dot one) + (acc x:A)(n:nat)\{measure (fun i=>i) n\} : A + (* acc * (x ** n) *) := + match n with + | 0\%nat => acc + | _ => if Even.even_odd_dec n + then binary_power_mult _ acc (dot x x) (div2 n) + else binary_power_mult _ (dot acc x) (dot x x) (div2 n) + end. +intros;apply lt_div2; auto with arith. +intros; apply lt_div2; auto with arith. +Defined. + +Definition binary_power `\{M:Monoid\} x n := binary_power_mult M one x n. + +Compute binary_power 2 100.\it\color{red} += 1267650600228229401496703205376 + : Z +\end{alltt} + +\subsection{The Equivalence Proof}\label{equiv-proof} + +The proof of equivalence between \texttt{power} and \texttt{binary\_power} is quite +long, and can be split in several lemmas. +Thus, it is useful to open a section, in which we fix some arbitrary monoid $M$. +Such a declaration is made with the \texttt{Context} command, which can be considered +as a version of \texttt{Variables} for declaring arbitrary instances of a given class. + +\begin{alltt} +Section About_power. + +Require Import Arith. + Context `\{M:Monoid A dot one\}. +\end{alltt} + +It is a good practice to define locally some specialized notations and tactics. + +\begin{alltt} + Ltac monoid_rw := + rewrite (@one_left A dot one M) || + rewrite (@one_right A dot one M)|| + rewrite (@dot_assoc A dot one M). + + Ltac monoid_simpl := repeat monoid_rw. + + Local Infix "*" := dot. + Local Infix "**" := power (at level 30, no associativity). +\end{alltt} + +\subsection{Some Useful Lemmas About power} + +We start by proving some well-known equalities about powers in a monoid. +Some of these equalities are integrated later in simplification tactics. + +\begin{alltt} + Lemma power_x_plus : forall x n p, x ** (n + p) = x ** n * x ** p. + Proof. + induction n as [| p IHp];simpl. + intros; monoid_simpl;trivial. + intro q;rewrite (IHp q); monoid_simpl;trivial. + Qed. + + Ltac power_simpl := repeat (monoid_rw || rewrite <- power_x_plus). + + Lemma power_commute : forall x n p, + x ** n * x ** p = x ** p * x ** n. + {\it\color{red}(* Proof skipped *)} + + Lemma power_commute_with_x : forall x n , + x * x ** n = x ** n * x. + {\it\color{red} (* Proof skipped *)} + + Lemma power_of_power : forall x n p, (x ** n) ** p = x ** (p * n). + {\it\color{red} (* Proof skipped *) } + + Lemma power_S : forall x n, x * x ** n = x ** S n. + {\it\color{red} (* Proof skipped *)} + + Lemma sqr : forall x, x ** 2 = x * x. + {\it\color{red} (* Proof skipped *)} + + Ltac factorize := repeat ( + rewrite <- power_commute_with_x || + rewrite <- power_x_plus || + rewrite <- sqr || + rewrite power_S || + rewrite power_of_power). + + Lemma power_of_square : forall x n, (x * x) ** n = x ** n * x ** n. + {\it\color{red}(* Proof skipped *)} +\end{alltt} + +\subsection{Final Steps} +We are now able to prove that the auxiliary function \texttt{binary\_power\_mult} +satiisfies its intuitive meaning. The proof --- partly skipped --- uses well-founded induction and the lemmas proven in the previous section: + +\begin{alltt} + Lemma binary_power_mult_ok : + forall n a x, binary_power_mult M a x n = a * x ** n. + Proof. + intro n; pattern n; apply lt_wf_ind. + {\it\color{red}(* Proof skipped *)} +\end{alltt} + +Then the main theorem follows immediately: + +\begin{alltt} + Lemma binary_power_ok : forall (x:A)(n:nat), binary_power x n = x ** n. + Proof. + intros n x;unfold binary_power;rewrite binary_power_mult_ok; + monoid_simpl;auto. + Qed. +\end{alltt} + + + +\subsection{Discharging the Context} + +It is time to close the section we opened for writing our proof of equivalence. +The theorem \texttt{binary\_power\_ok} is now provided with an universal +quantification over all the parameters of any monoid. + +\begin{alltt} +End About_power. + +About binary_power_ok.\it\color{red} +binary_power_ok : +forall (A : Type) (dot : A -> A -> A) (one : A) (M : Monoid dot one) + (x : A) (n : nat), binary_power x n = power x n + +Arguments A, dot, one, M are implicit and maximally inserted +Argument scopes are [type_scope _ _ _ _ nat_scope] +binary_power_ok is opaque +Expands to: Constant Top.binary_power_ok\tt\color{black} + +Check binary_power_ok 2 20.\it\color{red} +binary_power_ok 2 20 + : binary_power 2 20 = power 2 20\tt\color{black} + +Let Mfib := Build_M2 1 1 1 0. + +Check binary_power_ok Mfib 56.\it\color{red} + + binary_power_ok Mfib 56 + : binary_power Mfib 56 = power Mfib 56 + +\end{alltt} + + +\subsection{Subclasses} +We could prove many useful equalities in the section \texttt{about\_power}. +Nevertheless, we couldn't prove the equality $(xy)^n = x^n\,y^n$, because it is false +in general --- consider for instance the free monoid of strings, or simply +matrix multiplication. Nevertheless, this equality holds in every commutative +(a.k.a. \emph{abelian}) monoid. + +Thus we say that abelian monoids form a \emph{subclass} of the class +of monoids, and prove this equality in a context declaring an arbitrary +instance of this subclass. + +Structurally, we parameterize the new class \texttt{Abelian\_Monoid} +by an arbitrary instance $M$ of \texttt{Monoid}, and add a new field +stating the commutativity of \texttt{dot}. Please keep in mind that +we declared \texttt{A}, \texttt{dot} and \texttt{one} as +\emph{generalizable variables}, hence we can use the backquote symbol here: + +\begin{alltt} +Class Abelian_Monoid `(M:Monoid A dot one) := \{ + dot_comm : forall x y, dot x y = dot y x\}. +\end{alltt} + +A quick look at the representation of \emph{Abelian\_Monoid} as a record type +helps us understand how this class is implemented. + + \begin{alltt} +Print Abelian_Monoid.\it\color{red} +Record Abelian_Monoid (A : Type) (dot : A -> A -> A) +(one : A) (M : Monoid dot one) : Prop := Build_Abelian_Monoid + \{ dot_comm : forall x y : A, dot x y = dot y x \} + +For Abelian_Monoid: Arguments A, dot, one are implicit and maximally inserted +For Build_Abelian_Monoid: Arguments A, dot, one are implicit +For Abelian_Monoid: Argument scopes are [type_scope _ _ _] +For Build_Abelian_Monoid: Argument scopes are [type_scope _ _ _ _] +\end{alltt} + + +For building an instance of \texttt{Abelian\_Monoid}, we can start +from \texttt{ZMult}, the monoid on \texttt{Z}, adding a proof that +integer multiplication is commutative. + +\begin{alltt} +Instance ZMult_Abelian : Abelian_Monoid ZMult. +Proof. + split. + exact Zmult_comm. +Defined. +\end{alltt} + +We can now prove our equality by building an appropriate context. +Note that we can specify just the parameters of the monoid here in the +binder of the abelian monoid, an instance of monoid on those same +parameters is automatically generalized. Superclass parameters are +automatically generalized inside quoted binders. Again, this is simply +syntactic sugar. + +\begin{alltt} +Section Power_of_dot. + Context `\{AM:Abelian_Monoid A dot one\}. + + Theorem power_of_mult : forall n x y, + power (dot x y) n = dot (power x n) (power y n). + Proof. + induction n;simpl. + rewrite one_left;auto. + intros; rewrite IHn; repeat rewrite dot_assoc. + rewrite <- (dot_assoc x y (power x n)); rewrite (dot_comm y (power x n)). + repeat rewrite dot_assoc;trivial. + Qed. + +End Power_of_dot. + +Check power_of_mult 3 4 5.\it\color{red} +power_of_mult 3 4 5 + : power (4 * 5) 3 = power 4 3 * power 5 3 +\end{alltt} + +\chapter{Relations and rewriting} + +\section{Introduction: Lost in Manhattan} + +Assume you are lost in Manhattan, or in any city with the same geometry: +square blocks, square blocks, and so on. + +You ask some by-passer how to go to some other place, and you probably will get +an answer like that: +\begin{quote} +``go two blocks northward, then one block eastward, then three +blocks southward, and finally two blocks westward''. +\end{quote} + + +You thank this kind person, and you go one block southward, then one block +westward. + +If we represent such routes by lists of directions, you will consider +that the two considered routes +\begin{itemize} +\item \texttt{North::North::East::South::South::South::West::West::nil} +\item \texttt{South::West::nil} +\end{itemize} + +are not \emph{equal} --- because the former route is much longer than the other one ---, but \emph{equivalent}, which means that they both +lead to the same point. + +Then you notice that the route \texttt{West::North::East::South::nil} +is equivalent to \texttt{nil} (which means ``don't move!''). + +From both previous equivalences you want to infer simply that the long +route +\begin{alltt} +(North::North::East::South::South::South::West::West::nil)++ +(West::North::East::South::nil) +\end{alltt} + is equivalent to \texttt{South::West::nil}. + + +Moreover, you can consider this equivalence as a \emph{congruence} w.r.t. +route concatenation. For instance, one can easily show that the above +routes are equivalent using a lemma stating that if +the route \texttt{r} is equivalent to \texttt{r'}, and \texttt{s} is +equivalent to \texttt{s'} then \texttt{r++s} is equivalent to +\texttt{r'++s'}. We will say that list concatenation is +a \emph{proper} function with respect to the equivalence between routes. + +The {\coq} system provides now some useful tools for considering relations +and proper functions, allowing to use the \texttt{rewrite} tactics for +relations that are weaker than the Leibniz equality. Examples of such relations +include route-equivalence, non-canonical representation of finite sets, +partial commutation monoids, etc. + +Let us now start with our example. + +\section{Data Types and Definitions} + +We first load some useful modules, for representing directions, routes, and +the discrete plane on which routers operate: + + +\begin{alltt} +Require Import List ZArith Bool. +Open Scope Z_scope. + +Inductive direction : Type := North | East | South | West. + +Definition route := list direction. + +Record Point : Type := + \{Point_x : Z; Point_y : Z\}. + +Definition Point_O := Build_Point 0 0. +\end{alltt} + +\section{Route Semantics} +A route is just a ``program'' for moving from some point to another one. +The function \texttt{move} associates to any route a function from \texttt{Point} to \texttt{Point}. + +\begin{alltt} +Definition translate (dx dy:Z) (P : Point) := + Build_Point (Point_x P + dx) (Point_y P + dy). + +Fixpoint move (r:route) (P:Point) : Point := + match r with + | nil => P + | North :: r' => move r' (translate 0 1 P) + | East :: r' => move r' (translate 1 0 P) + | South :: r' => move r' (translate 0 (-1) P) + | West :: r' => move r' (translate (-1) 0 P) + end. + +Definition Point_eqb (P P':Point) := + Zeq_bool (Point_x P) (Point_x P') \&\& + Zeq_bool (Point_y P) (Point_y P'). + +Lemma Point_eqb_correct : forall p p', Point_eqb p p' = true <-> + p = p'. +\it Proof skipped.\tt +Qed. +\end{alltt} + +We consider that two routes are "equivalent" if they define +the same moves. For instance, the routes +\texttt{East::North::West::South::East::nil} and \texttt{East::nil} +are equivalent. + +\begin{alltt} +Definition route_equiv : relation route := + fun r r' => forall P, move r P = move r' P. +Infix "=r=" := route_equiv (at level 70):type_scope. + +Example Ex1 : East::North::West::South::East::nil =r= East::nil. +Proof. + intro P;destruct P;simpl. + unfold route_equiv,translate;simpl;f_equal;ring. +Qed. +\end{alltt} + +\section{On Route Equivalence} + +It is easy to study some abstract properties of the relation \texttt{route\_equiv}. First, we prove that this relation is reflexive, symmetric and transitive: + +\begin{alltt} +Lemma route_equiv_refl : Reflexive route_equiv. +Proof. + intros r p;reflexivity. +Qed. + +Lemma route_equiv_sym : Symmetric route_equiv. +Proof. + intros r r' H p; symmetry;apply H. +Qed. + +Lemma route_equiv_trans : Transitive route_equiv. +Proof. + intros r r' r'' H H' p; rewrite H; apply H'. +Qed. +\end{alltt} + +Note that, despite these properties, the tactics \texttt{reflexivity}, +\texttt{symmetry}, and \texttt{transitivity} are not directly usable +on the type \texttt{route}. + +\begin{alltt} +Goal forall r, route_equiv r r. +intro; reflexivity.\it\color{red} +Toplevel input, characters 40-51: +Error: Tactic failure: The relation route_equiv is not a + declared reflexive relation. + Maybe you need to require the Setoid library. +\end{alltt} + +The last error message comes from the fact that the tactic +\texttt{reflexivity} consults a base of registered instance of a class +named \texttt{Reflexive}. There exists also classes named \texttt{Symmetric}, +\texttt{Transitive}, and \texttt{Equivalence}. +This last class gathers the properties of reflexivity, symmetry and transitivity. +Thus, we can register an instance of the \texttt{Equivalence} class (and +not as a lemma as above). + +\begin{alltt} +Instance route_equiv_Equiv : Equivalence route_equiv. +Proof. split; + [apply route_equiv_refl | + apply route_equiv_sym | + apply route_equiv_trans]. +Qed. +\end{alltt} + +The tactics \texttt{reflexivity}, etc. can now be applied to the +relation \texttt{route\_equiv}. + +\begin{alltt} +Goal forall r, r =r= r. +Proof. intro; reflexivity. Qed. +\end{alltt} + +Note that it is possible to consider relations that are not equivalence +relations, but are only transitive, or reflexive and transitive, etc. by +using the right type classes. + +\section{Proper Functions} + +Since routes are represented as lists of directions, we wish to prove +some route equivalences by composition of already proven equivalences, +using some lemmas on consing and appending routes. + +For instance, we can prove that if we add the same direction in front of +two equivalent routes, the routes we obtain are still equivalent: + +\begin{alltt} +Lemma route_cons : forall r r' d, r =r= r' -> d::r =r= d::r'. +Proof. + intros r r' d H P;destruct d;simpl;rewrite H;reflexivity. +Qed. +\end{alltt} + +This lemma can be applied to re-use our previous example \texttt{Ex1}. + +\begin{alltt} +Goal (South::East::North::West::South::East::nil) =r= (South::East::nil). +Proof. apply route_cons;apply Ex1. Qed. +\end{alltt} + +Note that the proof of \texttt{route\_cons} contains a case analysis on $d$. Let us try to have a more +direct proof: + +\begin{alltt} +Lemma route_cons' : forall r r' d, r =r= r' -> d::r =r= d::r'. +Proof. + intros r r' d H;rewrite H.\it\color{red} + +Toplevel input, characters 80-89: +Error: Found no subterm matching "move r ?17869" in the current goal. \tt\color{black} +Abort. +\end{alltt} + +What we really need is to tell to the \texttt{rewrite} tactic how to +use \texttt{route\_cons} for using an equivalence \texttt{$r$ =r= $r'$} +for replacing $r$ with $r'$ in a term of the form \texttt{cons $d$ $r$} +for proving directly the equivalence \texttt{cons $d$ $r$ =r= cons $d$ $r'$}. +In other words, we say that \texttt{cons $d$} is \emph{proper} w.-r.-t. +the relation \texttt{route\_equiv}. + +In {\coq} this fact can be declared as an instance of: +\begin{alltt} + Proper (route\_equiv ==> route\_equiv) (cons d) +\end{alltt} + +This notation, which requires the library \texttt{Morphisms} to be loaded, +expresses that if two routes $r$ and $r'$ are related through +\texttt{route\_equiv}, then the routes \texttt{$d$::r} and \texttt{$d$::r'} +are also related by \texttt{route\_equiv}. + +In the notation used by \texttt{Proper} the first occurrence of +\texttt{route\_equiv} refers to the arguments of \texttt{cons $d$}, and the second one +to the result of this consing. The user must require and import +the \texttt{Morphisms} module to use this notation. +\begin{alltt} +Require Import Morphisms. + +Instance cons_route_Proper (d:direction) : + Proper (route_equiv ==> route_equiv) (cons d). +Proof. + intros r r' H ;apply route_cons;assumption. +Qed. +\end{alltt} + +We can now use \texttt{rewrite} to replace some +term by an equivalent one, provided the context is made by applications of +one or several functions of the form \texttt{cons $d$}: + +\begin{alltt} +Goal forall r r', r =r= r' -> South::West::r =r= South::West::r'. +Proof. + intros r r' H. \it\color{red} + +1 subgoal + + r : route + r' : route + H : r =r= r' + ============================ + South :: West :: r =r= South :: West :: r' +\end{alltt} + +Since the context of the +variable \texttt{r} is composed of applications of proper function + calls, the tactic \texttt{rewrite H} can be used to replace the occurrence of +\texttt{r} by \texttt{r'}: + +\begin{alltt} + rewrite H;reflexivity. +Qed. +\end{alltt} + +\section{Some Other instances of \texttt{Proper}} + + +We prove also that the function \texttt{move} +is proper with respect to route equivalence and Leibniz equality on points: + + +\begin{alltt} +Instance move_Proper : Proper (route_equiv ==> eq ==> eq) move. +Proof. + intros r r' Hr_r' p q Hpq. rewrite Hpq; apply Hr_r'. +Qed. +\end{alltt} + + +Let us prove now that list concatenation is proper w.r.t. +\texttt{route\_equiv}. + +First, a technical lemma, that relates \texttt{move} and list concatenation: + + +\begin{alltt} +Lemma route_compose : forall r r' P, move (r++r') P = move r' (move r P). +Proof. + induction r as [|d s IHs]; simpl; + [auto | destruct d; intros;rewrite IHs;auto]. +Qed. +\end{alltt} + +Then the proof itself: +\begin{alltt} +Instance app_route_Proper : + Proper (route_equiv ==> route_equiv ==> route_equiv) (@app direction). +Proof. + intros r r' H r'' r''' H' P. + repeat rewrite route_compose.\it\color{red} + +1 subgoal + + r : route + r' : route + H : r =r= r' + r'' : route + r''' : route + H' : r'' =r= r''' + P : Point + ============================ + move r'' (move r P) = move r''' (move r' P)\tt\color{black} + + now rewrite H, H'. +Qed. +\end{alltt} + +We are now able to compose proofs of route equivalence: + +\begin{alltt} +Example Ex2 : forall r, North::East::South::West::r =r= r. +Proof. intros r P;destruct P;simpl. + unfold route_equiv, translate;simpl;do 2 f_equal;ring. +Qed. + +Example Ex3 : forall r r', r =r= r' -> + North::East::South::West::r =r= r'. +Proof. intros r r' H. now rewrite Ex2. Qed. + +Example Ex4 : forall r r', r++ North::East::South::West::r' =r= r++r'. +Proof. intros r r'. now rewrite Ex2. Qed. +\end{alltt} + +This generalized rewriting principle applies to equivalence relations, +but also to e.g. order relations and can be used to rewrite under +binders, where the usual \texttt{rewrite} tactic fails. It is presented +in more detail in the reference manual and the article by \cite{sozeauJFR09}. + + +\subsection*{A non proper function} +It is easy to give an example of a non-proper function. Two routes may be +equivalent, but have different lengths. + +\begin{alltt} +Example length_not_Proper : ~Proper (route_equiv ==> @eq nat) (@length _). +Proof. intro H. + generalize (H (North::South::nil) nil);simpl;intro H0. + discriminate H0. + intro P;destruct P; simpl;unfold translate; simpl;f_equal;simpl;ring. +Qed +\end{alltt} + +\section{Deciding Route Equivalence} +Proofs of examples like \texttt{Ex2} may seem too complex for proving +that some routes are equivalent. It is better to define a simple boolean +function for deciding equivalence, and use reflection in case we have +closed terms of type $route$. + +We first define a boolean function : +\begin{alltt} +Definition route_eqb r r' : bool := + Point_eqb (move r Point_O) (move r' Point_O). +\end{alltt} + +Some technical lemmas proved in \texttt{Lost\_in\_NY} lead us to prove +the following equivalence, that allows us to prove some path equivalences +through a simple computation: + +\begin{alltt} +Lemma route_equiv_equivb : forall r r', route_equiv r r' <-> + route_eqb r r' = true. + +Ltac route_eq_tac := rewrite route_equiv_equivb;reflexivity. + +Example Ex1' : route_equiv (East::North::West::South::East::nil) (East::nil). +Proof. route_eq_tac. Qed. +\end{alltt} + +\section{Monoids and Setoids} +We would like to prove that route concatenation is associative, and admits +the empty route \texttt{nil} as a neutral element, making the type +\texttt{route} the carrier of some monoid. + +The \texttt{Monoid} class type defined in Sect.~\ref{Monoid-def} cannot be +used for this purpose, since the properties of associativity and +being a neutral element are defined in terms of Leibniz equality. + +We give below a definition of a new class \texttt{EMonoid} parameterized by +an equivalence relation: + +\begin{alltt} +Class EMonoid {A:Type}(E_eq :relation A)(dot : A->A->A)(one : A):=\{ + E_rel :> Equivalence E_eq; + dot_proper :> Proper (E_eq ==> E_eq ==> E_eq) dot; + E_dot_assoc : forall x y z : A, E_eq (dot x (dot y z)) (dot (dot x y) z); + E_one_left : forall x, E_eq (dot one x) x; + E_one_right : forall x, E_eq (dot x one) x \}. + +Fixpoint Epower `\{M: EMonoid A E_eq dot one\}(a:A)(n:nat) := + match n with + | 0%nat => one + | S p => dot a (Epower a p) + end. +\end{alltt} + +We register an instance of \texttt{EMonoid}: + +\begin{alltt} +Instance Route : EMonoid route_equiv (@app _) nil . +Proof. split. + apply route_equiv_Equiv. + apply app_route_Proper. + intros x y z P;repeat rewrite route_compose; trivial. + intros x P;repeat rewrite route_compose; trivial. + intros x P;repeat rewrite route_compose; trivial. +Qed. +\end{alltt} + +We can readily compute exponentiation of routes using this monoid: +\begin{alltt} +Goal forall n, Epower (South::North::nil) n =r= nil. +Proof. induction n; simpl. + reflexivity. + rewrite IHn. + route_eq_tac. +Qed. +\end{alltt} + + +\paragraph{Exercise} +It seems that route concatenation is commutative as far as route equivalence is +concerned. Is this true? In this case, define a subclass of \texttt{EMonoid} +that handles commutativity, and build an instance of this class for route +concatenation and equivalence. + +\section{Advanced Features of Type Classes} + +\subsection{Alternate definitions of the class \texttt{Monoid}} +\label{alternate} +Note that \texttt{A}, \texttt{dot} and \texttt{one} are \emph{parameters} +of this definition, whilst they could have been defined as \emph{fields} +of a structure. + +The following variant is correct too: +\begin{alltt} +Class Monoid' : Type := \{ + carrier: Type; + dot : carrier -> carrier -> carrier; + one : carrier; + dot_assoc : forall x y z:carrier, dot x (dot y z)= dot (dot x y) z; + one_left : forall x, dot one x = x; + one_right : forall x, dot x one = x\}. +\end{alltt} + +However, there is a flaw in the definition of \texttt{Monoid'}: if for some +reason one needs to consider two monoid structures ${\cal M}$ and +${\cal M'}$ on the same carrier, the sharing of the considered carrier would +be very clumsy to express and to reason about. + +\begin{alltt} +Section TwoMonoids. + Variables M M' : Monoid'. + Hypothesis same_carrier : @carrier M = @carrier M'. + Hypothesis same_one : @one M = @one M'.\it\color{red} +Toplevel input, characters 52-59: +Error: +In environment +M : Monoid' +M' : Monoid' +same_carrier : carrier = carrier +The term "one" has type "carrier" while it is expected to have type + "carrier". +\end{alltt} + +A possible solution would be using JM equality, but we don't get the +simplicity of the approach of Sect~\ref{on-monoids}. + \begin{alltt} + Require Import JMeq. + Hypothesis same_one : JMeq (@one M) (@one M'). +\end{alltt} + +Any definition using both monoids in the same expression will be filled +with coercions between the propositionally equal but not definitionally +equal carriers and operations, so this is an unworkable solution. + +A second variant could be to consider the carrier $A$ as the only parameter of +the definition and to leave the binary operation and neutral element as fields +of the class: +\begin{alltt} +Class Monoid' (A:Type) := \{ + dot : A -> A -> A; + one : A; + dot_assoc : forall x y z:A, dot x (dot y z)= dot (dot x y) z; + one_left : forall x, dot one x = x; + one_right : forall x, dot x one = x\}. +\end{alltt} + +It is possible to define the subclass of abelian monoids with this representation: +\begin{alltt} +Class AbelianMonoid' (A:Type) := \{ + underlying_monoid :> Monoid' A; + dot_comm : forall x y, dot x y = dot y x \}. + +Section Foo. + Variable A : Type. + Context (AM : AbelianMonoid' A). + + Goal forall x y z, dot x (dot y z) = dot y (dot x z). + Proof. intros x y z. + repeat rewrite dot_assoc. + now rewrite (dot_comm x y). + Qed. +End Foo. + +Require Import Arith. + +Instance Mnat : Monoid' nat. +Proof. split with plus 0;auto with arith. Defined. + +Instance AMnat : AbelianMonoid' nat. +Proof. split with Mnat. unfold dot;auto with arith. Defined. + +Goal dot 3 4 = 7. +Proof. reflexivity. Qed. +\end{alltt} + +Nevertheless, the reader will find in a paper by~\citet{math-classes} +arguments for disregarding this variant: +In short, some clumsiness would appear if we want to make \texttt{Monoid'} +a member of new classes like \texttt{Group}, \texttt{Ring}, etc. + + + +\subsection{Operational Type Classes} +Let us come back to the definitions of section Sect.~\ref{on-monoids} +Let us assume we wish to write functions and mathematical statements +with a syntax as close as possible to the standard mathematical notation. +For instance, nested applications of the \texttt{dot} operation should +be written with the help of an infix operator. + +The \texttt{Infix} command cannot be used directly, since \texttt{dot} +is not declared as a global constant. + +\begin{alltt} +Infix "*" := dot (at level 50, left associativity):M_scope. \it +Error: The reference dot was not found in the current environment. +\end{alltt} + A solution from ibid. consists in declaring a \emph{singleton type class} for representing binary operators: + +\begin{alltt} +Class monoid_binop (A:Type) := monoid_op : A -> A -> A. +\end{alltt} + +\emph{Nota: }Unlike multi-field class types, \texttt{monoid\_op} is not a constructor, +but a transparent constant such that \texttt{monoid\_op $f$} can be +$\delta\beta$-reduced into $f$. + +It is now possible to declare an infix notation: +\begin{alltt} +Delimit Scope M_scope with M. +Infix "*" := monoid_op: M_scope. +Open Scope M_scope. +\end{alltt} + +\label{Monoid-def} +We can now give a new definition of \texttt{Monoid}, using the type +\texttt{monoid\_binop $A$} instead of $A\arrow A \arrow A$, and the +infix notation \texttt{x * y} instead of \texttt{monoid\_op x y}: + +\begin{alltt} +Class Monoid (A:Type)(dot : monoid_binop A)(one : A) : Type := { + dot_assoc : forall x y z : A, x * (y * z)= x * y * z; + one_left : forall x, one * x = x; + one_right : forall x, x * one = x}. +\end{alltt} + +For building monoids like \texttt{ZMult} or \texttt{M2\_Monoid}, we +first declare instances of \texttt{monoid\_binop}. + +\begin{alltt} +Instance Zmult_op : monoid_binop Z := Zmult. + +Instance ZMult : Monoid Zmult_op 1. +Proof. split;intros; unfold Zmult_op, monoid_op; ring. Defined. + +Section matrices. + Variables (A:Type) + (zero one : A) + (plus mult minus : A -> A -> A) + (sym : A -> A). + {\color{blue}(* Definitions skipped, see section \ref{matring} *) } + + Global Instance M2_mult_op : monoid_binop M2 := M2_mult. + + Global Instance M2_Monoid : Monoid M2_mult_op Id2. + Proof. (* Proof skipped *) Defined. +End matrices. +\end{alltt} + +For dealing with matrices on \texttt{Z}, we may instantiate the parameters +\texttt{A}, \texttt{zero}, etc. + +\begin{alltt} +Instance M2_Z_op : monoid_binop (M2 Z) := M2_mult Zplus Zmult . +Instance M2_mono_Z : Monoid (M2_mult_op _ _) (Id2 _ _):= M2_Monoid Zth. + +Compute ((Build_M2 1 1 1 0) * (Build_M2 1 1 1 0))%M.\it\color{red} + = \{| c00 := 2; c01 := 1; c10 := 1; c11 := 1 |\}\tt\color{black} + : M2 Z +Compute ((Id2 0 1) * (Id2 0 1))%M.\it\color{red} + = \{| c00 := 1; c01 := 0; c10 := 0; c11 := 1 |\}\tt\color{black} + : M2 Z +\end{alltt} + + + +It is now easy to use the infix notation \texttt{*} in the definition of +functions like \texttt{power}: +\begin{alltt} +Generalizable Variables A dot one. + +Fixpoint power `\{M : Monoid A dot one\}(a:A)(n:nat) := + match n with + | 0\%nat => one + | S p => (a * power a p)\%M + end. + +Infix "**" := power (at level 30, no associativity):M_scope. + +Compute (2 ** 5) ** 2.\it += 1024 :Z\tt +Compute (Build_M2 1 1 1 0) ** 40.\it + = \{| + c00 := 165580141; + c01 := 102334155; + c10 := 102334155; + c11 := 63245986 |\} + : M2 Z +\end{alltt} + + +All the techniques we used in Sect.~\ref{equiv-proof} can be applied with +operational type classes. The main section of this proof is as follows: + +\begin{alltt} +Section About_power. + Context `(M:Monoid A). + Open Scope M_scope. + + Ltac monoid_rw := + rewrite one_left || rewrite one_right || rewrite dot_assoc. + Ltac monoid_simpl := repeat monoid_rw. + + Lemma power_x_plus : forall x n p, x ** (n + p) = x ** n * x ** p. + Proof. (* Proof skipped *) Qed. +End About_power. +\end{alltt} + +Notice that, when the section is closed, theorem statements keep the +notations of \texttt{M\_scope}: + +\begin{alltt} +Open Scope M_scope. +About power_of_power.\it\color{red} + +power_of_power : +forall (A : Type) (dot : monoid_binop A) (one : A) + (M : Monoid dot one) (x : A) (n p : nat), + (x ** n) ** p = x ** (p * n) +\end{alltt} + + +If we want to consider monoids w.r.t. some equivalence relation, +it is possible to associate an operational type class to the considered relation: + +\begin{alltt} +Require Import Setoid Morphisms. + +Class Equiv A := equiv : relation A. +Infix "==" := equiv (at level 70):type_scope. + +Open Scope M_scope. +Class EMonoid (A:Type)(E_eq :Equiv A) + (E_dot : monoid_binop A)(E_one : A):= \{ + E_rel :> Equivalence equiv; + dot_proper :> Proper (equiv ==> equiv ==> equiv) E_dot; + E_dot_assoc : forall x y z:A, + x * (y * z) == x * y * z; + E_one_left : forall x, E_one * x == x; + E_one_right : forall x, x * E_one == x\}. +\end{alltt} + +The overloaded \texttt{==} notation will refer to the appropriate +equivalence relation on the type of the arguments. One can develop in +this fashion a hierarchy of structures. In the following we define +the structure of semirings starting from a refinement of \texttt{EMonoid}. + +\begin{alltt} +(* Overloaded notations *) +Class RingOne A := ring_one : A. +Class RingZero A := ring_zero : A. +Class RingPlus A := ring_plus :> monoid_binop A. +Class RingMult A := ring_mult :> monoid_binop A. +Infix "+" := ring_plus. +Infix "*" := ring_mult. +Notation "0" := ring_zero. +Notation "1" := ring_one. + +Typeclasses Transparent RingPlus RingMult RingOne RingZero. + +Class Distribute `\{Equiv A\} (f g: A -> A -> A): Prop := + \{ distribute_l a b c: f a (g b c) == g (f a b) (f a c) + ; distribute_r a b c: f (g a b) c == g (f a c) (f b c) \}. + +Class Commutative \{A B\} `\{Equiv B\} (m: A -> A -> B): Prop := + commutativity x y : m x y == m y x. + +Class Absorb {A} `\{Equiv A\} (m: A -> A -> A) (x : A) : Prop := + \{ absorb_l c : m x c == x ; + absorb_r c : m c x == x \}. + +Class ECommutativeMonoid `(Equiv A) (E_dot : monoid_binop A) (E_one : A):= + \{ e_commmonoid_monoid :> EMonoid equiv E_dot E_one; + e_commmonoid_commutative :> Commutative E_dot \}. + +Class ESemiRing (A:Type) (E_eq :Equiv A) + (E_plus : RingPlus A) (E_zero : RingZero A) + (E_mult : RingMult A) (E_one : RingOne A):= + \{ add_monoid :> ECommutativeMonoid equiv ring_plus ring_zero ; + mul_monoid :> EMonoid equiv ring_mult ring_one ; + ering_dist :> Distribute ring_mult ring_plus ; + ering_0_mul :> Absorb ring_mult 0 \}. +\end{alltt} + +Note that we use a kind of multiple inheritance here, as a semiring contains two +monoids, one for addition and one for multiplication, that are related +by distributivity and absorbtion laws. To distinguish between the +corresponding monoid operations, we introduce the new operational type +classes \texttt{Ring}*. These classes are declared \texttt{Transparent} +for typeclass resolution, so that their expansion to +\texttt{monoid\_binop} can be used freely during conversion: they are +just abbreviations used for overloading notations. + +We also introduce classes for the standard properties of operations like +commutativity, distributivity etc... to be able to refer to them generically. + +We can now develop some generic theory on semirings using the overloaded +lemmas about distributivity or the constituent monoids. Resolution +automatically goes through the \texttt{ESemiRing} structure to find +proofs regarding the underlying monoids. + +\begin{alltt} +Section SemiRingTheory. + Context `\{ESemiRing A\}. + + Definition ringtwo := 1 + 1. + Lemma ringtwomult : forall x : A, ringtwo * x == x + x. + Proof. + intros. unfold ringtwo. + rewrite distribute_r. + now rewrite (E_one_left x). + Qed. + +End SemiRingTheory. +\end{alltt} + +\subsection{Instance Resolution} +Let us consider again the term written ``\,\applis{binary\_power\;2\; 55}\,''. +This term --- with all its arguments explicited --- is ``\,\applis{@binary\_power Z Zmult\_op 1\;2\;55}\,''. The implicit arguments +\texttt{Z}, \texttt{Zmult\_op} and \texttt{1} have been inferred +from the type \texttt{Z} of \texttt{2}, looking at the instances +of \texttt{Monoid} that were compatible with the instanciation +\texttt{A:=Z}. + +% \textbf{MS: C'est un bug de Coq de ne pas respecter la specification de +% la recherche d'instance. La specification est: on choisit l'instance +% la plus rÈcente parmis les instances applicables de la prioritÈ la +% plus faible. Dans la suite, Zmult\_op est choisit tandis que Zplus\_op +% devrait l'Ítre (mÍme prioritÈ, mais Zplus\_op est plus rÈcente). La +% gestion des prioritÈs pour indiquer la prÈfÈrence fonctionne en revanche.} + +If we consider another instance of \texttt{Monoid} with the same +domain, the instance resolution mechanism, which relies on \texttt{auto}, +may not respect the user's intuition. + +For instance, let us temporarily consider another monoid on \texttt{Z}. + +\begin{alltt} +Section Z_additive. + Instance Z_plus_op : monoid_binop Z := Zplus. + + Instance ZAdd : Monoid Z_plus_op 0. + Proof. split;intros;unfold Z_plus_op, mon_op;ring. Defined. +\end{alltt} + +Unfortunately, two instances of \texttt{monoid\_binop} are linked to the type +\texttt{Z}. Thus, a notation like \texttt{2 * 5} looks ambiguous: + +In the interaction below, the instance \texttt{Z\_plus\_op} is preferred +over \texttt{Z\_mult\_op}, as it was declared the latest. +\begin{alltt} +Compute 2 * 5.\it + = 7 + : Z +\end{alltt} + +To force an unambiguous interpretation regardless of the order of +declarations, one solution is to add to the instance declaration a +\emph{cost}, which is a natural number: the lowest the cost, the +higher is the priority. Let us consider the following two instance +declarations: + +\begin{alltt} +Instance Zmult_op : monoid_binop Z | 1 := Zmult. +Instance Zplus_op : monoid_binop Z | 2 := Zplus. + +Compute (2 * 5)%M.\it\color{red} += 10 : nat +\end{alltt} + +Now the highest priority (lowest cost) instance is selected. + + + + + +\chapter*{Conclusion} + +This concludes our tour of type classes and generalized rewriting. For +more information on classes, one can consult the lecture notes by \citet +{sozeau.Coq/classes/JFLA12} which develops other examples of +use. \citet{math-classes} develop a large hierarchy of structures +using classes, including pervasive use of generalized rewriting. +The current version of their library is available online at: +\url{https://github.com/math-classes}. +The library on categories and categorical syntax and semantics by +Benedikt Ahrens~\cite{Ahrens}, uses heavily type classes and is worth reading. + + +Generalized rewriting \citep{sozeauJFR09} is an example of the use of +type classes to develop a \emph{generic} tactic that can apply to +arbitrary user constants as long as ``Proper'' instances are declared on +them. As we've seen, the very nature of type classes is to do proof +search at typechecking-time. They are hence very fit to implement +generic tactics that depend on some properties of the terms fed to them, +for example associativity or commutativity of functions in the work of +\citet{DBLP:journals/corr/abs-1105-4537}. +They can also be used to concisely specify domain-specific proof +automation, solving side conditions for a particular class of problems +as in \cite{DBLP:conf/icfp/GonthierZND11}. These papers provide more +advanced examples and design patterns for working with type classes. + +\bibliography{biblio,morebiblio} +\bibliographystyle{plainnat} + +\end{document}