Contribution: ClassicalRealizability

Krivine's classical realizability



The aim of this Coq library is to provide a framework for checking proofs in Krivine's classical realizability for second-order Peano arithmetic. It is designed to be as extensible as the original theory by Krivine and to support on-the-fly extensions by new instructions with their evaluation rules.


classical realizability, krivine's realizability, primitive datatype, non determinism, quote, axiom of countable choice, real numbers


Copyright (c) 2014, Lionel Rieg


The aim of the library is to provide a framework for checking proofs in
Krivine's classical realizability.

As the original theory by Krivine, it is very modular and supports extension of
the KAM by new instructions and their evaluation rules on the fly.  The main
limitation of this library is that it currently only admits to use one pole at
a time.  In particular, any proof using more than one pole (like the absence of
a univesal realizer of the recurrence axiom under a deterministic evaluation)
cannot be directly expressed.

The library is structured as follows:
+ A core component gathered in Kbase.v:
  - ShallowEmbedding.v: basic definition of the KAM and Krivine's realizability
  - Tactics.v: automatization tactics to ease proofs
  - BasicResults.v: elementary results in calssical realizability
  - Subtyping.v: subtyping between formulæ which permits simpler reasoning
  - PropEmbedding.v: a translation of Prop into realizability formulæ
+ Several extensions of the core theory:
  - SimpleExtensions.v: easy extensions by adding new instructions
  - Peano.v: realization of Peano arithmetic
  - KBool.v: description, properties and specification of booleans
  - Fork.v: description, properties and specification of non-determinism
  - Quote.v: the 'quote' instruction, with the realizer of the countable AC
  - Dedekind: partial formalization of real numbers by Dedekind cuts
  - Integers.v: native integers
  - Rationals.v: native rational numbers
+ A partial formalization of real numbers by (a variant of) Cauchy sequences,
  gatherd in Reals.v:
  - QcOrderedType.v, QcComplement.v, Qcminmax.v, Qcabs.v: auxiliary results
    about the QCanon type, including a definition of absolute value
  - Real_defintions.v: basic definition of reals numbers
  - Real_relations.v: comparisons on real numbers and their properties
  - Real_operations.v: operations on real numbers and their properties
  - Real_axioms.v: Axioms of real numbers


Simply type compile all the files with:

If it does not work, you can easily regenerate the makefile with the following
    coq_makefile *.v -o makefile

It is known to compile with Coq v.8.4pl3.

To generate the documentation in an existing directiry "doc/", type
   coqdoc --utf8 -g -d doc/ *.v


This library is available under the CeCILL-B licence.

Available files