diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-15 14:47:20 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-15 14:47:20 +0000 |
commit | c511207bd0f25c4199770233175924a725526bd3 (patch) | |
tree | c5644b7b4d3577a96e7d823d51a90e049e25d386 | |
parent | 3064d1d1ec7a2781779b074d6d7d91ba9b990832 (diff) | |
download | compcert-c511207bd0f25c4199770233175924a725526bd3.tar.gz compcert-c511207bd0f25c4199770233175924a725526bd3.zip |
Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4.
VERSION: bump version number.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2379 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | VERSION | 3 | ||||
-rw-r--r-- | lib/Axioms.v | 40 |
2 files changed, 18 insertions, 25 deletions
@@ -1,4 +1,3 @@ -2.0 - +2.2 diff --git a/lib/Axioms.v b/lib/Axioms.v index 52a7fffa..6ae8669a 100644 --- a/lib/Axioms.v +++ b/lib/Axioms.v @@ -16,44 +16,38 @@ (** This file collects some axioms used throughout the CompCert development. *) Require ClassicalFacts. +Require FunctionalExtensionality. (** * Extensionality axioms *) -(** The following [Require Export] gives us functional extensionality for dependent function types: -<< -Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, - forall (f g : forall x : A, B x), - (forall x, f x = g x) -> f = g. ->> -and, as a corollary, functional extensionality for non-dependent functions: -<< -Lemma functional_extensionality {A B} (f g : A -> B) : +(** 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: *) -Require Export FunctionalExtensionality. + +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. intros; apply functional_extensionality. auto. Qed. +Proof @functional_extensionality. Implicit Arguments extensionality. -(** We also assert propositional extensionality. *) - -Axiom prop_ext: ClassicalFacts.prop_extensionality. -Implicit Arguments prop_ext. - (** * Proof irrelevance *) -(** We also use proof irrelevance, which is a consequence of propositional - extensionality. *) +(** We also use proof irrelevance. *) + +Axiom proof_irr: ClassicalFacts.proof_irrelevance. -Lemma proof_irr: ClassicalFacts.proof_irrelevance. -Proof. - exact (ClassicalFacts.ext_prop_dep_proof_irrel_cic prop_ext). -Qed. Implicit Arguments proof_irr. |