aac-tactics/meta.yml at master · rocq-community/aac-tactics · GitHub

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
---
fullname: AAC Tactics
shortname: aac-tactics
organization: rocq-community
community: true
action: true
nix: true
plugin: true
doi: 10.1007/978-3-642-25379-9_14
branch: master

synopsis: >-
  Rocq tactics for rewriting universally quantified equations, modulo
  associative (and possibly commutative and idempotent) operators

description: |-
  This Rocq plugin provides tactics for rewriting and proving universally
  quantified equations modulo associativity and commutativity of some operator,
  with idempotent commutative operators enabling additional simplifications.
  The tactics can be applied for custom operators by registering the operators and
  their properties as type class instances. Instances for many commonly used operators,
  such as for binary integer arithmetic and booleans, are provided with the plugin.

publications:
- pub_doi: 10.1007/978-3-642-25379-9_14
  pub_url: https://arxiv.org/abs/1106.4448
  pub_title: Tactics for Reasoning modulo AC in Coq

authors:
- name: Thomas Braibant
  initial: true
- name: Damien Pous
  initial: true
- name: Fabian Kunze
  initial: false

maintainers:
- name: Karl Palmskog
  nickname: palmskog

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: GNU Lesser General Public License v3.0 or later
  identifier: LGPL-3.0-or-later

supported_rocq_versions:
  text: master (use the corresponding branch or release for other Rocq versions)
  opam: '{= "dev"}'

supported_ocaml_versions:
    text: 4.09.0 or later
    opam: '{>= "4.09.0"}'

tested_rocq_opam_versions:
- version: dev
  repo: 'rocq/rocq-prover'

dependencies:
- opam:
    name: rocq-stdlib
  description: |-
    Rocq's standard library

namespace: AAC_tactics

keywords:
- name: reflexive tactic
- name: rewriting
- name: rewriting modulo associativity and commutativity
- name: rewriting modulo ac
- name: decision procedure

categories:
- name: Miscellaneous/Rocq Extensions
- name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures

documentation: |
  ## Documentation

  The following example shows an application of the tactics for reasoning over Z binary numbers:
  ```coq
  From AAC_tactics Require Import AAC.
  From AAC_tactics Require Instances.
  From Stdlib Require Import ZArith.

  Section ZOpp.
    Import Instances.Z.
    Variables a b c : Z.
    Hypothesis H: forall x, x + Z.opp x = 0.

    Goal a + b + c + Z.opp (c + a) = b.
      aac_rewrite H.
      aac_reflexivity.
    Qed.

    Goal Z.max (b + c) (c + b) + a + Z.opp (c + b) = a.
      aac_normalise.
      aac_rewrite H.
      aac_reflexivity.
    Qed.
  End ZOpp.
  ```

  The file [Tutorial.v](theories/Tutorial.v) provides a succinct introduction
  and more examples of how to use this plugin.

  The file [Instances.v](theories/Instances.v) defines several type class instances
  for frequent use-cases of this plugin, that should allow you to use it off-the-shelf.
  Namely, it contains instances for:

  - Peano naturals (`Import Instances.Peano.`)
  - Z binary numbers (`Import Instances.Z.`)
  - Lists (`Import Instances.Lists.`)
  - N binary numbers (`Import Instances.N.`)
  - Positive binary numbers (`Import Instances.P.`)
  - Rational numbers (`Import Instances.Q.`)
  - Prop (`Import Instances.Prop_ops.`)
  - Booleans (`Import Instances.Bool.`)
  - Relations (`Import Instances.Relations.`)
  - all of the above (`Import Instances.All.`)

  To understand the inner workings of the tactics, please refer to
  the `.mli` files as the main source of information on each `.ml` file.

  ## Acknowledgements

  The initial authors are grateful to Evelyne Contejean, Hugo Herbelin,
  Assia Mahboubi, and Matthieu Sozeau for highly instructive discussions.
  The plugin took inspiration from the plugin tutorial "constructors" by
  Matthieu Sozeau, distributed under the LGPL 2.1.
---