A solver for finite sets and maps
Agda's standard library contains a solver (automated prover) for equalities between expressions using operators from semirings or rings. For instance, it can automatically prove that the natural number expressions m + n + m and 2 * m + n are equal. However, this solver cannot handle truncated subtraction between natural numbers, a subtraction operation that returns zero if the second argument is larger than the first. Note that there is no "minus" operation such that n + -n = 0 for every natural number n.
The idea of this project is to start by constructing a solver for natural numbers with truncated subtraction. If this works out well, then it might be possible to extend the solver to handle other types with similar structure, for instance finite set data structures together with set difference operations.
Contact: Nils Anders Danielsson