Module 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:
  forall {A: Type} {B : A -> Type} (f g : forall x : A, B x),
  (forall 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:
  forall {A B: Type} (f g : A -> B), (forall 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:
  forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g.
Proof @functional_extensionality.

Implicit Arguments extensionality.

Proof irrelevance


We also use proof irrelevance.

Axiom proof_irr: ClassicalFacts.proof_irrelevance.

Implicit Arguments proof_irr.