Library compcert.lib.Axioms


This file collects some axioms used throughout the CompCert development.

Require ClassicalFacts.
Require FunctionalExtensionality.

Extensionality axioms

The Require FunctionalExtensionality gives us functional extensionality for dependent function types:

Lemma functional_extensionality_dep:
  ∀ {A: Type} {B : A → Type} (f g : ∀ x : A, B x),
  (∀ x, f x = g x) → f = g.
Proof @FunctionalExtensionality.functional_extensionality_dep.

and, as a corollary, functional extensionality for non-dependent functions:

Lemma functional_extensionality:
  ∀ {A B: Type} (f g : A → B), (∀ x, f x = g x) → f = g.
Proof @FunctionalExtensionality.functional_extensionality.

For compatibility with earlier developments, extensionality is an alias for functional_extensionality.

Lemma extensionality:
  ∀ {A B: Type} (f g : A → B), (∀ x, f x = g x) → f = g.
Proof @functional_extensionality.

Proof irrelevance

We also use proof irrelevance.

Axiom proof_irr: ClassicalFacts.proof_irrelevance.

Arguments proof_irr [A].