Home

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

Docker CI

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

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:

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:

String orders

The file StringOrders.v contains some order relations on strings, in particular a total lexicographic order.

The following modules are defined: