Call-by-name Forcing in Coq
This is a plugin for Coq v8.5 that implements the call-by-name forcing translation. The translation is described in this draft.
You need Coq v8.5 development files. The
COQBIN environment variable
should be pointing to the Coq binaries folder. Echoing
make should be
The main features added by the plugin are the two following commands.
Forcing Translate foo using Obj Hom.
This translates the term
foo in the forcing layer described by the
Obj must have type
Hom must have type
Obj -> Obj -> Type. The translation takes care of the Yoneda embedding so nothing more is expected. The translation currently works for global constants and inductive types.
All constants the term
foo depends on must have been translated prior to the invocation of this command, otherwise it will fail.
Forcing Translate foo as id1 ... idn using Obj Hom.
Same as the above but allow to give a name to the translated constants. Without the provided name, the automatically generated constant is named
Note that the translation may generate several new constants, for instance in the inductive cases where in addition to the type, constructors are generated.
Forcing Definition foo : type using Obj Hom.
This command starts the proof mode and let the user provide a term whose type is the forcing translation of
type. When the proof is finished, an axiom
foo is added to the environment and the term provided by the user is added as the forcing translation of
Forcing Definition foo : type as id using Obj Hom.
Same as above but allows to give a name to the translated constant instead of the automatic