Library compcert.lib.Axioms

This file collects some axioms used throughout the CompCert development.

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.

We also use proof irrelevance.