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
|
### **Equations** - a function definition plugin.
[](https://github.com/mattam82/Coq-Equations/actions/workflows/build.yml)
[](https://zenodo.org/record/3012649#.XcEydZNKjOQ)
[](https://coq.zulipchat.com/#narrow/stream/237659-Equations-devs.20.26.20users)
Copyright 2009-2022 Matthieu Sozeau `matthieu.sozeau@inria.fr`
Copyright 2015-2018 Cyprien Mangin `cyprien.mangin@m4x.org`
Distributed under the terms of the GNU Lesser General Public License
Version 2.1 or later
(see
[LICENSE](http://github.com/mattam82/Coq-Equations/raw/main/LICENSE)
for details).
Equations provides a notation for writing programs by dependent
pattern-matching and (well-founded) recursion
in [Coq](http://coq.inria.fr). It compiles everything down to
eliminators for inductive types, equality and accessibility,
providing a definitional extension to the Coq kernel.
The plugin can be used with Coq's standard logic in `Prop`
for a proof-irrelevant, erasable interpretation of pattern-matching,
or with a polymorphic logic in `Type` or re-using the prelude
of the [HoTT/Coq](http://github.com/HoTT/HoTT) library for a
proof-relevant interpretation. In all cases, the resulting
definitions are axiom-free.
***Table of Contents***
- [Documentation](#documentation)
- [Papers](#papers)
- [Gallery](examples)
- [Installation](#installation)
- [HoTT Variant](#hott-variant)
## Live demo
Try it now in your browser with [JSCoq](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html)!
## Documentation
- The [reference manual](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations.pdf)
provides an introduction and a summary of the commands and options.
This introduction can also be followed interactively with Equations installed:
[equations_intro.v](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations_intro.v)
- A gallery of [examples](http://mattam82.github.io/Coq-Equations/examples) provides more consequent
developments using Equations.
## Papers and presentations
- [Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq](https://sozeau.gitlabpages.inria.fr/www/research/publications/Equations_Reloaded-ICFP19.pdf). Matthieu Sozeau and Cyprien Mangin.
In: Proc. ACM Program. Lang. 3, ICFP, Article 86 (August 2019), 29 pages. [DOI](https://doi.org/10.1145/3341690),
[slides](https://sozeau.gitlabpages.inria.fr/www/research/publications/Equations_Reloaded-ICFP19-190819.pdf).
This presents version 1.2 and above of the package.
See [Equations Reloaded](http://mattam82.github.io/Coq-Equations/equations-reloaded) for associated material, including a VM to run the examples.
- [Equations for HoTT](https://sozeau.gitlabpages.inria.fr/www/research/publications/Equations_for_HoTT-HoTT19-130819.pdf).
Matthieu Sozeau, Talk given at the [Homotopy Type Theory 2019](https://hott.github.io/HoTT-2019//programme/#sozeau)
Conference in Pittsburgh, PA, August 2019.
This explains the no-confusion principle and strong equivalences
used by Equations and Jesper Cockx's version of dependent pattern-matching in Agda
in terms of HoTT.
- [Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study](https://sozeau.gitlabpages.inria.fr/www/research/publications/Equations_for_Hereditary_Substitution_in_Leivants_Predicative_System_F:_a_case_study.pdf).
Cyprien Mangin and Matthieu Sozeau.
In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice.
Volume 185 of EPTCS. May 2015 - LFMTP'15.
This is a case study on a proof of normalization for an hereditary substitution procedure on a variant of System F.
- [Equations: A Dependent Pattern-Matching Compiler](https://link.springer.com/chapter/10.1007/978-3-642-14052-5_29) Matthieu
Sozeau (2010)
In: Kaufmann M., Paulson L.C. (eds) Interactive Theorem
Proving. ITP 2010. Lecture Notes in Computer Science,
vol 6172. Springer, Berlin, Heidelberg.
This presents an earlier version of the package.
## Installation
The latest version works with Coq 8.13 (branch
[8.13](https://github.com/mattam82/Coq-Equations/tree/8.13)),
Coq 8.14 (branch
[8.14](https://github.com/mattam82/Coq-Equations/tree/8.14)),
Coq 8.15 (branch
[8.15](https://github.com/mattam82/Coq-Equations/tree/8.15)),
and the current Coq main branch (branch
[main](https://github.com/mattam82/Coq-Equations/tree/main)).
See [releases](https://github.com/mattam82/Coq-Equations/releases) for
sources and official releases.
### Install with OPAM
This package is available on [OPAM](http://opam.ocaml.org/).
Activate the [Coq repository](https://coq.inria.fr/opam-using.html)
if you didn't do it yet:
opam repo add coq-released https://coq.inria.fr/opam/released
and run:
opam install coq-equations
To get the beta versions of Coq, activate the repository:
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
To get the development version of Equations, activate the repository:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
### Install from source
Alternatively, to compile Equations, simply run:
./configure.sh
make
in the toplevel directory, with `coqc` and `ocamlc` in your path.
Optionally, one can build the test-suite or examples:
make examples test-suite
Then add the paths to your `.coqrc`:
Add ML Path "/Users/mat/research/coq/equations/src".
Add Rec LoadPath "/Users/mat/research/coq/equations/theories" as Equations.
Or install it:
make install
As usual, you will need to run this command with the appropriate privileges
if the version of Coq you are using is installed system-wide, rather than
in your own directory. E.g. on Ubuntu, you would prefix the command with
`sudo` and then enter your user account password when prompted.
## HoTT Variant
The HoTT variant of Equations works with the coq-hott library for Coq 8.13 and up. When using `opam`, simply install first the `coq-hott` library and `coq-equations` will install its HoTT variant. From source, first
install `coq-hott` and then use:
./configure.sh --enable-hott
This will compile the `HoTT` library variant in addition to the standard one.
Then, after `make install`, one can import the plugin in Coq, using:
From Equations Require Import HoTT.All.
|
