FRex AGda augMENTation
Requirements: Agda 2.6.1 and Standard Library 1.4
An extensible tactic for the Agda proof assistant, capable of synthesising proofs of algebraic identities. The tactic
(and its underlying formalisms) are all --without-K --safe, so it's compatible with a variety of Agda configurations
and, most importantly, constructive.
hello_world : ∀ {x y} → (2 + x) + (y + 3) ≡ x + (y + 5)
hello_world = fragment CSemigroupFrex +-csemigroupThe tactic builds on a library supporting the presentation of arbitrary finitary, mono-sorted (first-order) equational-theories and can automatically derive specifications for solvers for their class of models (free extensions). The tactic is compatible with any free extension making it very flexible: if you have an interesting algebraic structure, you can write a solver and immediately leverage the tactic.
At present, we have built-in support for:
- Semigroups
- Commutative semigroups
- ... (more to come)
For some more examples, see src/Fragment/Examples.
For a browsable overview of the interface, see the API documentation.
For a full description see the following:
Proof Synthesis with Free Extensions in Intensional Type Theory
Nathan Corbyn
Master's Thesis 2021
[bibtex] [pdf]
It's also worth checking out the other libraries developed as part of the Frex Project, and our publications.
