All axioms used in the CompCert development

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 27 insertions, 0 deletions

diff --git a/lib/Axioms.v b/lib/Axioms.v
new file mode 100644
index 0000000..0d82ed4
--- /dev/null
+++ b/lib/Axioms.v
@@ -0,0 +1,27 @@
+Require ClassicalFacts.
+
+(* We use just 2 axioms of extensionality:
+
+1.  Functional extensionality for dependent functions
+  (FunctionalExtensionality.functional_extensionality_dep)
+   forall {A} {B : A -> Type},   forall (f g : forall x : A, B x), (forall x, f x = g x) -> f = g.
+
+2.  Propositional extensionality  (forall A B:Prop, (A <-> B) -> A = B.)
+
+*)
+
+Require Export FunctionalExtensionality.  (* Contains one Axiom *)
+
+Axiom prop_ext: ClassicalFacts.prop_extensionality.
+Implicit Arguments prop_ext.
+
+Lemma proof_irr: ClassicalFacts.proof_irrelevance.
+Proof.
+exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext).
+Qed.
+Implicit Arguments proof_irr.
+
+Lemma extensionality:
+ forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
+Proof. intros; apply functional_extensionality. auto. Qed.
+Implicit Arguments extensionality.