diff options
Diffstat (limited to 'theories/Logic')
29 files changed, 418 insertions, 204 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index d954f40c..38377573 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-2012 *) (* \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). @@ -47,7 +45,7 @@ Lemma AC_IF : (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). Proof. intros P B e1 e2 Q p1 p2. -unfold IFProp in |- *. +unfold IFProp. case (EM B); assumption. Qed. @@ -78,7 +76,7 @@ Record retract_cond : Prop := Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. Proof. intros r. -case r; simpl in |- *. +case r; simpl. trivial. Qed. @@ -115,7 +113,7 @@ Lemma retract_pow_U_U : retract (pow U) U. Proof. exists g f. intro a. -unfold f, g in |- *; simpl in |- *. +unfold f, g; simpl. apply AC. exists (fun x:pow U => x) (fun x:pow U => x). trivial. @@ -132,8 +130,8 @@ Definition R : U := g (fun u:U => Not_b (u U u)). Lemma not_has_fixpoint : R R = Not_b (R R). Proof. -unfold R at 1 in |- *. -unfold g in |- *. +unfold R at 1. +unfold g. rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). trivial. exists (fun x:pow U => x) (fun x:pow U => x); trivial. @@ -143,7 +141,7 @@ Qed. Theorem classical_proof_irrelevence : T = F. Proof. generalize not_has_fixpoint. -unfold Not_b in |- *. +unfold Not_b. apply AC_IF. intros is_true is_false. elim is_true; elim is_false; trivial. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 60dbf3ea..1a32d518 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-2012 *) (* \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. @@ -346,7 +344,7 @@ Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. Proof. intros rel_choice proof_irrel. - red in |- *; intros A B P R H. + red; intros A B P R H. destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)). intros (x,HPx). destruct (H x HPx) as (y,HRxy). @@ -387,7 +385,7 @@ Qed. Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice : ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice). Proof. - auto decomp using + intuition auto using guarded_rel_choice_imp_rel_choice, rel_choice_and_proof_irrel_imp_guarded_rel_choice. Qed. @@ -441,7 +439,7 @@ Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice : FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises <-> GuardedFunctionalChoice. Proof. - auto decomp using + intuition auto using guarded_fun_choice_imp_indep_of_general_premises, guarded_fun_choice_imp_fun_choice, fun_choice_and_indep_general_prem_imp_guarded_fun_choice. @@ -482,7 +480,7 @@ Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice : FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox <-> OmniscientFunctionalChoice. Proof. - auto decomp using + intuition auto using omniscient_fun_choice_imp_small_drinker, omniscient_fun_choice_imp_fun_choice, fun_choice_and_small_drinker_imp_omniscient_fun_choice. @@ -549,7 +547,7 @@ Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon : (EpsilonStatement -> SmallDrinker'sParadox * ConstructiveIndefiniteDescription). Proof. - auto decomp using + intuition auto using epsilon_imp_constructive_indefinite_description, constructive_indefinite_description_and_small_drinker_imp_epsilon, epsilon_imp_small_drinker. @@ -582,7 +580,7 @@ Lemma classical_denumerable_description_imp_fun_choice : (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R. Proof. intros A Descr. - red in |- *; intros R Rdec H. + red; intros R Rdec H. set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y'). destruct (Descr R') as (f,Hf). intro x. @@ -691,7 +689,7 @@ Qed. Corollary dep_iff_non_dep_functional_rel_reification : FunctionalRelReification <-> DependentFunctionalRelReification. Proof. - auto decomp using + intuition auto using non_dep_dep_functional_rel_reification, dep_non_dep_functional_rel_reification. Qed. @@ -816,9 +814,9 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : (forall P:Prop, P \/ ~ P) -> forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. Proof. - intros FunReify EM C; auto decomp using - constructive_definite_descr_excluded_middle, - (relative_non_contradiction_of_definite_descr (C:=C)). + intros FunReify EM C H. + apply relative_non_contradiction_of_definite_descr; trivial. + auto using constructive_definite_descr_excluded_middle. Qed. (**********************************************************************) diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 3f36ff38..d25e0e21 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-2012 *) (* \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..479056c9 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-2012 *) (* \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..2fd6e68e 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-2012 *) (* \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,13 +16,11 @@ 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 }. +Local Notation inhabited A := A (only parsing). (** The idea for the following proof comes from [ChicliPottierSimpson02] *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 52ecadaf..7ab991f8 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-2012 *) (* \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..34ae1cd5 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-2012 *) (* \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: @@ -119,7 +117,7 @@ Qed. *) -Notation Local inhabited A := A (only parsing). +Local Notation inhabited A := A (only parsing). Lemma prop_ext_A_eq_A_imp_A : prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. @@ -150,7 +148,7 @@ Proof. case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). intro f. - pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. + pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1. rewrite (g1_o_g2 (fun x:A => f (g1 x x))). reflexivity. Qed. @@ -193,13 +191,13 @@ Section Proof_irrelevance_gen. intros Ext Ind. case (ext_prop_fixpoint Ext bool true); intros G Gfix. set (neg := fun b:bool => bool_elim bool false true b). - generalize (refl_equal (G neg)). - pattern (G neg) at 1 in |- *. + generalize (eq_refl (G neg)). + pattern (G neg) at 1. apply Ind with (b := G neg); intro Heq. rewrite (bool_elim_redl bool false true). - change (true = neg true) in |- *; rewrite Heq; apply Gfix. + change (true = neg true); rewrite Heq; apply Gfix. rewrite (bool_elim_redr bool false true). - change (neg false = false) in |- *; rewrite Heq; symmetry in |- *; + change (neg false = false); rewrite Heq; symmetry ; apply Gfix. Qed. @@ -209,9 +207,9 @@ Section Proof_irrelevance_gen. intros Ext Ind A a1 a2. set (f := fun b:bool => bool_elim A a1 a2 b). rewrite (bool_elim_redl A a1 a2). - change (f true = a2) in |- *. + change (f true = a2). rewrite (bool_elim_redr A a1 a2). - change (f true = f false) in |- *. + change (f true = f false). rewrite (aux Ext Ind). reflexivity. Qed. @@ -230,9 +228,9 @@ Section Proof_irrelevance_Prop_Ext_CC. Definition FalseP : BoolP := fun C c1 c2 => c2. Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : - c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. + c1 = BoolP_elim C c1 c2 TrueP := eq_refl c1. Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : - c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. + c2 = BoolP_elim C c1 c2 FalseP := eq_refl c2. Definition BoolP_dep_induction := forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. @@ -265,9 +263,9 @@ Section Proof_irrelevance_CIC. | trueP : boolP | falseP : boolP. Definition boolP_elim_redl (C:Prop) (c1 c2:C) : - c1 = boolP_ind C c1 c2 trueP := refl_equal c1. + c1 = boolP_ind C c1 c2 trueP := eq_refl c1. Definition boolP_elim_redr (C:Prop) (c1 c2:C) : - c2 = boolP_ind C c1 c2 falseP := refl_equal c2. + c2 = boolP_ind C c1 c2 falseP := eq_refl c2. Scheme boolP_indd := Induction for boolP Sort Prop. Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. @@ -346,8 +344,8 @@ Section Proof_irrelevance_EM_CC. Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). Proof. - unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); - unfold b2p in |- *; intros. + unfold p2b; intro A; apply or_dep_elim with (b := em A); + unfold b2p; intros. apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). destruct (b H). Qed. @@ -355,8 +353,8 @@ Section Proof_irrelevance_EM_CC. Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. Proof. intro not_eq_b1_b2. - unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); - unfold b2p in |- *; intros. + unfold p2b; intro A; apply or_dep_elim with (b := em A); + unfold b2p; intros. assumption. destruct not_eq_b1_b2. rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H. @@ -394,9 +392,9 @@ Section Proof_irrelevance_CCI. Hypothesis em : forall A:Prop, A \/ ~ A. Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) - (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). + (a:A) : f a = or_ind f g (or_introl B a) := eq_refl (f a). Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) - (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). + (b:B) : g b = or_ind f g (or_intror A b) := eq_refl (g b). Scheme or_indd := Induction for or Sort Prop. Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index fafa0b94..4a4fc23f 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-2012 *) (* \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..cda9d22c 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-2012 *) (* \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..7e1a4096 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-2012 *) (* \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 *) @@ -41,7 +42,7 @@ Qed. Lemma not_ex_all_not : forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. Proof. (* Intuitionistic *) -unfold not in |- *; intros P notex n abs. +unfold not; intros P notex n abs. apply notex. exists n; trivial. Qed. @@ -51,20 +52,20 @@ Lemma not_ex_not_all : Proof. intros P H n. apply NNPP. -red in |- *; intro K; apply H; exists n; trivial. +red; intro K; apply H; exists n; trivial. Qed. Lemma ex_not_not_all : forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). Proof. (* Intuitionistic *) -unfold not in |- *; intros P exnot allP. +unfold not; intros P exnot allP. elim exnot; auto. Qed. Lemma all_not_not_ex : forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). Proof. (* Intuitionistic *) -unfold not in |- *; intros P allnot exP; elim exP; intros n p. +unfold not; intros P allnot exP; elim exP; intros n p. apply allnot with n; auto. Qed. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index c51050d5..1f6b05f5 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-2012 *) (* \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 *) @@ -18,7 +20,7 @@ Axiom classic : forall P:Prop, P \/ ~ P. Lemma NNPP : forall p:Prop, ~ ~ p -> p. Proof. -unfold not in |- *; intros; elim (classic p); auto. +unfold not; intros; elim (classic p); auto. intro NP; elim (H NP). Qed. @@ -33,7 +35,7 @@ Qed. Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P. Proof. -intros; apply NNPP; red in |- *. +intros; apply NNPP; red. intro; apply H; intro; absurd P; trivial. Qed. @@ -66,7 +68,7 @@ Qed. Lemma or_not_and : forall P Q:Prop, ~ P \/ ~ Q -> ~ (P /\ Q). Proof. -simple induction 1; red in |- *; simple induction 2; auto. +simple induction 1; red; simple induction 2; auto. Qed. Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q. @@ -110,7 +112,7 @@ Module Eq_rect_eq. Lemma eq_rect_eq : forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. -intros; rewrite proof_irrelevance with (p1:=h) (p2:=refl_equal p); reflexivity. +intros; rewrite proof_irrelevance with (p1:=h) (p2:=eq_refl p); reflexivity. Qed. End Eq_rect_eq. diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 94e623bd..86fdd69f 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-2012 *) (* \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..89d3eebc 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-2012 *) (* \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 15714 2012-08-08 18:54:37Z 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. @@ -113,7 +112,7 @@ of our searching algorithm. *) Let R (x y : nat) : Prop := x = S y /\ ~ P y. -Notation Local acc x := (Acc R x). +Local Notation acc x := (Acc R x). Lemma P_implies_acc : forall x : nat, P x -> acc x. Proof. @@ -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..aaf1813b 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-2012 *) (* \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..3e5d4ef0 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-2012 *) (* \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..87b27987 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-2012 *) (* \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 @@ -63,7 +61,7 @@ Variable pred_extensionality : PredicateExtensionality. Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B. Proof. intros A B H. - change ((fun _ => A) true = (fun _ => B) true) in |- *. + change ((fun _ => A) true = (fun _ => B) true). rewrite pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B). reflexivity. @@ -136,8 +134,8 @@ right. intro HP. assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b). intro b; split. -unfold class_of_false in |- *; right; assumption. -unfold class_of_true in |- *; right; assumption. +unfold class_of_false; right; assumption. +unfold class_of_true; right; assumption. assert (Heq : class_of_true = class_of_false). apply pred_extensionality with (1 := Hequiv). apply diff_true_false. @@ -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. @@ -190,8 +188,8 @@ Lemma projT1_injective : a1=a2 -> a1'=a2'. Proof. intro Heq ; unfold a1', a2', A'. rewrite Heq. - replace (or_introl (a2=a2) (refl_equal a2)) - with (or_intror (a2=a2) (refl_equal a2)). + replace (or_introl (a2=a2) (eq_refl a2)) + with (or_intror (a2=a2) (eq_refl a2)). reflexivity. apply proof_irrelevance. Qed. @@ -267,7 +265,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) -Notation Local inhabited A := A (only parsing). +Local Notation inhabited A := A (only parsing). Section ExtensionalEpsilon_imp_EM. @@ -281,7 +279,7 @@ Hypothesis epsilon_extensionality : forall (A:Type) (i:inhabited A) (P Q:A->Prop), (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q. -Notation Local eps := (epsilon bool true) (only parsing). +Local Notation eps := (epsilon bool true) (only parsing). Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P. Proof. diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index 9134b3aa..da3e5b08 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-2012 *) (* \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..6841334f 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-2012 *) (* \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..a22f286e 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-2012 *) (* \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. @@ -94,14 +101,14 @@ Section Dependent_Equality. forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. Proof. destruct 1. - apply eq_dep1_intro with (refl_equal p). - simpl in |- *; trivial. + apply eq_dep1_intro with (eq_refl p). + 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 *) @@ -114,26 +121,105 @@ Proof. apply eq_dep_intro. Qed. -Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *) +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.2"). (* 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. @@ -164,12 +250,12 @@ Section Equivalences. (** Uniqueness of Reflexive Identity Proofs *) Definition UIP_refl_ := - forall (x:U) (p:x = x), p = refl_equal x. + forall (x:U) (p:x = x), p = eq_refl x. (** Streicher's axiom K *) Definition Streicher_K_ := - forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. (** Injectivity of Dependent Equality is a consequence of *) (** Invariance by Substitution of Reflexive Equality Proof *) @@ -303,14 +389,14 @@ Proof (eq_dep_eq__UIP U eq_dep_eq). (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) -Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x. +Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. Proof (UIP__UIP_refl U UIP). (** Streicher's axiom K is a direct consequence of Uniqueness of Reflexive Identity Proofs *) Lemma Streicher_K : - forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. Proof (UIP_refl__Streicher_K U UIP_refl). End Axioms. @@ -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..3a6f6a23 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -1,14 +1,15 @@ (************************************************************************) (* 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-2012 *) (* \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]. +(** We prove that there is only one proof of [x=x], i.e [eq_refl x]. This holds if the equality upon the set of [x] is decidable. A corollary of this theorem is the equality of the right projections of two equal dependent pairs. @@ -42,7 +43,7 @@ Section EqdepDec. Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' := eq_ind _ (fun a => a = y') eq2 _ eq1. - Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = refl_equal y. + Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = eq_refl y. Proof. intros. case u; trivial. @@ -60,7 +61,7 @@ Section EqdepDec. Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v. intros. - unfold nu in |- *. + unfold nu. case (eq_dec x y); intros. reflexivity. @@ -68,13 +69,13 @@ Section EqdepDec. Qed. - Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v. + Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v. Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u. Proof. intros. - case u; unfold nu_inv in |- *. + case u; unfold nu_inv. apply trans_sym_eq. Qed. @@ -89,10 +90,10 @@ Section EqdepDec. Qed. Theorem K_dec : - forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p. + forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p. Proof. intros. - elim eq_proofs_unicity with x (refl_equal x) p. + elim eq_proofs_unicity with x (eq_refl x) p. trivial. Qed. @@ -114,7 +115,7 @@ Section EqdepDec. Proof. intros. cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). - simpl in |- *. + simpl. case (eq_dec x x). intro e. elim e using K_dec; trivial. @@ -134,7 +135,7 @@ Require Import EqdepFacts. Theorem K_dec_type : forall A:Type, (forall x y:A, {x = y} + {x <> y}) -> - forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. Proof. intros A eq_dec x P H p. elim p using K_dec; intros. @@ -145,7 +146,7 @@ Qed. Theorem K_dec_set : forall A:Set, (forall x y:A, {x = y} + {x <> y}) -> - forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. Proof fun A => K_dec_type (A:=A). (** We deduce the [eq_rect_eq] axiom for (decidable) types *) @@ -211,13 +212,13 @@ Module DecidableEqDep (M:DecidableType). (** Uniqueness of Reflexive Identity Proofs *) - Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x. + Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. Proof (UIP__UIP_refl U UIP). (** Streicher's axiom K *) Lemma Streicher_K : - forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. Proof (K_dec_type eq_dec). (** Injectivity of equality on dependent pairs in [Type] *) @@ -280,13 +281,13 @@ Module DecidableEqDepSet (M:DecidableSet). (** Uniqueness of Reflexive Identity Proofs *) - Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x. + Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. Proof N.UIP_refl. (** Streicher's axiom K *) Lemma Streicher_K : - forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. + forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. Proof N.Streicher_K. (** Proof-irrelevance on subsets of decidable sets *) @@ -300,7 +301,7 @@ Module DecidableEqDepSet (M:DecidableSet). Lemma inj_pair2 : forall (P:U -> Type) (p:U) (x y:P p), - existS P p x = existS P p y -> x = y. + existT P p x = existT P p y -> x = y. Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq. (** Injectivity of equality on dependent pairs with second component diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v new file mode 100644 index 00000000..9cbf756d --- /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-2012 *) +(* \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..ecb7428e 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-2012 *) (* \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..1dce51b2 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-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,7 +46,7 @@ Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF). Proof. intros i y. apply y. -unfold le, WF, induct in |- *. +unfold le, WF, induct. apply p2p2. intros x H0. apply y. @@ -55,7 +55,7 @@ Qed. Lemma lemma1 : induct (fun u => p2b (I u)). Proof. -unfold induct in |- *. +unfold induct. intros x p. apply (p2p2 (I x)). intro q. diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index afca2ee1..5424eea8 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-2012 *) (* \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..530e0555 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-2012 *) (* \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..7d6d0cf8 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-2012 *) (* \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..2e9f0c19 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-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -25,7 +25,7 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. - intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=refl_equal p). + intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=eq_refl p). reflexivity. Qed. End Eq_rect_eq. diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 25d07fc9..efec03d4 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-2012 *) (* \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..c0a6f9ed 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-2012 *) (* \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). |