From f4b416882955d9d91bca60f3eb35b95f4124a5be Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 28 Jun 2010 08:27:37 +0000 Subject: All axioms used in the CompCert development git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Axioms.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 lib/Axioms.v (limited to 'lib/Axioms.v') diff --git a/lib/Axioms.v b/lib/Axioms.v new file mode 100644 index 00000000..0d82ed4b --- /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. -- cgit