Proof Examples
Table of contents:
- WP1: Mathematical Interfaces and Reflexive Tactics
- WP2: A library of Linear Algebra
- WP3: A library of Homological Algebra and Algebraic Topology
- Definition and properties of Simplicial Complexes
- Generation of facets of a simplicial complex from a digital image
- Incidence Simplicial Matrices
- Homology groups
- Admissible Discrete Vector Fields
- Homology and Persistent Homology
- Basic Perturbation Lemma
- A certified reduction strategy for homological image processing
- WP4: Computation with Real Numbers
Proof Examples in WP1: Mathematical Interfaces and Reflexive Tactics
Regular 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.
- Coq/SSReflect development
NOTE: you will first need to rename the fileregexp-tar-bzip2.txttoregexp.tar.bzip2, was not possible to upload a bzip2 extension.
Executable algorithm for determinant computation
The data in these files correspond to the code annex to deliverable 1.4.
Quantifier Elimination in Algebraically Closed Fields
The 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 Fields
The 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 computation
The code available here is part of the deliverable 1.5.
Proof Examples in WP2: A library of Linear Algebra
Smith 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 Cauchy-Binet 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 Topology
Definition 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.
- BPL one matrix (Compatible version with SSReflect 1.3)
- BPL two matrices (Compatible version with SSReflect 1.3)
- BPL general (Compatible version with SSReflect 1.3)
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.
- DVF homology (Compatible version with SSReflect 1.3)
- Vector Field Reduction Theorem (Compatible version with SSReflect 1.3)
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 Numbers
Computing PI using arithmetic-geometric means (Y. Bertot)
- A file to be used in conjunction with Coq's standard library (version 8.4), ssreflect, and the Coquelicot library (version of july 2013)
Rohn's theorem, a sketch of Perron-Frobenius, and canonical forms
- This zip archive contains the full proof that matrices are similar to
their Frobenius normal forms and Jordan normal forms. In turn, this result is used in an incomplete sketch of a proof of the Perron-Frobenius theorem. Last, the Perron-Frobenius 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.