Abstract
We present an extension of a Coq library for relation algebras, where we provide support for cardinals in a point-free way. This makes it possible to reason purely algebraically, which is well-suited for mechanisation. We discuss several applications in the area of graph theory and program verification.
This work was supported by the project ANR 12IS02001 PACE.
D. Pous—This author is supported by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Berghammer, R., Höfner, P., Stucke, I.: Tool-based verification of a relational vertex coloring program. In: Kahl, W., Winter, M., Oliveira, J. (eds.) RAMiCS 2015. LNCS, vol. 9348, pp. 275–292. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24704-5_17
Berghammer, R., Stucke, I., Winter, M.: Investigating and computing bipartitions with algebraic means. In: Kahl, W., Winter, M., Oliveira, J. (eds.) RAMiCS 2015. LNCS, vol. 9348, pp. 257–274. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24704-5_16
Brunet, P., Pous, D., Stucke, I.: Cardinalities of relations in Coq. Coq Development and full version of this extended abstract (2016). http://media.informatik.uni-kiel.de/cardinal/
Furusawa, H.: Algebraic formalisations of fuzzy relations and their representation theorems. Ph.D. thesis, Department of Informatics, Kyushu University (1998)
Galatos, N., Jipsen, P., Kowalski, T., Ono, H., Lattices, R.: An Algebraic Glimpse at Substructural Logics. Elsevier, Oxford (2007)
Kahl, W.: Calculational relation-algebraic proofs in Isabelle/Isar. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 178–190. Springer, Heidelberg (2004)
Kahl, W.: Dependently-typed formalisation of relation-algebraic abstractions. In: de Swart, H. (ed.) RAMICS 2011. LNCS, vol. 6663, pp. 230–247. Springer, Heidelberg (2011)
Kawahara, Y.: On the cardinality of relations. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 251–265. Springer, Heidelberg (2006)
Pous, D.: Relation Algebra and KAT in Coq. http://perso.ens-lyon.fr/damien.pous/ra/
Pous, D.: Kleene algebra with tests and coq tools for while programs. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 180–196. Springer, Heidelberg (2013)
Schmidt, G., Ströhlein, T.: Relation algebras: concept of points and representability. Discrete Math. 54(1), 83–92 (1985)
Schmidt, G., Ströhlein, T.: Relations and Graphs - Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, Berlin (1993)
Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reason. 2(1), 41–62 (2009)
Tarski, A.: On the calculus of relations. J. Symbolic Log. 6(3), 73–89 (1941)
Tarski, A., Givant, S.: A Formalization of Set Theory without Variables, vol. 41. Colloquium Publications, AMS, Providence, Rhode Island (1987)
Wei, V.: A lower bound for the stability number of a simple graph. Bell Laboratories Technical Memorandum 81–11217-9 (1981)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Brunet, P., Pous, D., Stucke, I. (2016). Cardinalities of Finite Relations in Coq. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_29
Download citation
DOI: https://doi.org/10.1007/978-3-319-43144-4_29
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43143-7
Online ISBN: 978-3-319-43144-4
eBook Packages: Computer ScienceComputer Science (R0)