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.