The Logic of Coq

(Part of the Coq FAQ)

General

What is the logic of Coq?

Coq is based on an axiom-free type theory called the Calculus of Inductive Constructions (see Coquand [1], Luo [2] and Coquand–Paulin-Mohring [3] in the References section below). It includes higher-order functions and predicates, inductive and co-inductive datatypes and predicates, and a stratified hierarchy of sets.

The Calculus of Inductive Constructions can be seen as an impredicative variant of Martin-Löf's type theory, where impredicativity means that there is a type of propositions Prop which is stable by quantification over arbitrary large types, including the type of propositions itself.

Note that the logic of Coq slightly differs in the details from one version of Coq to the other. For instance, recent versions have eta for tuples, strict propositions, universe polymorphism, cumulativity in inductive types, ...

Is Coq's logic intuitionistic or classical?

Coq's logic is modular. The core logic is intuitionistic (i.e. excluded-middle A ∨ ¬A is not granted by default). It can be extended to classical logic on demand by requiring an optional module stating A ∨ ¬A.

How does the logic of Coq compare to the one of Agda, Isabelle, Lean, Mizar, ...

In contrast with Coq, Agda implements a predicative variant of Martin-Löf's type theory. As for Cubical Agda, it implements a cubical type theory (predicative, with univalence and higher inductive types).

Isabelle is a logical framework which supports many logics but the instance of Isabelle which has the largest set of library is Isabelle/HOL which is based on a polymorphic variant of Church's simple type theory (also known as Church's Higher Order Logic), which, with hindsight, is a variant of Girard's System Fω extended with classical logic, functional extensionality, propositional extensionality and Hilbert's ε choice operator. Isabelle does not have the full expressivity of dependent types but dependencies can generally be represented in the fibered way, that is by sets equipped with an indexing function (as when defining a graph as a set of vertices and a set of edges with source and target functions).

Lean implements a variant of the Calculus of Inductive Constructions.

Mizar implements Tarski-Grothendieck's set theory.

Can I define non-terminating programs in Coq?

All programs in Coq are terminating. Especially, loops must come with an evidence of their termination.

Non-terminating programs can be simulated by passing around a bound on how long the program is allowed to run before dying.

Nevertheless, Coq has an "unsafe mode" which supports the definition of programs that do not come with a proof of their termination.

How is equational reasoning working in Coq?

Coq comes with an internal notion of computation called conversion (e.g. (1+x)+y is internally equivalent to 1+(x+y); similarly applying argument a to a function mapping x to some expression t converts to the expression t where x is replaced by a). This notion of conversion (which is decidable because Coq programs are terminating) covers a certain part of equational reasoning but is limited to sequential evaluation of expressions of (not necessarily closed) programs. Besides conversion, equations have to be treated by hand or using specialised tactics.

Axioms

What axioms can be safely added to Coq?

There are a few typical useful axioms that are independent from the Calculus of Inductive Constructions and that can be safely added to Coq. These axioms are stated in the directory Logic of the standard library of Coq. The most interesting ones are:

• Excluded-middle: ∀ A : Prop, A ∨ ¬A
• Proof-irrelevance: ∀ A : Prop, ∀ p1 p2 : A, p1 = p2
• Unicity of equality proofs (or equivalently Streicher's axiom K): ∀ A, ∀ x y : A, ∀ p1 p2 : x = y, p1 = p2
• The axiom of unique choice: ∀ x, ∃! y R(x, y) → ∃ f, ∀ x R(x, f(x))
• The functional axiom of choice: ∀ x, ∃ y R(x, y) → ∃ f, ∀ x R(x, f(x))
• Definite description: ∀ A : Type, ∀ P : A → Prop, inhabited A → {x : A | (∃x, P x) → P x}
• Indefinite description: ∀ A : Type, ∀ P : A → Prop, inhabited A → {x : A | (∃!x, P x) → P x}
• Extensionality of propositions: ∀ P Q : Prop, (P ↔ Q) → P = Q
• Extensionality of predicates: ∀ P Q : A → Prop, (∀ x, P(x) ↔ Q(x)) → P = Q
• Extensionality of functions: ∀ f g : A → B, (∀ x, f(x) = g(x)) → f = g
• Univalence (also known as extensionality of types): ∀ A B : Type, (A ≃ B) ≃ (A = B) (requires to call Coq with the option -indices-matter)

Here is a visual summary of the relative strength of these axioms, most proofs can be found in directory Logic of the standard library. (Statements in boldface are the most "interesting" ones for Coq.) The justification of their validity relies on the interpretability in set theory.

XFig sources of the previous diagram.

What is the standard model of Coq?

CIC is commonly considered consistent by interpreting it in a standard set-theoretic boolean model, even with classical logic, axiom of choice and predicate extensionality added.

What is Streicher's axiom K?

Streicher's axiom K [4] is an axiom that asserts dependent elimination of reflexive equality proofs.

Axiom Streicher_K :
  forall (A : Type) (x : A) (P : x = x -> Prop),
    P (eq_refl x) -> forall p : x = x, P p.

Axiom K is equivalent to Uniqueness of Identity Proofs [4]:

Axiom UIP : forall (A : Set) (x y : A) (p1 p2: x = y), p1 = p2.

Axiom K is also equivalent to Uniqueness of Reflexive Identity Proofs [4]:

Axiom UIP_refl : forall (A : Set) (x : A) (p : x = x), p = eq_refl x.

Axiom K is also equivalent to:

Axiom eq_rec_eq :
  forall (A : Set) (x : A) (P : A -> Set) (p : P x) (h : x = x),
    p = eq_rect x P p x h.

It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs):

Inductive eq_dep (U : Set) (P : U -> Set) (p : U) (x : P p) :
  forall q : U, P q -> Prop :=
    eq_dep_intro : eq_dep U P p x p x.

Axiom eq_dep_eq :
  forall (U : Set) (u : U) (P : U -> Set) (p1 p2 : P u),
    eq_dep U P u p1 u p2 -> p1 = p2.

In the general case, axiom K is an independent statement of the Calculus of Inductive Constructions. However, it is true on decidable domains (see file Eqdep_dec.v). It is also trivially a consequence of proof-irrelevance (see below) hence of classical logic.

What is proof-irrelevance?

A specificity of the Calculus of Inductive Constructions is to permit statements about proofs. This leads to the question of comparing two proofs of the same proposition. Identifying all proofs of the same proposition is called proof-irrelevance:

∀ A : Prop, ∀ p q : A, p = q

Proof-irrelevance (in Prop) can be assumed without contradiction in Coq. It expresses that only provability matters, whatever the exact form of the proof is. This is in harmony with the common purely logical interpretation of Prop. Contrastingly, proof-irrelevance is inconsistent in Set since there are types in Set, such as the type of booleans, that are provably more than 2 elements.

Proof-irrelevance (in Prop) is a consequence of classical logic (see proofs in file Classical.v and Berardi.v). Proof-irrelevance is also a consequence of propositional extensionality (i.e. (A ↔ B) → A = B, see the proof in file ClassicalFacts.v).

Proof-irrelevance directly implies Streicher's axiom K.

What about functional extensionality?

Extensionality of functions is admittedly consistent with the Set-predicative Calculus of Inductive Constructions.

Let A, B be types. To deal with extensionality on A → B without relying on a general extensionality axiom, a possible approach is to define one's own extensional equality on A → B.

Definition ext_eq (f g : A -> B) := forall x : A, f x = g x.

and to reason on A -> B as a setoid (see the Chapter on Setoids in the Reference Manual).

Is Prop impredicative?

Yes, the sort Prop of propositions is impredicative. Otherwise said, a statement of the form ∀ A : Prop, P A can be instantiated by itself: if ∀ A : Prop, P A is provable, then P (∀ A : Prop, P A) is.

Is Set impredicative?

No, the sort Set lying at the bottom of the hierarchy of computational types is predicative in the basic Coq system. This means that a family of types in Set, e.g. ∀ A : Set, A → A, is not a type in Set and it cannot be applied on itself.

However, the sort Set was impredicative in the original versions of Coq. See the corresponding wiki page for more information.

Is Type impredicative?

No, Type is stratified. This is hidden for the user, but Coq internally maintains a set of constraints ensuring stratification.

If Type were impredicative then it would be possible to encode Girard's systems U− and U in Coq and it is known from Girard, Coquand, Hurkens and Miquel that systems U− and U are inconsistent [Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding can be found in file Logic/Hurkens.v of the Coq standard library.

For instance, when the user see ∀ X : Type, X → X : Type, each occurrence of Type is implicitly bound to a different level, say α and β and the actual statement is ∀ X : Type(α), X → X : Type(β) with the constraint α < β.

When a statement violates a constraint, the message Universe inconsistency appears. Example: fun (x : Type) (y : forall X : Type, X -> X) => y x x.

I have two proofs of the same proposition. Can I prove they are equal?

In the base Coq system, the answer is generally no. However, if classical logic is set, the answer is yes for propositions in Prop. The answer is also yes if proof irrelevance holds (see above).

There are also "simple enough" propositions for which you can prove the equality without requiring any extra axioms. This is typically the case for propositions defined deterministically as a first-order inductive predicate on decidable sets. See for instance in this section an axiom-free proof of the uniqueness of the proofs of the proposition le m n (less or equal on nat).

I have two proofs of an equality statement. Can I prove they are equal?

Yes, if equality is decidable on the domain considered (which is the case for nat, bool, etc): see Coq file Eqdep_dec.v). No otherwise, unless assuming Streicher's axiom K (see [4]) or a more general assumption such as proof-irrelevance (see above or classical logic.

All of these statements can be found in file Eqdep.v.

Can I prove that the second components of equal dependent pairs are equal?

The answer is the same as for proofs of equality statements. It is provable if equality on the domain of the first component is decidable (look at inj_right_pair from file Eqdep_dec.v), but not provable in the general case. However, it is consistent (with the Calculus of Constructions) to assume it is true. The file Eqdep.v actually provides an axiom (equivalent to Streicher's axiom K) which entails the result (look at inj_pair2 in Eqdep.v).

Impredicativity

Do False, eq, and Acc have a special status?

Although these inductive types are in Prop, their values can be eliminated while constructing objects of type Set.

This applies to all inductive types of type Prop that are:

• empty: without constructors (e.g. False)
• singleton: having one single constructor, whose arguments (if any) are all of type Prop

See also the reference manual chapter on the Calculus of Inductive Constructions.

Is Coq’s logic conservative over Coquand’s Calculus of Constructions?

In CIC, the impredicative sort of CC can be interpreted as Prop. Through this interpretation, CIC is presumably conservative over CC. The general idea is that no proof-relevant information can flow from Prop to Set, even though singleton elimination can be used. Hence types in Set should be smashable to the unit type and Set and Type themselves be mapped to Prop.

References

[1] Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2/3), 1988.

[2] Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.

[3] Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

[4] Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Proceedings of the meeting Twenty-five years of constructive type theory. Oxford University Press, 1998.

[5] Jean-Yves Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In Proceedings of the 2nd Scandinavian Logic Symposium. North-Holland, 1970.

[6] Thierry Coquand. Une Théorie des Constructions. PhD thesis, Université Paris 7, January 1985.