Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->StructTact
StructTact is a Coq library of structural tactics as well as lemmas about lists, finite types, and orders on strings that use the tactics. The structural tactics enable a style of proof where hypothesis names are never mentioned. When automatically generated names change during proof development, structural tactics will still work.
Meta
- Author(s):
- Ryan Doenges
- Karl Palmskog
- Keith Simmons (initial)
- James R. Wilcox (initial)
- Doug Woos (initial)
- License: BSD 2-Clause "Simplified" license
- Compatible Coq versions: 8.10 or later
- Additional dependencies: none
- Coq namespace:
StructTact
- Related publication(s):
Building and installation instructions
The easiest way to install StructTact is via OPAM:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-struct-tact
To instead build and install manually, do:
git clone https://github.com/uwplse/StructTact.git
cd StructTact
make # or make -j <number-of-cores-on-your-machine>
make install
Documentation
StructTact consists mainly of files originally developed as part of the Verdi framework, which have here been adapted for easier reuse in other projects.
Structural tactics
The structural tactics are found in the file StructTactics.v
,
and are named by analogy to the structural properties of
simple type systems: weakening, exchange, and contraction.
In the context of proof assistants, these are analogous to the ability to add
new hypotheses in the context, reorder existing hypotheses, and delete
unused hypotheses. Theoretically, Coq inherits these properties from the
underlying type system, but in practice, automatically generated hypothesis
names cause proof scripts to break when the context is adjusted in seemingly
irrelevant ways.
Structural tactics restore these properties at the level of Ltac by enabling a style of proof where hypothesis names are never mentioned. When automatically generated names change during proof development, structural tactics still work.
For tactic documentation, see the inline comments in StructTactics.v
.
Utility definitions and lemmas
The file Util.v
collects definitions, lemmas, and tactics about lists, booleans, propositions, and
functions that were useful in other projects. Notably, the following files are exported:
BoolUtil.v
: general boolean lemmas, tactics, and definitionsPropUtil.v
: general lemmas about propositions and sum typesUpdate.v
: functionupdate
that modifies a function to return a new value for a specific argumentUpdate2.v
: functionupdate2
that modifies a function to return a new value for specific pair of argumentsListTactics.v
: tactics operating on contexts withmap
,NoDup
, andIn
ListUtil.v
: general list lemmas, involving, e.g.,NoDup
,map
,filter
, andfirstn
Assoc.v
: association lists with get, set, and delete functionsBefore.v
: relationbefore
capturing when an element appears before another in a listDedup.v
: functiondedup
remove duplicates from a list using decidable equalityFilterMap.v
: functionfilterMap
that maps a partial function on a list and ignores failuresNth.v
: relationNth
capturing the element at some position in a listPrefix.v
: relationPrefix
capturing when one list is a prefix of anotherRemoveAll.v
: functionremove_all
which removes all elements of one list from another; set subtractionSubseq.v
: relationsubseq
capturing when one list is a subsequence of another
Finite types
The file Fin.v
contains definitions and lemmas related to fin n
, a type with n
elements,
isomorphic to Fin.t n
from the standard library, but with a slightly different
definition that is more convenient to work with.
The following constructions are defined on fin
:
fin_eq_dec
: decidable equalityall_fin n
: list of all elements offin n
fin_to_nat
: convert afin n
to anat
fin_lt
: an ordering onfin n
, implemented usingfin_to_nat
fin_OT_compat
: legacyOrderedType
module forfin n
(for use withFMap
)fin_OT
: modernOrderedType
module forfin n
(for use withMSet
)fin_of_nat
: convert anat
to afin n
, when possible
String orders
The file StringOrders.v
contains some order relations on strings, in particular a total lexicographic order.
The following modules are defined:
string_lex_as_OT_compat
: legacyOrderedType
module forstring
(for use withFMap
)string_lex_as_OT
: modernOrderedType
module forstring
(for use withMSet
)