-
Notifications
You must be signed in to change notification settings - Fork 5
/
meta.yml
219 lines (169 loc) · 8.22 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
---
fullname: ATBR
shortname: atbr
organization: coq-community
community: true
action: true
coqdoc: true
doi: 10.2168/LMCS-8(1:16)2012
plugin: true
synopsis: Coq library and tactic for deciding Kleene algebras
description: |-
This library provides algebraic tools for working with binary relations.
The main tactic provided is a reflexive tactic for solving (in)equations
in an arbitrary Kleene algebra. The decision procedure goes through
standard finite automata constructions.
Note that the initial authors consider this library to be superseded
by the Relation Algebra library, which is based on derivatives
rather than automata: https://github.com/damien-pous/relation-algebra
publications:
- pub_url: https://arxiv.org/abs/1105.4537
pub_title: Deciding Kleene Algebras in Coq
pub_doi: 10.2168/LMCS-8(1:16)2012
authors:
- name: Thomas Braibant
initial: true
- name: Damien Pous
initial: true
maintainers:
- name: Tej Chajed
nickname: tchajed
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: GNU Lesser General Public License v3.0 or later
identifier: LGPL-3.0-or-later
supported_coq_versions:
text: master (use the corresponding branch or release for other Coq versions)
opam: '{= "dev"}'
supported_ocaml_versions:
text: 4.09.0 or later
opam: '{>= "4.09.0"}'
tested_coq_opam_versions:
- version: 'dev'
namespace: ATBR
keywords:
- name: Kleene algebra
- name: finite automata
- name: semiring
- name: matrices
- name: decision procedure
- name: reflexive tactic
categories:
- name: Miscellaneous/Coq Extensions
- name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures
documentation: |
## Documentation
The development and underlying theory of the library is described in the paper
[Deciding Kleene Algebras in Coq][paper], Logical Methods in Computer Science,
Volume 8, Issue 1, 2012.
Below are succinct descriptions of each file and tactic. See also the
[coqdoc presentation][coqdoc] of the Coq source files from the latest release.
### Library files
| Filename | Description
| -------- | -----------
| ATBR | Export all relevant modules, except those related to matrices
| ATBR_Matrices | Export all relevant modules, including those related to matrices
#### Algebraic hierarchy
| Filename | Description
| -------- | -----------
| Classes | Definitions of algebraic classes of the development
| Graph | Lemmas and hints about the base class (carrier with equality)
| Monoid | Monoids, free monoids, finite iterations over a monoid, various tactics
| SemiLattice | Semilattices, tactics: normalise, reflexivity, rewrite
| SemiRing | Idempotent semirings, tactics: normalise, reflexivity, rewrite
| KleeneAlgebra | Kleene algebras, basic properties
| Converse | Structures with converse (semirings and Kleene Algebras)
| Functors | Functors between the various algebraic structures
| StrictKleeneAlgebra | Class of Strict Kleene algebras (without 0), and extension of the decision procedure
#### Models
| Filename | Description
| -------- | -----------
| Model_Relations | Kleene Algebra of (heterogeneous) binary relations
| Model_StdRelations | Kleene Algebra of standard (homogeneous) binary relations
| Model_Languages | Kleene Algebra of languages
| Model_RegExp | Kleene Algebra of regular expressions (syntactic free model), typed reification
| Model_MinMax | (min,+) Kleene Algebra (matrices on this algebra give weighted graphs)
#### Matrices
| Filename | Description
| -------- | -----------
| MxGraph | Matrices without operations; blocks definitions
| MxSemiLattice | Semilattices of matrices
| MxSemiRing | Semiring of matrices
| MxKleeneAlgebra | Kleene algebra of matrices (definition of the star operation)
| MxFunctors | Extension of functors to matrices
#### Decision procedure for KA
| Filename | Description
| -------- | -----------
| DKA_Definitions | Base definitions for the decision procedure for KA (automata types, notations, ...)
| DKA_StateSetSets | Properties about sets of sets
| DKA_CheckLabels | Algorithm to check whether two regex have the same set of labels
| DKA_Construction | Construction algorithm, and proof of correctness
| DKA_Epsilon | Removal of epsilon transitions, proof of correctness
| DKA_Determinisation | Determinisation algorithm, proof of correctness
| DKA_Merge | Union of DFAs, proof of correctness
| DKA_DFA_Language | Language recognised by a DFA, equivalence with the evaluation of the DFA
| DKA_DFA_Equiv | Equivalence check for DFAs, proof of correctness
| DecideKleeneAlgebra | Kozen's initiality proof, kleene_reflexivity tactic
#### Other tools
| Filename | Description
| -------- | -----------
| StrictStarForm | Conversion of regular expressions into strict star form, kleene_ssf tactic
| Equivalence | Tactic for solving equivalences by transitivity
#### Examples
| Filename | Description
| -------- | -----------
| Examples | Small tutorial file, that goes through our set of tactics
| ChurchRosser | Simple usages of kleene_reflexivity to prove commutation properties
| ChurchRosser_Points | Comparison between a standard CR proof and algebraic ones
#### Misc.
| Filename | Description
| -------- | -----------
| Common | Shared simple tactics and definitions
| BoolView | View mechanism for Boolean computations
| Numbers | NUM interface, to abstract over the representation of numbers, sets, and maps
| Utils_WF | Utilities about well-founded relations; partial fixpoint operators (powerfix)
| DisjointSets | Efficient implementation of a disjoint sets data structure
| Force | Functional memoisation (in case one needs efficient matrix computations)
| Reification | Reified syntax for the various algebraic structures
#### Finite sets and maps
| Filename | Description
| -------- | -----------
| MyFSets | Efficient ordered datatypes constructions (for FSets functors)
| MyFSetProperties | Handler for FSet properties
| MyFMapProperties | Handler for FMap properties
#### OCaml modules
| Filename | Description
| -------- | -----------
| `reification.ml` | reification for the reflexive tactics
### Tactics
#### Reflexive tactics
| Tactic | Description
| ------ | -----------
| `semiring_reflexivity` | solve an (in)equation on the idempotent semiring (*,+,1,0)
| `semiring_normalize` | simplify an (in)equation on the idempotent semiring (*,+,1,0)
| `semiring_clean` | simplify 0 and 1
| `semiring_cleanassoc` | simplify 0 and 1, normalize the parentheses
| `kleene_reflexivity` | solve an (in)equation in Kleene Algebras
| `ckleene_reflexivity` | solve an (in)equation in Kleene Algebras with converse
| `skleene_reflexivity` | solve an (in)equation in Strict Kleene Algebras (without 0)
| `kleene_clean_zero` | remove zeros in a KA expression
| `kleene_ssf` | put KA expressions into strict star form
#### Rewriting tactics
| Tactic | Description
| ------ | -----------
| `ac_rewrite H` | rewrite a closed equality modulo (AC) of (+)
| `monoid_rewrite H` | rewrite a closed equality modulo (A) of (*)
#### Other tactics
| Tactic | Description
| ------ | -----------
| `converse_down` | push converses down to terms leaves
| `switch` | add converses to the goal and push them down to terms leaves
## Acknowledgements
The initial authors would like to thank Guilhem Moulin and Sebastien Briais,
who participated to a preliminary version of this project. They are also grateful
to Assia Mahboubi, Matthieu Sozeau, Bruno Barras, and Hugo Herbelin for highly
stimulating discussions, as well as numerous hints for solving various problems.
[paper]: https://arxiv.org/abs/1105.4537
[coqdoc]: https://coq-community.github.io/atbr/docs/latest/coqdoc/toc.html
---