-
Notifications
You must be signed in to change notification settings - Fork 11
/
meta.yml
154 lines (123 loc) · 5.71 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
fullname: Real closed fields
shortname: real-closed
organization: math-comp
opam_name: coq-mathcomp-real-closed
community: false
action: true
coqdoc: false
synopsis: >-
Mathematical Components Library on real closed fields
description: |-
This library contains definitions and theorems about real closed
fields, with a construction of the real closure and the algebraic
closure (including a proof of the fundamental theorem of
algebra). It also contains a proof of decidability of the first
order theory of real closed field, through quantifier elimination.
publications:
- pub_url: https://hal.inria.fr/inria-00593738v4
pub_title: "Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination"
pub_doi: 10.2168/LMCS-8(1:2)2012
- pub_url: https://hal.inria.fr/hal-00671809v2
pub_title: Construction of real algebraic numbers in Coq
pub_doi: 10.1007/978-3-642-32347-8_6
authors:
- name: Cyril Cohen
initial: true
- name: Assia Mahboubi
initial: initial
opam-file-maintainer: Cyril Cohen <[email protected]>
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
file: CECILL-B
supported_coq_versions:
text: Coq 8.17 or later
opam: '{>= "8.17"}'
tested_coq_opam_versions:
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-dev'
repo: 'mathcomp/mathcomp'
- version: 'coq-8.18'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.1"}'
description: |-
[MathComp ssreflect 2.1 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
description: |-
[MathComp field](https://math-comp.github.io)
- opam:
name: coq-mathcomp-bigenough
version: '{>= "1.0.0"}'
description: |-
[MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
namespace: mathcomp.real_closed
keywords:
- name: real closed field
documentation: |-
## Documentation
The repository contains
- the decision procedure `rcf_sat` and its corectness lemma [`rcf_satP`](https://github.com/math-comp/real-closed/blob/3721886fffb13ea9c80824043f119ffed0c780f2/theories/qe_rcf.v#L991) for the first order theory of real closed fields through
[certified quantifier elimination](https://hal.inria.fr/inria-00593738v4)
- the definition `{realclosure F}` , a [construction of the real closure of an archimedean field](https://hal.inria.fr/hal-00671809v2), which is canonically a [`rcfType`](https://github.com/math-comp/math-comp/blob/c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa/mathcomp/algebra/ssrnum.v#L63) when `F` is an archimedean field, and the characteristic theorems of section [`RealClosureTheory`](https://github.com/math-comp/real-closed/blob/3721886fffb13ea9c80824043f119ffed0c780f2/theories/realalg.v#L1477).
- the definition `complex R`, a construction of the algebraic closure of a real closed field, which is canonically a [`numClosedFieldType`](https://github.com/math-comp/math-comp/blob/c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa/mathcomp/algebra/ssrnum.v#L73) that additionally satisfies [`complexalg_algebraic`](https://github.com/math-comp/real-closed/blob/3721886fffb13ea9c80824043f119ffed0c780f2/theories/complex.v#L1324).
Except for the end-results listed above, one should not rely on anything.
The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp)
library for the [Coq](https://coq.inria.fr) proof assistant.
## Development instructions
### With nix.
1. Install nix:
- To install it on a single-user unix system where you have admin
rights, just type:
> sh <(curl https://nixos.org/nix/install)
You should run this under your usual user account, not as
root. The script will invoke `sudo` as needed.
For other configurations (in particular if multiple users share
the machine) or for nix uninstallation, go to the [appropriate
section of the nix
manual](https://nixos.org/nix/manual/#ch-installing-binary).
- You need to **log out of your desktop session and log in again** before you proceed to step 2.
- Step 1. only need to be done once on a same machine.
2. Open a new terminal. Navigate to the root of the Abel repository. Then type:
> nix-shell
- This will download and build the required packages, wait until
you get a shell.
- You need to type this command every time you open a new terminal.
- You can call `nixEnv` after you start the nix shell to see your
work environemnet (or call `nix-shell` with option `--arg
print-env true`).
3. You are now in the correct work environment. You can do
> make
and do whatever you are accustomed to do with Coq.
4. In particular, you can edit files using `emacs` or `coqide`.
- If you were already using emacs with proof general, make sure you
empty your `coq-prog-name` variables and any other proof general
options that used to be tied to a previous local installation of
Coq.
- If you do not have emacs installed, but want to use it, you can
go back to step 2. and call `nix-shell` with the following option
> nix-shell --arg withEmacs true
in order to get a temporary installation of emacs and
proof-general. Make sure you add `(require 'proof-site)` to your
`$HOME/.emacs`.