CoqAndAxioms

This page lists the key axioms that one may consider using in their Coq development.

Proof irrelevance

Proof irrelevance asserts that two proofs of a same proposition are equal.

Axiom proof_irrelevance :
  forall (P : Prop) (p q : P), p = q.

Proof irrelevance is useful for proving equalities between values of types of the form {x | P x}. Proof irrelevance is derivable from propositional extensionality.

Axiom K / Uniqueness of Identity Proofs

Streicher's axiom K is stated as follows.

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

A common equivalent form to axiom K is Uniqueness of Identity Proofs (UIP).

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

Another common equivalent form is Uniqueness of Reflexivity Proofs.

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

Yet another common equivalent form is the injectivity of dependent pairs.

Axiom inj_dep_pair : forall (A : Type) (P : A -> Type) (p : A) (x y : P p),
  existT P p x = existT P p y -> x = y.

of which the particular case when A := Type and P := fun X => X, known as elimination of John Major's equality, is again equivalent to axiom K.

Axiom JMeq_eq : forall (A : Type) (x y : A),
   JMeq A x A y -> x = y.

where JMeq A x A y is an explicit inductive definition, equivalent to existT (fun X => X) A x = existT (fun X => X) A y.

The axiom K is useful for performing non-trivial inversions on definitions involving dependent types. Nevertheless, any A whose equality is decidable satisfies axiom K by a theorem from Hedberg.

Note 1: since Coq standard library states x = y by default in Prop, axiom K for this equality is a consequence of proof irrelevance.

Note 2: axiom K is incompatible with the univalence axiom, which itself requires equality to be stated in Type, using the option -indices-matter.

Functional extensionality

Functional extensionality asserts that two functions that produce equal results on all arguments are equal. For dependently-typed functions, the axiom is as follows.

Axiom func_ext_dep : forall (A : Type) (B : A -> Type) (f g : forall x, B x),
  (forall x, f x = g x) -> f = g.

In the particular case of functions with a non-dependent type, the axiom admits the following simpler form.

Lemma func_ext : forall A B (f g : A -> B),
  (forall x, f x = g x) -> f = g.

Extensionality results for functions of several arguments can be derived from the basic axiom.

Propositional extensionality

Propositional extensionality asserts that two equivalent propositions are equal.

Axiom prop_ext : forall (P Q : Prop),
  (P <-> Q) -> P = Q.

Propositional extensional is convenient for performing rewriting. It is needed for using Hilbert's epsilon operator in practice and, in particular, to build quotient structures in the general case.

Propositional extensionality combined with functional extensionality entails predicate extensionality.

Excluded middle (classical logic)

The excluded middle asserts that any proposition is either true or false. The excluded middle is needed to establish some mathematical results, in particular those related to undecidable properties or formal semantics about Turing-complete languages (e.g., equivalence between big-step and small-step semantics).

Axiom classic : forall (P : Prop), P \/ ~ P.

The above axiom is provable from indefinite description and proof irrelevance. With propositional extensionality, the excluded middle can also be stated in the following way.

Axiom prop_degeneracy : forall (P : Prop),
   P = True \/ P = False.

Strong excluded middle

The strong excluded middle asserts that one can build a value by dynamically testing whether a proposition is true or false. This axiom is non-constructive.

Axiom classicT : forall (P : Prop), {P} + {~ P}.

With this axiom, one can write If P then x else y for any proposition P.

This axiom is derivable from indefinite description and the excluded middle.

Axiom of choice

The axiom of choice is required for proving certain mathematical results. The axiom of choice can take many different forms. The functional choice is one of the most common.

Axiom func_choice : forall A B (R : A -> B -> Prop),
  (forall x, exists y, R x y) ->
  exists f, forall x, R x (f x).

A useful strengthened version is the omniscient choice axiom, which involves a pre-condition and delays the need for exhibiting the proof of functionality. (Below, {Inhab B} asserts that B is inhabited.)

Axiom omniscient_func_choice : forall A `{Inhab B} (R : A -> B -> Prop),
  exists f, forall x, (exists y, R x y) -> R x (f x).

The axiom of functional choice is a direct consequence of the indefinite description axiom. The omniscient version moreover require classical logic to be derived.

Indefinite description / Hilbert's epsilon operator

The indefinite description axiom asserts that from a proof of type exists x, P x one can construct a value of type {x | P x}. This axiom is non-constructive.

Axiom indefinite_description : forall (A : Type) (P : A -> Prop),
   ex P -> sig P.

Indefinite description can be used for example to build quotient structures in the general case, or to build the fixed point of an arbitrarily-complex functional.

Equivalently, one can take as axiom Hilbert's epsilon operator which, given a predicate P, returns a value x satisfying P if there exists one, otherwise returns an arbitrary value.

Axiom epsilon : forall `{Inhab A} (P : A -> Prop), A.
Axiom epsilon_spec : forall `{Inhab A} (P : A -> Prop),
  (exists x, P x) -> P (epsilon P).

Above Inhab A indicates that the type A is inhabited, but without specifying which inhabitant is considered. This notion can be defined using a type class as follows.

Class Inhab (A : Type) : Prop :=
  { inhabited : exists x : A, True }.

Summary

All the axioms listed above can be derived from the three following axioms:

• dependent functional extensionality,
• propositional extensionality,
• indefinite description.