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.

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 definitions
PropUtil.v: general lemmas about propositions and sum types
Update.v: function update that modifies a function to return a new value for a specific argument
Update2.v: function update2 that modifies a function to return a new value for specific pair of arguments
ListTactics.v: tactics operating on contexts with map, NoDup, and In
ListUtil.v: general list lemmas, involving, e.g., NoDup, map, filter, and firstn
Assoc.v: association lists with get, set, and delete functions
Before.v: relation before capturing when an element appears before another in a list
Dedup.v: function dedup remove duplicates from a list using decidable equality
FilterMap.v: function filterMap that maps a partial function on a list and ignores failures
Nth.v: relation Nth capturing the element at some position in a list
Prefix.v: relation Prefix capturing when one list is a prefix of another
RemoveAll.v: function remove_all which removes all elements of one list from another; set subtraction
Subseq.v: relation subseq 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 equality
all_fin n: list of all elements of fin n
fin_to_nat: convert a fin n to a nat
fin_lt: an ordering on fin n, implemented using fin_to_nat
fin_OT_compat: legacy OrderedType module for fin n (for use with FMap)
fin_OT: modern OrderedType module for fin n (for use with MSet)
fin_of_nat: convert a nat to a fin 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: legacy OrderedType module for string (for use with FMap)
string_lex_as_OT: modern OrderedType module for string (for use with MSet)

uwplse/StructTact