An Exceptional Type Theory in Coq
This plugin allows to automatically translate Coq terms in such a way that they can now use exceptions. This can be useful for programming, e.g. to allow failure locally and prove after the fact that assuming a few properties the translated term does not fail, without endangering reduction as a monadic translation would do. This can also be used to extend the logical power of Coq itself, allowing to prove a few semi-classical principles amongst which independent of premises or Markov's rule.
A draft paper describing the translation can be found here.
This requires Coq 8.7. If the
COQBIN variable is correctly set, a
invokation should be enough.
Alternatively, one can install this plugin through OPAM. Assuming the Coq repositories are available (see the official documentation), it is enough to do the following.
opam pin add coq-exceptional-tt https://github.com/CoqHott/exceptional-tt.git opam install coq-exceptional-tt
Use of the plugin
The plugin adds four new commands which we describe below.
Effect Translate GLOBAL [using GLOBAL].
This command translates the given global definition into the type theory with
exception. The resulting term is parameterized over the type of exceptions used.
It can be restricted to a particular exception type by adding the
Beware, the resulting theory is inconsistent in general. You need to show parametricity to ensure consistency, see below.
Parametricity Translate GLOBAL [using GLOBAL].
This command automatically proves that the term generated by
is parametric and thus does not endanger consistency. All global definitions
used by the original term must have been shown to be parametric for this to
using clause can be used to specialize the type of exceptions
used. Generic and instantiated effectful and parametricity terms can be mixed
as long as it makes sense, e.g. it is legal to write
Effect Translate foo. Parametricity Translate foo using bar.
Effect Translate foo using bar. Parametricity Translate foo using bar.
but the following will fail:
Effect Translate foo using bar. Parametricity Translate foo.
Effect Definition IDENT : TYPE [using GLOBAL].
This command opens the proof mode and ask the user to provide a proof of TYPE in the effectful translation. When the proof is complete, the axiom IDENT is added to Coq, a term IDENTᵉ is defined with the content of the proof, and the axiom IDENT is registered to be mapped to IDENTᵉ through the effectful translation.
Parametricity Definition GLOBAL [using GLOBAL].
This command opens the proof mode and ask the user to provide a proof that the mentioned global is indeed parametric. When the proof is complete, an axiom is added to Coq, whose parametricity translation is mapped to the provided proof.
The repository contains a few examples in the
Sections are not handled.
The translation cannot properly handle the impredicative universe Prop. In the current implementation, it interprets Prop as Type, and will fail dynamically with a universe inconsistency if the original proof-term actually relied on impredicativity.
The translation does not handle primitive records nor universe polymorphism yet.
The parametric translation is not generic over fixpoints. It can only translate
a well-behaved subset of them and will dynamically fail with a typing error
if not on that fragment. We recommand using the
Parametric Definition command
to handwrite the proof in that case.
This software is licensed under the WTFPL 2.0.