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 full description see the following:

      Proof Synthesis with Free Extensions in Intensional Type Theory (link to come)
      Nathan Corbyn
      Master's Thesis 2020

It's also worth checking out the other libraries developed as part of the Frex Project, and our publications.