https://www.cl.cam.ac.uk/~jdy22/projects/frex/
Frex offers a new approach to synthesising algebraic proofs in dependently-typed programming languages, based on free extensions from universal algebra. Frex provides a common interface to algebraic reasoning, supporting the construction of terms from variables and operations, then automatically extending built-in propositional equality to support user-defined equations.
The library has two parts:
-
Core frex (
src/Frex)The basic definitions and concepts revolving free extensions.
-
Notation (
src/Notation)A hierarchy of notation in algebraic structures.
-
Frexlets (
src/Frexlet)An extensible collection of instances of the basic definitions covering common algebraic structures.
