Abstracts.2018.ProofByReflection

Proof by Reflection

by Jannis Limperg

Code with notes

Proof by reflection (which is only superficially related to Agda's Reflection metaprogramming facilities) is a proof technique for dependently typed languages. It is typically used to build solvers for a class of problems, for example determining whether a formula of propositional logic is true. These solvers can replace lengthy manual proofs, and they are typically more efficient than tactics based on metaprogramming.

I will live-code the second-most boring example of proof by reflection: a simplifier for equations in a monoid. Afterwards, I'll talk briefly about variations on the basic technique and more interesting applications.