diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-28 08:27:37 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-06-28 08:27:37 +0000 |
commit | f4b416882955d9d91bca60f3eb35b95f4124a5be (patch) | |
tree | ecd9aaa949936818036ba9aa038ee9ae08c4ff59 /lib/Axioms.v | |
parent | a834a2aa0dfa9c2da663f5a645a6b086c0321871 (diff) | |
download | compcert-f4b416882955d9d91bca60f3eb35b95f4124a5be.tar.gz compcert-f4b416882955d9d91bca60f3eb35b95f4124a5be.zip |
All axioms used in the CompCert development
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Axioms.v')
-rw-r--r-- | lib/Axioms.v | 27 |
1 files changed, 27 insertions, 0 deletions
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. |