Project Pages Internal Pages 
ForMath /
Proof ExamplesTable of contents:
Proof Examples in WP1: Mathematical Interfaces and Reflexive TacticsRegular Expression Equivalence in Type Theory (T. Coquand, G. Gonthier and V. Siles)This is the work corresponding to deliverable 1.1 about encoding Finite Automata in Type Theory using Regular Expressions.
Executable algorithm for determinant computationThe data in these files correspond to the code annex to deliverable 1.4. Quantifier Elimination in Algebraically Closed FieldsThe code available here is part of the deliverable 1.3. This development is described in this paper published in the proceedings of the CICM'2010 international conference. Quantifier Elimination in Real Closed FieldsThe code available here is part of the deliverable 1.3. This development is described in this paper published in the Logical Methods in Computer Sciences journal.
Subresultant coefficents, Gcd computationThe code available here is part of the deliverable 1.5. Proof Examples in WP2: A library of Linear AlgebraSmith Normal form and executable rank for matrices (C. Cohen, M. Dénès, A. Mörtberg and V. Siles)This is the data for the deliverable 2.2 about Smith Normal form over Principal Ideal Domains. A formal proof of the CauchyBinet formula (V. Siles)This proof consists mainly of two files: The CoqEAL library (C. Cohen, M. Dénès, A. Mörtberg)
Proof Examples in WP3: A library of Homological Algebra and Algebraic TopologyDefinition and properties of Simplicial Complexes (Y. Bertot, L. Rideau and La Rioja node)The data in these files correspond to the code related to deliverable 3.1. A detailed description about this formalization was given in the report Report on a SSReflect week. Generation of facets of a simplicial complex from a digital image (J. Heras and M. Poza)The data in these files correspond to the code related to deliverable 3.1. A detailed description about this formalization was given in the report From Digital Images to Simplicial Complexes: A report. Incidence Simplicial Matrices (M. Dénès, J. Heras, M. Poza and L. Rideau)The data in this file correspond to the code related to deliverable 3.2.
A detailed description about this formalization was given in the paper Incidence Simplicial Matrices formalized in Coq/SSReflect.
Homology groups (J. Heras)The data in this file correspond to the code related to deliverable 3.2 about the computation of homology groups given two matrices such that their product is equal to zero. The file needs the development of executable rank for matrices given in the first proof example in WP2. Admissible Discrete Vector Fields (M. Poza)The data in this file correspond to the code related to the construction of an admissible discrete vector
field from a matrix. The algorithm which has been formalized was introduced in the paper of A. Romero and F. Sergeraert entitled "Discrete Vector Fields and Fundamental Algebraic Topology".
Homology and Persistent Homology (J. Heras, T. Coquand, A. Mörtberg, and V. Siles)The data in this file correspond to the code related to homology and persistent homology. This allows one to compute both Betti and persistent Betti numbers from simplicial complexes.
Basic Perturbation Lemma (M. Poza, C. Dominguez, J. Heras, and J. Rubio)The data in these files correspond to the code related to the formalisation of the Basic Perturbation Lemma in the finitely generated context.
A paper related to this work and the theory graph of this development can be seen at this link. In this link, we can also see the code of these files with the version 1.4 of SSReflect.
A certified reduction strategy for homological image processing (M. Poza, C. Dominguez, J. Heras, and J. Rubio)The data in these files correspond to the code related to homology and admissible discrete vector fields. Moreover, we introduce the formalisation of the Vector Field Reduction Theorem in the particular case of digital images.
A paper related to this work and the theory graph of this development can be seen at this link. In this link, we can also see the code of these files with the version 1.4 of SSReflect.
Proof Examples in WP4: Computation with Real NumbersComputing PI using arithmeticgeometric means (Y. Bertot)
Rohn's theorem, a sketch of PerronFrobenius, and canonical forms
their Frobenius normal forms and Jordan normal forms. In turn, this result is used in an incomplete sketch of a proof of the PerronFrobenius theorem. Last, the PerronFrobenius theorem is used in the proof of some of Rohn's theorems concerning the regularity of matrices with interval coefficients. An algebraic library based on type classes.Computing with real numbers and metric spaces.
