diff options
Diffstat (limited to 'theories/Logic')
29 files changed, 343 insertions, 129 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index d954f40c..2b388687 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Berardi.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) imply proof irrelevance (PI). diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 60dbf3ea..8d82bc8e 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,14 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Some facts and definitions concerning choice and description in intuitionistic logic. diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 3f36ff38..9362a11f 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* File created for Coq V5.10.14b, Oct 1995 *) (** Classical Logic *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 17b08a2f..6bc0be1d 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides classical logic and functional choice; this especially provides both indefinite descriptions and choice functions but this is weaker than providing epsilon operator and classical logic diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index ad454a4d..d35ed138 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides classical logic and definite description, which is equivalent to providing classical logic and Church's iota operator *) @@ -18,14 +16,12 @@ Set Implicit Arguments. -Require Export Classical. +Require Export Classical. (* Axiomatize classical reasoning *) +Require Export Description. (* Axiomatize constructive form of Church's iota *) Require Import ChoiceFacts. 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 }. - (** The idea for the following proof comes from [ChicliPottierSimpson02] *) Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 52ecadaf..ae32b127 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -1,14 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides classical logic and indefinite description under the form of Hilbert's epsilon operator *) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 5f4516dd..bcec657a 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,14 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Some facts and definitions about classical logic Table of contents: diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index fafa0b94..ebb73b19 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -1,14 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalUniqueChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides classical logic and unique choice; this is weaker than providing iota operator and classical logic as the definite descriptions provided by the axiom of unique choice can diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 06502d63..7d8bde71 100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -1,12 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Set.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* File created for Coq V5.10.14b, Oct 1995, by duplication of + Classical_Pred_Type.v *) (** This file is obsolete, use Classical_Pred_Type.v via Classical.v instead *) diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index bcd529f0..9d57fe88 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -1,12 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* This file is a renaming for V5.10.14b, Oct 1995, of file Classical.v + introduced in Coq V5.8.3, June 1993 *) (** Classical Predicate Logic on Type *) diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index c51050d5..d2b35da2 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -1,12 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Prop.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* File created for Coq V5.10.14b, Oct 1995 *) +(* Classical tactics for proving disjunctions by Julien Narboux, Jul 2005 *) +(* Inferred proof-irrelevance and eq_rect_eq added by Hugo Herbelin, Mar 2006 *) (** Classical Propositional Logic *) diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 94e623bd..9b28a6ab 100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file is obsolete, use Classical.v instead *) (** Classical Logic for Type *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 004fdef3..33550389 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -1,26 +1,25 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ConstructiveEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(*i $Id: ConstructiveEpsilon.v 14628 2011-11-03 23:22:45Z herbelin $ i*) -(*i $Id: ConstructiveEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(** This module proves the constructive description schema, which -infers the sigma-existence (i.e., [Set]-existence) of a witness to a -predicate from the regular existence (i.e., [Prop]-existence). One -requires that the underlying set is countable and that the predicate -is decidable. *) +(** This provides with a proof of the constructive form of definite +and indefinite descriptions for Sigma^0_1-formulas (hereafter called +"small" formulas), which infers the sigma-existence (i.e., +[Type]-existence) of a witness to a decidable predicate over a +countable domain from the regular existence (i.e., +[Prop]-existence). *) (** Coq does not allow case analysis on sort [Prop] when the goal is in -[Set]. Therefore, one cannot eliminate [exists n, P n] in order to +not in [Prop]. Therefore, one cannot eliminate [exists n, P n] in order to show [{n : nat | P n}]. However, one can perform a recursion on an inductive predicate in sort [Prop] so that the returning type of the -recursion is in [Set]. This trick is described in Coq'Art book, Sect. +recursion is in [Type]. This trick is described in Coq'Art book, Sect. 14.2.3 and 15.4. In particular, this trick is used in the proof of [Fix_F] in the module Coq.Init.Wf. There, recursion is done on an inductive predicate [Acc] and the resulting type is in [Type]. @@ -41,7 +40,7 @@ For the first one we provide explicit and short proof terms. *) (* Direct version *) -Section ConstructiveIndefiniteDescription_Direct. +Section ConstructiveIndefiniteGroundDescription_Direct. Variable P : nat -> Prop. @@ -79,11 +78,11 @@ Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} := | right no => linear_search (S m) (inv_before_witness m b no) end. -Definition constructive_indefinite_description_nat : +Definition constructive_indefinite_ground_description_nat : (exists n, P n) -> {n:nat | P n} := fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)). -End ConstructiveIndefiniteDescription_Direct. +End ConstructiveIndefiniteGroundDescription_Direct. (************************************************************************) @@ -91,7 +90,7 @@ End ConstructiveIndefiniteDescription_Direct. Require Import Arith. -Section ConstructiveIndefiniteDescription_Acc. +Section ConstructiveIndefiniteGroundDescription_Acc. Variable P : nat -> Prop. @@ -151,40 +150,40 @@ destruct (IH y Ryx) as [n Hn]. exists n; assumption. Defined. -Theorem constructive_indefinite_description_nat_Acc : +Theorem constructive_indefinite_ground_description_nat_Acc : (exists n : nat, P n) -> {n : nat | P n}. Proof. intros H; apply acc_implies_P_eventually. apply P_eventually_implies_acc_ex; assumption. Defined. -End ConstructiveIndefiniteDescription_Acc. +End ConstructiveIndefiniteGroundDescription_Acc. (************************************************************************) -Section ConstructiveEpsilon_nat. +Section ConstructiveGroundEpsilon_nat. Variable P : nat -> Prop. Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}. -Definition constructive_epsilon_nat (E : exists n : nat, P n) : nat - := proj1_sig (constructive_indefinite_description_nat P P_decidable E). +Definition constructive_ground_epsilon_nat (E : exists n : nat, P n) : nat + := proj1_sig (constructive_indefinite_ground_description_nat P P_decidable E). -Definition constructive_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_epsilon_nat E) - := proj2_sig (constructive_indefinite_description_nat P P_decidable E). +Definition constructive_ground_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_ground_epsilon_nat E) + := proj2_sig (constructive_indefinite_ground_description_nat P P_decidable E). -End ConstructiveEpsilon_nat. +End ConstructiveGroundEpsilon_nat. (************************************************************************) -Section ConstructiveEpsilon. +Section ConstructiveGroundEpsilon. (** For the current purpose, we say that a set [A] is countable if there are functions [f : A -> nat] and [g : nat -> A] such that [g] is a left inverse of [f]. *) -Variable A : Set. +Variable A : Type. Variable f : A -> nat. Variable g : nat -> A. @@ -201,24 +200,43 @@ Proof. intro n; unfold P'; destruct (P_decidable (g n)); auto. Defined. -Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}. +Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}. Proof. intro H. assert (H1 : exists n : nat, P' n). destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption. -apply (constructive_indefinite_description_nat P' P'_decidable) in H1. +apply (constructive_indefinite_ground_description_nat P' P'_decidable) in H1. destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption. Defined. -Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}. +Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}. Proof. - intros; apply constructive_indefinite_description; firstorder. + intros; apply constructive_indefinite_ground_description; firstorder. Defined. -Definition constructive_epsilon (E : exists x : A, P x) : A - := proj1_sig (constructive_indefinite_description E). - -Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E) - := proj2_sig (constructive_indefinite_description E). - -End ConstructiveEpsilon. - +Definition constructive_ground_epsilon (E : exists x : A, P x) : A + := proj1_sig (constructive_indefinite_ground_description E). + +Definition constructive_ground_epsilon_spec (E : (exists x, P x)) : P (constructive_ground_epsilon E) + := proj2_sig (constructive_indefinite_ground_description E). + +End ConstructiveGroundEpsilon. + +(* begin hide *) +(* Compatibility: the qualificative "ground" was absent from the initial +names of the results in this file but this had introduced confusion +with the similarly named statement in Description.v *) +Notation constructive_indefinite_description_nat := + constructive_indefinite_ground_description_nat (only parsing). +Notation constructive_epsilon_spec_nat := + constructive_ground_epsilon_spec_nat (only parsing). +Notation constructive_epsilon_nat := + constructive_ground_epsilon_nat (only parsing). +Notation constructive_indefinite_description := + constructive_indefinite_ground_description (only parsing). +Notation constructive_definite_description := + constructive_definite_ground_description (only parsing). +Notation constructive_epsilon_spec := + constructive_ground_epsilon_spec (only parsing). +Notation constructive_epsilon := + constructive_ground_epsilon (only parsing). +(* end hide *) diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index ace50884..fec7904e 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Decidable.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Properties of decidable propositions *) Definition decidable (P:Prop) := P \/ ~ P. diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index c59d8460..b74ebcc8 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Description.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides a constructive form of definite description; it allows to build functions from the proof of their existence in any context; this is weaker than Church's iota operator *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 257245cc..8569e55e 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,14 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show that the axiom of choice in equivalence classes entails @@ -158,8 +156,8 @@ End PredExt_RelChoice_imp_EM. (**********************************************************************) (** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) -(** This is an adaptation of Diaconescu's paradox exploiting that - proof-irrelevance is some form of extensionality *) +(** This is an adaptation of Diaconescu's theorem, exploiting the + form of extensionality provided by proof-irrelevance *) Section ProofIrrel_RelChoice_imp_EqEM. diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index 9134b3aa..cb8f8a73 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Epsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides indefinite description under the form of Hilbert's epsilon operator; it does not assume classical logic. *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 7918061c..b8e99036 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -1,13 +1,15 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *) +(* Abstraction with respect to the eq_rect_eq axiom and creation of + EqdepFacts.v by Hugo Herbelin, Mar 2006 *) (** This file axiomatizes the invariance by substitution of reflexive equality proofs [[Streicher93]] and exports its consequences, such diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 2d5f1537..d84cd824 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -1,13 +1,17 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *) +(* Further documentation and variants of eq_rect_eq by Hugo Herbelin, + Apr 2003 *) +(* Abstraction with respect to the eq_rect_eq axiom and renaming to + EqdepFacts.v by Hugo Herbelin, Mar 2006 *) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -33,7 +37,8 @@ Table of contents: -1. Definition of dependent equality and equivalence with equality +1. Definition of dependent equality and equivalence with equality of + dependent pairs and with dependent pair of equalities 2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K @@ -45,6 +50,8 @@ Table of contents: (************************************************************************) (** * Definition of dependent equality and equivalence with equality of dependent pairs *) +Import EqNotations. + Section Dependent_Equality. Variable U : Type. @@ -75,11 +82,11 @@ Section Dependent_Equality. Scheme eq_indd := Induction for eq Sort Prop. - (** Equivalent definition of dependent equality expressed as a non - dependent inductive type *) + (** Equivalent definition of dependent equality as a dependent pair of + equalities *) Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop := - eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y. + eq_dep1_intro : forall h:q = p, x = rew h in y -> eq_dep1 p x q y. Lemma eq_dep1_dep : forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y. @@ -95,13 +102,13 @@ Section Dependent_Equality. Proof. destruct 1. apply eq_dep1_intro with (refl_equal p). - simpl in |- *; trivial. + simpl; trivial. Qed. End Dependent_Equality. -Implicit Arguments eq_dep [U P]. -Implicit Arguments eq_dep1 [U P]. +Arguments eq_dep [U P] p x q _. +Arguments eq_dep1 [U P] p x q y. (** Dependent equality is equivalent to equality on dependent pairs *) @@ -116,24 +123,103 @@ Qed. Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *) -Lemma equiv_eqex_eqdep : +Lemma eq_dep_eq_sigT : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), - existT P p x = existT P q y <-> eq_dep p x q y. + eq_dep p x q y -> existT P p x = existT P q y. Proof. - split. - (* -> *) - apply eq_sigT_eq_dep. - (* <- *) destruct 1; reflexivity. Qed. -Lemma eq_dep_eq_sigT : +Lemma eq_sigT_iff_eq_dep : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), - eq_dep p x q y -> existT P p x = existT P q y. + existT P p x = existT P q y <-> eq_dep p x q y. +Proof. + split; auto using eq_sigT_eq_dep, eq_dep_eq_sigT. +Qed. + +Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *) + +Lemma eq_sig_eq_dep : + forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + exist P p x = exist P q y -> eq_dep p x q y. +Proof. + intros. + dependent rewrite H. + apply eq_dep_intro. +Qed. + +Lemma eq_dep_eq_sig : + forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + eq_dep p x q y -> exist P p x = exist P q y. Proof. destruct 1; reflexivity. Qed. +Lemma eq_sig_iff_eq_dep : + forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + exist P p x = exist P q y <-> eq_dep p x q y. +Proof. + split; auto using eq_sig_eq_dep, eq_dep_eq_sig. +Qed. + +(** Dependent equality is equivalent to a dependent pair of equalities *) + +Set Implicit Arguments. + +Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}. +Proof. + intros; split; intro H. + - change x2 with (projT1 (existT P x2 H2)). + change H2 with (projT2 (existT P x2 H2)) at 5. + destruct H. simpl. + exists eq_refl. + reflexivity. + - destruct H as (->,<-). + reflexivity. +Defined. + +Lemma eq_sigT_fst : + forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2. +Proof. + intros. + change x2 with (projT1 (existT P x2 H2)). + destruct H. + reflexivity. +Defined. + +Lemma eq_sigT_snd : + forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2. +Proof. + intros. + unfold eq_sigT_fst. + change x2 with (projT1 (existT P x2 H2)). + change H2 with (projT2 (existT P x2 H2)) at 3. + destruct H. + reflexivity. +Defined. + +Lemma eq_sig_fst : + forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2. +Proof. + intros. + change x2 with (proj1_sig (exist P x2 H2)). + destruct H. + reflexivity. +Defined. + +Lemma eq_sig_snd : + forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2. +Proof. + intros. + unfold eq_sig_fst, eq_ind. + change x2 with (proj1_sig (exist P x2 H2)). + change H2 with (proj2_sig (exist P x2 H2)) at 3. + destruct H. + reflexivity. +Defined. + +Unset Implicit Arguments. + (** Exported hints *) Hint Resolve eq_dep_intro: core. @@ -326,5 +412,5 @@ Notation inj_pairT2 := inj_pair2. End EqdepTheory. -Implicit Arguments eq_dep []. -Implicit Arguments eq_dep1 []. +Arguments eq_dep U P p x q _ : clear implicits. +Arguments eq_dep1 U P p x q y : clear implicits. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 77908b08..59088aa7 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -1,12 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* Created by Bruno Barras, Jan 1998 *) +(* Made a module instance for EqdepFacts by Hugo Herbelin, Mar 2006 *) (** We prove that there is only one proof of [x=x], i.e [refl_equal x]. This holds if the equality upon the set of [x] is decidable. diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v new file mode 100644 index 00000000..f5e71ef4 --- /dev/null +++ b/theories/Logic/ExtensionalityFacts.v @@ -0,0 +1,136 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Some facts and definitions about extensionality + +We investigate the relations between the following extensionality principles + +- Functional extensionality +- Equality of projections from diagonal +- Unicity of inverse bijections +- Bijectivity of bijective composition + +Table of contents + +1. Definitions + +2. Functional extensionality <-> Equality of projections from diagonal + +3. Functional extensionality <-> Unicity of inverse bijections + +4. Functional extensionality <-> Bijectivity of bijective composition + +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Being an inverse *) + +Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g b) = b). + +(** The diagonal over A and the one-one correspondence with A *) + +Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }. + +Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}. + +Arguments pi1 {A} _. +Arguments pi2 {A} _. + +Lemma diagonal_projs_same_behavior : forall A (x:Delta A), pi1 x = pi2 x. +Proof. + destruct x as (a1,a2,Heq); assumption. +Qed. + +Lemma diagonal_inverse1 : forall A, is_inverse (A:=A) delta pi1. +Proof. + split; [trivial|]; destruct b as (a1,a2,[]); reflexivity. +Qed. + +Lemma diagonal_inverse2 : forall A, is_inverse (A:=A) delta pi2. +Proof. + split; [trivial|]; destruct b as (a1,a2,[]); reflexivity. +Qed. + +(** Functional extensionality *) + +Local Notation FunctionalExtensionality := + (forall A B (f g : A -> B), (forall x, f x = g x) -> f = g). + +(** Equality of projections from diagonal *) + +Local Notation EqDeltaProjs := (forall A, pi1 = pi2 :> (Delta A -> A)). + +(** Unicity of bijection inverse *) + +Local Notation UniqueInverse := (forall A B (f:A->B) g1 g2, is_inverse f g1 -> is_inverse f g2 -> g1 = g2). + +(** Bijectivity of bijective composition *) + +Definition action A B C (f:A->B) := (fun h:B->C => fun x => h (f x)). + +Local Notation BijectivityBijectiveComp := (forall A B C (f:A->B) g, + is_inverse f g -> is_inverse (A:=B->C) (action f) (action g)). + +(**********************************************************************) +(** * Functional extensionality <-> Equality of projections from diagonal *) + +Theorem FunctExt_iff_EqDeltaProjs : FunctionalExtensionality <-> EqDeltaProjs. +Proof. + split. + - intros FunExt *; apply FunExt, diagonal_projs_same_behavior. + - intros EqProjs **; change f with (fun x => pi1 {|pi1:=f x; pi2:=g x; eq:=H x|}). + rewrite EqProjs; reflexivity. +Qed. + +(**********************************************************************) +(** * Functional extensionality <-> Unicity of bijection inverse *) + +Lemma FunctExt_UniqInverse : FunctionalExtensionality -> UniqueInverse. +Proof. + intros FunExt * (Hg1f,Hfg1) (Hg2f,Hfg2). + apply FunExt. intros; congruence. +Qed. + +Lemma UniqInverse_EqDeltaProjs : UniqueInverse -> EqDeltaProjs. +Proof. + intros UniqInv *. + apply UniqInv with delta; [apply diagonal_inverse1 | apply diagonal_inverse2]. +Qed. + +Theorem FunctExt_iff_UniqInverse : FunctionalExtensionality <-> UniqueInverse. +Proof. + split. + - apply FunctExt_UniqInverse. + - intro; apply FunctExt_iff_EqDeltaProjs, UniqInverse_EqDeltaProjs; trivial. +Qed. + +(**********************************************************************) +(** * Functional extensionality <-> Bijectivity of bijective composition *) + +Lemma FunctExt_BijComp : FunctionalExtensionality -> BijectivityBijectiveComp. +Proof. + intros FunExt * (Hgf,Hfg). split; unfold action. + - intros h; apply FunExt; intro b; rewrite Hfg; reflexivity. + - intros h; apply FunExt; intro a; rewrite Hgf; reflexivity. +Qed. + +Lemma BijComp_FunctExt : BijectivityBijectiveComp -> FunctionalExtensionality. +Proof. + intros BijComp. + apply FunctExt_iff_UniqInverse. intros * H1 H2. + destruct BijComp with (C:=A) (1:=H2) as (Hg2f,_). + destruct BijComp with (C:=A) (1:=H1) as (_,Hfg1). + rewrite <- (Hg2f g1). + change g1 with (action g1 (fun x => x)). + rewrite -> (Hfg1 (fun x => x)). + reflexivity. +Qed. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index a696b6c8..35db160f 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: FunctionalExtensionality.v 14641 2011-11-06 11:59:10Z herbelin $ 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. *) diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index afaeb51a..bb03c666 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index afca2ee1..8badc07c 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: IndefiniteDescription.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file provides a constructive form of indefinite description that allows to build choice functions; this is weaker than Hilbert's epsilon operator (which implies weakly classical properties) but diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 95640d67..753009e6 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: JMeq.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** John Major's Equality as proposed by Conor McBride Reference: @@ -26,6 +24,8 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := Set Elimination Schemes. +Arguments JMeq_refl {A x} , [A] x. + Hint Resolve JMeq_refl. Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. @@ -113,8 +113,7 @@ apply JMeq_refl. Qed. Lemma eq_dep_strictly_stronger_JMeq : - exists U, exists P, exists p, exists q, exists x, exists y, - JMeq x y /\ ~ eq_dep U P p x q y. + exists U P p q x y, JMeq x y /\ ~ eq_dep U P p x q y. Proof. exists bool. exists (fun _ => True). exists true. exists false. exists I. exists I. diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index 2a55f0bb..36508969 100644 --- a/theories/Logic/ProofIrrelevance.v +++ b/theories/Logic/ProofIrrelevance.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index 160ac2d5..6accc480 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 25d07fc9..d0d58e37 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RelationalChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file axiomatizes the relational form of the axiom of choice *) Axiom relational_choice : diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v index df64822d..f0876fbc 100644 --- a/theories/Logic/SetIsType.v +++ b/theories/Logic/SetIsType.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,4 +14,4 @@ Set: simply insert some Require Export of this file at starting points of the development and try to recompile... *) -Notation "'Set'" := Type (only parsing).
\ No newline at end of file +Notation "'Set'" := Type (only parsing). |