blob: 38fc514e1402f6b0906db000ba1ab06db4fb0b59 (
plain)
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
|
aac_tactics
===========
Thomas Braibant & Damien Pous
Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France
FOREWORD
========
This plugin provides tactics for rewriting universally quantified
equations, modulo associativity and commutativity of some operators.
INSTALLATION
============
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-aac-tactics
DOCUMENTATION
=============
Please refer to Tutorial.v for a succinct introduction on how to use
this plugin.
To understand the inner-working of the tactic, please refer to the
.mli files as the main source of information on each .ml
file. Alternatively, [make world] generates ocamldoc/coqdoc
documentation in directories doc/ and html/, respectively.
File Instances.v defines several instances for frequent use-cases of
this plugin, that should allow you to use it out-of-the-shelf. Namely,
we have instances for:
- Peano naturals (Import Instances.Peano)
- Z binary numbers (Import Instances.Z)
- N binary numbers (Import Instances.N)
- P binary numbers (Import Instances.P)
- Rationnal numbers (Import Instances.Q)
- Prop (Import Instances.Prop_ops)
- Booleans (Import Instances.Bool)
- Relations (Import Instances.Relations)
- All of the above (Import Instances.All)
ACKNOWLEDGEMENTS
================
We are grateful to Evelyne Contejean, Hugo Herbelin, Assia Mahboubi
and Matthieu Sozeau for highly instructive discussions.
This plugin took inspiration from the plugin tutorial "constructors",
distributed under the LGPL 2.1, copyrighted by Matthieu Sozeau
|
