Coq*
Coq* Homepage
[]
What is Coq* ?

This page gives a (very) short description of a branch of the development of Coq, called Coq*. This prototype is based on Bruno Bernardo's Ph.D. work, and is developed by Bruno Barras.

The theory behind this prototype is based on Miquel's Implicit Calculus of Constructions (ICC). It allows the user to use 2 kinds of products:
  • an explicit product: forall x:A,B  (or A->B)
  • an implicit product: forall [x:A],B  (or [A]->B)
    • As the notation suggests, the explicit product behaves exactly like Coq's product. The implicit one is used to tag arguments as logical (implicit). Extraction will erase them, even if they are not of the Prop kind.

    Disclaimer: the consistency of the full system is not yet established. In particular, the usage of (dependent) sums is still being studied. One typical example is the set of all objects of a given sort (the inhabitants of its types, of course this type lies in a higher universe):
    Inductive obj : Type := repr : forall [A:Type], A -> obj.
    Download

    It is available as a darcs repository. You can get a working copy with the following command:

    darcs get http://www.lix.polytechnique.fr/Labo/Bruno.Barras/darcs/V8-implicit/

    If you don't use darcs, you can simply recursively download folder

    http://www.lix.polytechnique.fr/Labo/Bruno.Barras/darcs/V8-implicit/_darcs/pristine/    .

    Note about versions: Coq* tries to follow the development of Coq as closely as possible. Currently, the above code is based on SVN revision 10047 of the development trunk of coq.

    Compilation and Installation

    It compiles in the same way as Coq:

    ./configure [...config options...]
    make
    make install

    This command builds the same executables as Coq (coqtop, coqc and coqide), both bytecode and native versions.

    Usage guidelines

    Basically, the usage is the same as Coq. You are just allowed to put [ ] around bindings to declare implicit arguments. It is not mandatory to tag implicit arguments passed to functions, the typechecker infers that automatically. See the examples below to get the idea.

    There is just one new vernacular command to print the extracted term (in the sense of ICC):
    Print Extraction <term>.

    Some tactics have been extended to support for implicit arguments.

  • generalize [ <constr> ] introduces an implicit product instead of an explicit one

    • Examples
    Here are some very simple examples developped in Coq*:
  • Euclidean division
  • Vectors (lists of a given size)
  • Impredicative Vectors (in impredicative encoding style)
  • Axioms and consequences in Coq*
  • Formalization of Paradoxes (hopefully) avoided.