diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 4 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 4 | ||||
| -rw-r--r-- | theories/Logic/Decidable.v | 9 | ||||
| -rw-r--r-- | theories/Logic/DecidableTypeEx.v | 24 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 4 | ||||
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 10 | ||||
| -rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 60 |
7 files changed, 87 insertions, 28 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index d15e2c96..31c41120 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 11238 2008-07-19 09:34:03Z herbelin $ i*) +(*i $Id: ClassicalDescription.v 11481 2008-10-20 19:23:51Z herbelin $ i*) (** This file provides classical logic and definite description, which is equivalent to providing classical logic and Church's iota operator *) @@ -21,7 +21,7 @@ Set Implicit Arguments. Require Export Classical. Require Import ChoiceFacts. -Notation Local inhabited A := A. +Notation Local inhabited A := A (only parsing). Axiom constructive_definite_description : forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 8a045ec8..db92696b 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 11238 2008-07-19 09:34:03Z herbelin $ i*) +(*i $Id: ClassicalFacts.v 11481 2008-10-20 19:23:51Z herbelin $ i*) (** Some facts and definitions about classical logic @@ -119,7 +119,7 @@ Qed. *) -Notation Local inhabited A := A. +Notation Local inhabited A := A (only parsing). Lemma prop_ext_A_eq_A_imp_A : prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index a7c098e8..00d63252 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Decidable.v 10500 2008-02-02 15:51:00Z letouzey $ i*) +(*i $Id: Decidable.v 11735 2009-01-02 17:22:31Z herbelin $ i*) (** Properties of decidable propositions *) @@ -80,6 +80,13 @@ Proof. unfold decidable; tauto. Qed. +Theorem not_iff : + forall A B:Prop, decidable A -> decidable B -> + ~ (A <-> B) -> (A /\ ~ B) \/ (~ A /\ B). +Proof. +unfold decidable; tauto. +Qed. + (** Results formulated with iff, used in FSetDecide. Negation are expanded since it is unclear whether setoid rewrite will always perform conversion. *) diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index 9c928598..9c59c519 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: DecidableTypeEx.v 11699 2008-12-18 11:49:08Z letouzey $ *) Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. @@ -46,24 +46,16 @@ Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. Definition eq_dec := M.eq_dec. End Make_UDT. -(** An OrderedType can be seen as a DecidableType *) +(** An OrderedType can now directly be seen as a DecidableType *) -Module OT_as_DT (O:OrderedType) <: DecidableType. - Module OF := OrderedTypeFacts O. - Definition t := O.t. - Definition eq := O.eq. - Definition eq_refl := O.eq_refl. - Definition eq_sym := O.eq_sym. - Definition eq_trans := O.eq_trans. - Definition eq_dec := OF.eq_dec. -End OT_as_DT. +Module OT_as_DT (O:OrderedType) <: DecidableType := O. (** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) -Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT). -Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT). -Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT). -Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT). +Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. +Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. +Module N_as_DT <: UsualDecidableType := N_as_OT. +Module Z_as_DT <: UsualDecidableType := Z_as_OT. (** From two decidable types, we can build a new DecidableType over their cartesian product. *) @@ -99,7 +91,7 @@ End PairDecidableType. (** Similarly for pairs of UsualDecidableType *) -Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: DecidableType. +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := prod D1.t D2.t. Definition eq := @eq t. Definition eq_refl := @refl_equal t. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 880ef7e2..b935a676 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v 11238 2008-07-19 09:34:03Z herbelin $ i*) +(*i $Id: Diaconescu.v 11481 2008-10-20 19:23:51Z herbelin $ i*) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show @@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) -Notation Local inhabited A := A. +Notation Local inhabited A := A (only parsing). Section ExtensionalEpsilon_imp_EM. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 844bff88..d5738c82 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 11095 2008-06-10 19:36:10Z herbelin $ i*) +(*i $Id: EqdepFacts.v 11735 2009-01-02 17:22:31Z herbelin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -53,7 +53,7 @@ Section Dependent_Equality. Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := eq_dep_intro : eq_dep p x p x. - Hint Constructors eq_dep: core v62. + Hint Constructors eq_dep: core. Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x. Proof eq_dep_intro. @@ -63,7 +63,7 @@ Section Dependent_Equality. Proof. destruct 1; auto. Qed. - Hint Immediate eq_dep_sym: core v62. + Hint Immediate eq_dep_sym: core. Lemma eq_dep_trans : forall (p q r:U) (x:P p) (y:P q) (z:P r), @@ -135,8 +135,8 @@ Qed. (** Exported hints *) -Hint Resolve eq_dep_intro: core v62. -Hint Immediate eq_dep_sym: core v62. +Hint Resolve eq_dep_intro: core. +Hint Immediate eq_dep_sym: core. (************************************************************************) (** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *) diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v new file mode 100644 index 00000000..4445b0e1 --- /dev/null +++ b/theories/Logic/FunctionalExtensionality.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: FunctionalExtensionality.v 11686 2008-12-16 12:57:26Z msozeau $ i*) + +(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. + It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) + +Set Manual Implicit Arguments. + +(** The converse of functional extensionality. *) + +Lemma equal_f : forall {A B : Type} {f g : A -> B}, + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + +(** Statements of functional extensionality for simple and dependent functions. *) + +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. + +Lemma functional_extensionality {A B} (f g : A -> B) : + (forall x, f x = g x) -> f = g. +Proof. + intros ; eauto using @functional_extensionality_dep. +Qed. + +(** Apply [functional_extensionality], introducing variable x. *) + +Tactic Notation "extensionality" ident(x) := + match goal with + [ |- ?X = ?Y ] => + (apply (@functional_extensionality _ _ X Y) || + apply (@functional_extensionality_dep _ _ X Y)) ; intro x + end. + +(** Eta expansion follows from extensionality. *) + +Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : + f = fun x => f x. +Proof. + intros. + extensionality x. + reflexivity. +Qed. + +Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. +Proof. + intros A B f. apply (eta_expansion_dep f). +Qed. |