This folder contains the Reification tactics for our submission to the 2021 Coq Workshop, as well as the associated demo files.
For build instructions, see the README for the whole libary. Note that you must not follow the instructions for installing from OPAM, since the version published on OPAM does not include our additions. In short, you need to follow the "manual installation" section, which boils down to:
opam switch create fol-toolbox 4.07.1+flambda
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only
Once you are done with this, you can build the demos and their dependencies using:
cd theories
make FOL/Reification/DemoPA.vo
make FOL/Reification/DemoPAExtensional.vo
You have to include GeneralReflection.v (e.g. using Require Import FOL.Reification.GeneralReflection.).
The main tactic you will want to use is represent. It can be invoked on goals like representableP n P.
Before you can use the tactic, you must define an instance of tarski_reflector, which can easily be done using buildDefaultTarski.
A more detailed documentation can be found here. This document explains the internal operations of the reification engine, all tactics, and the extension point mechanism. It also contains hints and common mistakes one should avoid.
All files starting with Demo are demo files, which demonstrate the reification tactic.
This file proves some facts in PA semantically, i.e. we prove that these hold in all models of PA. These facts include the commutativiy of + and *. For this, we use our reification tactic to ease use of the induction axiom scheme.
This file proves the same facts as DemoPA.v. However, here we assume a model where equality is extensional. This makes the actual proofs shorter, since we can use rewriting. However, we have to use the extension point mechanism to teach the reification engine how to handle equality.
This file contains the entire reification engine, all tactic definitions, and most of the utils. Its inner workings are documented in the documentation mentioned above.