A list of tactics for Agda…

README.md

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

When I say solver, I mean an Agda function which solves a class of problems. Usually, these require you to encode the problem statement as an Agda data type, such as the ring solver from Algebra.Solver.Ring in the standard library:

_ : ∀ (x r k : ℤ) → 2 + x + (x + (1 + x) * k + r) ≡ r + (1 + x) * (2 + k)
_ = solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r) 
                       :=
                       r :+ (con 1 :+ x) :* (con 2 :+ k))

When I say backed by, I mean that the tactic uses an external program, such as Z3, to solve problems. Tactics which use external programs do not necessarily construct proof objects.

Maintained tactics

agda-stdlib

Provides:

• a tactic for inserting congruences;
• a tactic for solving equations over monoids;
• a tactic for solving equations over rings;
• a solver for monoids;
• a solver for commutative monoids;
• a solver for idempotent commutative monoids;
• a solver for rings;

agda-prelude

Provides:

• a tactic for inserting congruences;
• a tactic for solving equations over monoids;
• a tactic for deriving decidable equality, quote, and TreeEncoding.

equality

Provides tactics for inserting congruences for propositional equality, cubical path equality, and cubical identity.

Schmitty

Provides:

• an embedding of SMT-LIB;
• a tactic for executing SMT-LIB scripts, backed by any compatible solver;
• a tactic for SMT solving, backed by any compatible solver.

agda-fragment

Provides an extensible tactic for solving equations over algebraic structures, restricted to a single carrier type.

agda-presburger

Provides a solver for Presburger arithmetic.

Unmaintained tactics

@kazkansouh

Requires unmaintained fork of Agda.

Provides:

• a tactic for SAT solving, optionally backed by Z3 or eProver;
• a tactic for CTL model checking, optionally backed by NuSMV.

AutoInAgda

Provides a tactic for proof search using hint databases, restricted to first-order terms.

agda-rw

Provides:

• a tactic for inserting congruences;
• a tactic for proof search using hint databases, restricted to first-order terms.

agda-holes

Provides a tactic for inserting congruences.

agda-stdlib PR #1158

Unmerged pull request on the standard library.

Provides a tactic for inserting congruences.

agda-ring-solver

Merged into agda-stdlib as Tactic.RingSolver.

Provides a tactic for solving polynomials over "almost commutative" rings.