Library CompOptCert.Axioms


This file collects some axioms used throughout the CompCert development.

Require ClassicalFacts.
Require FunctionalExtensionality.

Require Export Classical.
Require Export ClassicalChoice.
Require Export 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:
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.