forked from coq-community/coqeal
-
Notifications
You must be signed in to change notification settings - Fork 0
/
meta.yml
226 lines (184 loc) · 6.97 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
---
fullname: CoqEAL
shortname: coqeal
organization: coq-community
community: true
action: true
coqdoc: false
dune: false
synopsis: >-
CoqEAL - The Coq Effective Algebra Library
description: |-
This Coq library contains a subset of the work that was developed in the context
of the ForMath EU FP7 project (2009-2013). It has two parts:
- theory, which contains developments in algebra including normal forms of matrices,
and optimized algorithms on MathComp data structures.
- refinements, which is a framework to ease change of data representations during a proof.
publications:
- pub_url: https://hal.inria.fr/hal-00734505/document
pub_title: A refinement-based approach to computational algebra in Coq
pub_doi: 10.1007/978-3-642-32347-8_7
- pub_url: https://hal.inria.fr/hal-01113453/document
pub_title: Refinements for free!
pub_doi: 10.1007/978-3-319-03545-1_10
- pub_url: https://hal.inria.fr/hal-01378905/document
pub_title: A Coq Formalization of Finitely Presented Modules
pub_doi: 10.1007/978-3-319-08970-6_13
- pub_url: https://hal.inria.fr/hal-01081908/document
pub_title: Formalized Linear Algebra over Elementary Divisor Rings in Coq
pub_doi: 10.2168/LMCS-12(2:7)2016
- pub_url: https://hal.inria.fr/hal-01414881/document
pub_title: A refinement-based approach to large scale reflection for algebra
- pub_url: https://tel.archives-ouvertes.fr/tel-00986283/
pub_title: Interaction entre algèbre linéaire et analyse en formalisation des mathématiques
authors:
- name: Guillaume Cano
initial: true
- name: Cyril Cohen
initial: true
- name: Maxime Dénès
initial: true
- name: Érik Martin-Dorel
initial: false
- name: Anders Mörtberg
initial: true
- name: Damien Rouhling
initial: false
- name: Pierre Roux
initial: false
- name: Vincent Siles
initial: true
maintainers:
- name: Cyril Cohen
nickname: CohenCyril
- name: Pierre Roux
nickname: proux01
opam-file-maintainer: Cyril Cohen <cyril.cohen@inria.fr>
opam-file-version: dev
license:
fullname: MIT License
identifier: MIT
supported_coq_versions:
text: 8.13 or later (use releases for other Coq versions)
opam: '{(>= "8.13" & < "8.17~") | (= "dev")}'
dependencies:
- opam:
name: coq-bignums
description: |-
[Bignums](https://github.com/coq/bignums) same version as Coq
- opam:
name: coq-paramcoq
version: '{>= "1.1.3"}'
description: |-
[Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
- opam:
name: coq-mathcomp-multinomials
version: '{((>= "1.5.1" & < "1.7~") | = "dev")}'
description: |-
[MathComp Multinomials](https://github.com/math-comp/multinomials) >= 1.5.1 and < 1.7
- opam:
name: coq-mathcomp-algebra
version: '{((>= "1.13.0" & < "1.16~") | = "dev")}'
description: |-
[MathComp algebra](https://math-comp.github.io) 1.13.0 or later
- opam:
name: coq-mathcomp-real-closed
version: '{(>= "1.1.2" & < "1.2~") | (= "dev")}'
description: |-
[MathComp real-closed](https://math-comp.github.io) 1.1.2 or later
tested_coq_opam_versions:
- version: '1.15.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.13'
repo: 'mathcomp/mathcomp'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.16'
repo: 'mathcomp/mathcomp-dev'
namespace: CoqEAL
keywords:
- name: effective algebra
- name: elementary divisor rings
- name: Smith normal form
- name: mathematical components
- name: Bareiss
- name: Karatsuba multiplication
- name: refinements
categories:
- name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
documentation: |-
## Theory
The theory directory has the following content:
- `ssrcomplements`, `minor` `mxstructure`, `polydvd`, `similar`,
`binetcauchy`, `ssralg_ring_tac`: Various extensions of the
Mathematical Components library.
- `dvdring`, `coherent`, `stronglydiscrete`, `edr`: Hierarchy of
structures with divisibility (from rings with divisibility, PIDs,
elementary divisor rings, etc.).
- `fpmod`: Formalization of finitely presented modules.
- `kaplansky`: For providing elementary divisor rings from the
Kaplansky condition.
- `closed_poly`: Polynomials with coefficients in a closed field.
- `companion`, `frobenius_form`, `jordan`, `perm_eq_image`,
`smith_complements`: Results on normal forms of matrices.
- `bareiss_dvdring`, `bareiss`, `gauss`, `karatsuba`, `rank`
`strassen` `toomcook`, `smithpid`, `smith`: Various efficient
algorithms for computing operations on polynomials or matrices.
## Refinements
The refinements directory has the following content:
- `refinements`: Classes for refinements and refines together with
operational typeclasses for common operations.
- `binnat`: Proof that the binary naturals of Coq (`N`) are a refinement
of the MathComp unary naturals (`nat`) together with basic operations.
- `binord`: Proof that the binary natural numbers of Coq (`N`) are a refinement
of the MathComp ordinals.
- `binint`: MathComp integers (`ssrint`) are refined to a new type
parameterized by positive numbers (represented by a sigma type) and
natural numbers. This means that proofs can be done using only
lemmas from the MathComp library which leads to simpler proofs than
previous versions of `binint` (e.g., `N`).
- `binrat`: Arbitrary precision rational numbers (`bigQ`) from the
[Bignums](https://github.com/coq/bignums) library are refined to
MathComp's rationals (`rat`).
- `rational`: The rational numbers of MathComp (`rat`) are refined to
pairs of elements refining integers using parametricity of
refinements.
- `seqmatrix` and `seqmx_complements`: Refinement of MathComp
matrices (`M[R]_(m,n)`) to lists of lists (`seq (seq R)`).
- `seqpoly`: Refinement of MathComp polynomials (`{poly R}`) to lists (`seq R`).
- `multipoly`: Refinement of
[MathComp multinomials](https://github.com/math-comp/multinomials)
and multivariate polynomials to Coq
[finite maps](https://github.com/coq/coq/blob/master/theories/FSets/FMapAVL.v).
Files should use the following conventions (w.r.t. `Local` and `Global` instances):
```coq
(** Part 1: Generic operations *)
Section generic_operations.
Global Instance generic_operation := ...
(** Part 2: Correctness proof for proof-oriented types and programs *)
Section theory.
Local Instance param_correctness : param ...
(** Part 3: Parametricity *)
Section parametricity.
Global Instance param_parametricity : param ...
Proof. exact: param_trans. Qed.
End parametricity.
End theory.
```
---