Introducing the finite-prover library (was: [Agda] Feedback requested on automated decision module)

[Samuel Gélineau]

After Gregory Crosswhite's automated decision module, here is the
library finite-prover, which does the same thing, but faster and with
a simpler API. Here is where you can find the code and how you could
use it:

http://github.com/agda/agda-finite-prover


⋅-identity : Identity I _⋅_
⋅-identity = auto finitePauli 1 (λ x → I ⋅ x ≈ x) refl
           , auto finitePauli 1 (λ x → x ⋅ I ≈ x) refl

⋅-commutative : Commutative _⋅_
⋅-commutative = auto finitePauli 2 (λ x y → x ⋅ y ≈ y ⋅ x) refl

⋅-inverse : Inverse I (λ x → x) _⋅_
⋅-inverse = auto finitePauli 1 (λ x → x ⋅ x ≈ I) refl
          , auto finitePauli 1 (λ x → x ⋅ x ≈ I) refl

⋅-associative : Associative _⋅_
⋅-associative = auto finitePauli 3 (λ x y z → (x ⋅ y) ⋅ z ≈ x ⋅ (y ⋅ z)) refl


finite-prover's strategy is to instantiate the proposition at every
possible combination of arguments, yielding a large matrix containing
all possibilities. The matrix generated by the left-hand side is then
compared with the matrix generated by the right-hand side, in one
swift refl check.

The automated decision library, on the other hand, decides each
proposition using nested applications of Fin's "all?" and extracts the
witness from the resulting (yes _) instance. One advantage of this
library is that it can also prove that an equation does *not* hold, by
extracting the witness from the resulting (no _) instance. In
practice, however, deciding propositions is much slower than comparing
matrices.

On my machine, type-checking ⋅-identity, ⋅-commutative and ⋅-inverse
is 4 times faster (12 seconds vs 3 seconds) using finite-prover than
using the automated decision module. The real difference, however,
occurs when type-checking ⋅-associative: finite-prover did not take
noticeably longer than with the other examples, while the automated
decision module hung for a long while until it eventually ran out of
stack space!

---

I'd like to add a few notes regarding the internals of the
implementation. In addition to an implementation of Data.Matrix which
might be useful to other projects, finite-prover contains two
generalizations of (Data.Vec.N-ary). The first makes it possible to
use (N-ary n A B) when A and B live at different levels, and the
second allows B to depend on the vector (xs : Vec n A) of arguments
preceding it. This makes it possible for an expression like (auto _ n
P refl) to have a type like (∀ x y → x ⋅ y ≡ y ⋅ x), where (x ⋅ y ≡ y
⋅ x) depends on the arguments x and y and has level zero regardless of
the level of those arguments.

Hoping you find my library and/or its N-ary generalizations useful,
– Samuel