fragment

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 +-csemigroup

The 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.