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.
- 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):
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-tactTo 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 installStructTact consists mainly of files originally developed as part of the Verdi framework, which have here been adapted for easier reuse in other projects.
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.
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: functionupdatethat modifies a function to return a new value for a specific argumentUpdate2.v: functionupdate2that modifies a function to return a new value for specific pair of argumentsListTactics.v: tactics operating on contexts withmap,NoDup, andInListUtil.v: general list lemmas, involving, e.g.,NoDup,map,filter, andfirstnAssoc.v: association lists with get, set, and delete functionsBefore.v: relationbeforecapturing when an element appears before another in a listDedup.v: functiondedupremove duplicates from a list using decidable equalityFilterMap.v: functionfilterMapthat maps a partial function on a list and ignores failuresNth.v: relationNthcapturing the element at some position in a listPrefix.v: relationPrefixcapturing when one list is a prefix of anotherRemoveAll.v: functionremove_allwhich removes all elements of one list from another; set subtractionSubseq.v: relationsubseqcapturing when one list is a subsequence of another
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 nfin_to_nat: convert afin nto anatfin_lt: an ordering onfin n, implemented usingfin_to_natfin_OT_compat: legacyOrderedTypemodule forfin n(for use withFMap)fin_OT: modernOrderedTypemodule forfin n(for use withMSet)fin_of_nat: convert anatto afin n, when possible
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: legacyOrderedTypemodule forstring(for use withFMap)string_lex_as_OT: modernOrderedTypemodule forstring(for use withMSet)
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent