-
Notifications
You must be signed in to change notification settings - Fork 12
/
meta.yml
266 lines (213 loc) · 9.43 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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
---
fullname: Hydras & Co.
shortname: hydra-battles
organization: coq-community
community: true
action: true
synopsis: >-
Variations on Kirby & Paris' hydra battles, Gödel's 1st
incompleteness theorem, and other entertaining math in Coq
description: |-
This Coq-based project has four parts:
- An exploration of some properties of Kirby and Paris' hydra
battles, including the study of several representations of
ordinal numbers and a part of the so-called _Ketonen and Solovay
machinery_ (combinatorial properties of epsilon0).
This part also hosts a formalization by Russell O'Connor of
primitive recursive functions and Peano Arithmetic (PA).
- Some algorithms for computing _x^n_ with as few multiplications as
possible (using _addition chains_).
- A bridge to definitions and results in the
[Gaia project](https://github.com/coq-community/gaia), in particular
on ordinals.
- A proof originally by Russell O'Connor of the Gödel-Rosser 1st
incompleteness theorem, which says that any first order theory
extending NN (which is PA without induction) that is complete is
inconsistent.
Both the [documentation](https://coq-community.org/hydra-battles/doc/hydras.pdf)
and the Coq sources are _work continuously in progress_. For more information on
how the project is organized, maintained, and documented, see
[this paper](https://hal.archives-ouvertes.fr/hal-03404668) from
the proceedings of [JFLA 2022](http://jfla.inria.fr/jfla2022.html).
build: |-
## Building and installation
- To get the required dependencies, you can use [opam](https://opam.ocaml.org)
or [Nix](https://nixos.org). With opam:
- `opam install ./coq-hydra-battles.opam --deps-only` to get the _hydra battles_ dependencies;
- `opam install ./coq-addition-chains.opam --deps-only` to get the _addition chains_ dependencies.
- `opam install ./coq-gaia-hydras.opam --deps-only` to get the _gaia hydras_ dependencies.
- `opam install ./coq-goedel.opam --deps-only` to get the _Goedel_ dependencies.
With Nix, just run `nix-shell` to get all the dependencies
(including for building the documentation). If you only want the
dependencies to build a sub-package, you can run one of:
- `nix-shell --argstr job hydra-battles`
- `nix-shell --argstr job addition-chains`
- `nix-shell --argstr job gaia-hydras`
- `nix-shell --argstr job goedel`
- Building the PDF documentation also requires
[Alectryon](https://github.com/cpitclaudel/alectryon) 1.4
and [SerAPI](https://github.com/ejgallego/coq-serapi).
See [`doc/movies/Readme.md`](doc/movies/Readme.md) for details.
- The general Makefile is in the top directory:
- `make` : compilation of the Coq scripts
- `make pdf` : generation of PDF documentation as `doc/hydras.pdf`
- `make html` : generation of HTML documentation in `theories/html`
- You may also rely on `dune` to install just one part. Run:
- `dune build coq-hydra-battles.install` to build only the _hydra battles_ part
- `dune build coq-addition-chains.install` to build only the _addition chains_ part
- `dune build coq-gaia-hydras.install` to build only the _gaia hydras_ part
- `dune build coq-goedel.install` to build only the _goedel_ part
- Documentation for the `master` branch is continuously deployed at:
- https://coq-community.org/hydra-battles/doc/hydras.pdf
- https://coq-community.org/hydra-battles/theories/html/toc.html
publications:
- pub_url: https://hal.archives-ouvertes.fr/hal-03404668
pub_title: 'Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment'
- pub_url: https://arxiv.org/abs/cs/0505034
pub_title: Essential Incompleteness of Arithmetic Verified by Coq
pub_doi: 10.1007/11541868_16
- pub_url: https://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf
pub_title: Accessible Independence Results for Peano Arithmetic
pub_doi: 10.1112/blms/14.4.285
- pub_url: https://www.jstor.org/stable/2006985
pub_title: Rapidly Growing Ramsey Functions
pub_doi: 10.2307/2006985
- pub_url: https://link.springer.com/book/10.1007/978-3-642-66473-1
pub_title: Proof Theory
pub_doi: 10.1007/978-3-642-66473-1
authors:
- name: Yves Bertot
- name: Pierre Castéran
- name: Évelyne Contejean
- name: Jeremy Damour
- name: Stéphane Desarzens
- name: Russell O'Connor
- name: Karl Palmskog
- name: Clément Pit-Claudel
- name: Théo Zimmermann
maintainers:
- name: Pierre Castéran
nickname: Casteran
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: MIT License
identifier: MIT
supported_coq_versions:
text: 8.14 or later
opam: '{>= "8.14"}'
tested_coq_opam_versions:
- version: '1.18.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '1.17.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.15'
repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.14'
repo: 'mathcomp/mathcomp'
dependencies:
- opam:
name: coq-equations
version: '{>= "1.2"}'
description: |-
[Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
- 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-ssreflect
version: '{>= "1.13.0" & < "1.19"}'
description: |-
[MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 to 1.18
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp Algebra](https://github.com/math-comp/math-comp)
- opam:
name: coq-gaia-schutte
version: '{>= "1.14" & < "1.18"}'
description: |-
[Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 to 1.17
- opam:
name: coq-mathcomp-zify
version: '{< "2~"}'
description: |-
[Mczify](https://github.com/math-comp/mczify)
- opam:
name: coq-libhyps
description: |-
[LibHyps](https://github.com/Matafou/LibHyps)
- opam:
name: coq-coqprime
version: '{>= "1.3.0"}'
description: |-
[CoqPrime](https://github.com/thery/coqprime)
- opam:
name: coq-zorns-lemma
version: '{>= "10.2.0"}'
description: |-
[ZornsLemma](https://github.com/coq-community/zorns-lemma) 10.2.0 or later
namespace: hydras
keywords:
- name: Ketonen-Solovay machinery
- name: ordinals
- name: primitive recursive functions
categories:
- name: Mathematics/Combinatorics and Graph Theory
- name: Mathematics/Logic/Foundations
documentation: |-
## Contents
### Coq sources (directory theories)
- theories/ordinals
- Hydra/*.v
- Representation in _Coq_ of hydras and hydra battles
- A proof of termination of all hydra battles (using ordinal numbers below epsilon0)
- A proof that no variant bounded by some ordinal less than epsilon0 can prove this termination
- Comparison of the length of some kind of Hydra battles with the Hardy hierarchy of fast growing functions
- OrdinalNotations/*.v
- Generic formalization on ordinal notations (well-founded ordered datatypes with a comparison function)
- Epsilon0/*.v
- Data types for representing ordinals less than epsilon0 in Cantor normal form
- The _Ketonen-Solovay machinery_: canonical sequences, accessibility, paths inside epsilon0
- Representation of some hierarchies of fast growing functions
- Schutte/*.v
- An axiomatization of countable ordinals, after Kurt Schütte. It is intended to be a reference for the data types considered in theories/Epsilon0.
- Gamma0/*.v
- A data type for ordinals below Gamma0 in Veblen normal form (**draft**).
- rpo/*.v
- A contribution on _recursive path orderings_ by Evelyne Contejean.
- Ackermann/*.v
- Primitive recursive functions, first-order logic, NN, and PA
- MoreAck/*.v
- Complements to the legacy **Ackermann** library
- Prelude/*.v
- Various auxiliary definitions and lemmas
- theories/additions/*.v
- Addition chains
- theories/gaia/*.v
- Bridge to the ordinals in Gaia that are encoded following Schütte and Ackermann
- theories/goedel/*.v
- Gödel's 1st incompleteness theorem and its variations
### Exercises
- exercises/ordinals/*.v
- Exercises on ordinals
- exercises/primrec/*.v
- Exercises on primitive recursive functions
## Contributions are welcome
Any suggestion for improving the Coq scripts and/or the documentation will be taken into account.
- In particular, we would be delighted to replace proofs with simpler ones, and/or to propose various proofs or definitions of the same concept, in order to illustrate different techniques and patterns. New tactics for automatizing the proofs are welcome too.
- Along the text, we propose several _projects_, the solution of which is planned to be integrated in the development.
- Please do not hesitate to send your remarks as GitHub issues and your suggestions of improvements (including solutions of "projects") as pull requests.
- Of course, new topics are welcome !
- If you wish to contribute without having to clone the project /
install the dependencies on your machine, you may use
[Gitpod](https://gitpod.io/#https://github.com/coq-community/hydra-battles/)
to get an editor and all the dependencies in your browser, with
support to open pull requests as well.
- __Contact__ : pierre dot casteran at gmail dot com
A bibliography is at the end of the documentation. Please feel free to suggest more references to us.
---