diff options
Diffstat (limited to 'theories7/Logic')
| -rw-r--r-- | theories7/Logic/Berardi.v | 170 | ||||
| -rw-r--r-- | theories7/Logic/ChoiceFacts.v | 134 | ||||
| -rwxr-xr-x | theories7/Logic/Classical.v | 14 | ||||
| -rw-r--r-- | theories7/Logic/ClassicalChoice.v | 31 | ||||
| -rw-r--r-- | theories7/Logic/ClassicalDescription.v | 76 | ||||
| -rw-r--r-- | theories7/Logic/ClassicalFacts.v | 214 | ||||
| -rwxr-xr-x | theories7/Logic/Classical_Pred_Set.v | 64 | ||||
| -rwxr-xr-x | theories7/Logic/Classical_Pred_Type.v | 64 | ||||
| -rwxr-xr-x | theories7/Logic/Classical_Prop.v | 85 | ||||
| -rwxr-xr-x | theories7/Logic/Classical_Type.v | 14 | ||||
| -rw-r--r-- | theories7/Logic/Decidable.v | 58 | ||||
| -rw-r--r-- | theories7/Logic/Diaconescu.v | 133 | ||||
| -rwxr-xr-x | theories7/Logic/Eqdep.v | 183 | ||||
| -rw-r--r-- | theories7/Logic/Eqdep_dec.v | 149 | ||||
| -rw-r--r-- | theories7/Logic/Hurkens.v | 79 | ||||
| -rw-r--r-- | theories7/Logic/JMeq.v | 64 | ||||
| -rw-r--r-- | theories7/Logic/ProofIrrelevance.v | 113 | ||||
| -rw-r--r-- | theories7/Logic/RelationalChoice.v | 17 |
18 files changed, 1662 insertions, 0 deletions
diff --git a/theories7/Logic/Berardi.v b/theories7/Logic/Berardi.v new file mode 100644 index 00000000..db9007ec --- /dev/null +++ b/theories7/Logic/Berardi.v @@ -0,0 +1,170 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Berardi.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** This file formalizes Berardi's paradox which says that in + the calculus of constructions, excluded middle (EM) and axiom of + choice (AC) implie proof irrelevenace (PI). + Here, the axiom of choice is not necessary because of the use + of inductive types. +<< +@article{Barbanera-Berardi:JFP96, + author = {F. Barbanera and S. Berardi}, + title = {Proof-irrelevance out of Excluded-middle and Choice + in the Calculus of Constructions}, + journal = {Journal of Functional Programming}, + year = {1996}, + volume = {6}, + number = {3}, + pages = {519-525} +} +>> *) + +Set Implicit Arguments. + +Section Berardis_paradox. + +(** Excluded middle *) +Hypothesis EM : (P:Prop) P \/ ~P. + +(** Conditional on any proposition. *) +Definition IFProp := [P,B:Prop][e1,e2:P] + Cases (EM B) of + (or_introl _) => e1 + | (or_intror _) => e2 + end. + +(** Axiom of choice applied to disjunction. + Provable in Coq because of dependent elimination. *) +Lemma AC_IF : (P,B:Prop)(e1,e2:P)(Q:P->Prop) + ( B -> (Q e1))-> + (~B -> (Q e2))-> + (Q (IFProp B e1 e2)). +Proof. +Intros P B e1 e2 Q p1 p2. +Unfold IFProp. +Case (EM B); Assumption. +Qed. + + +(** We assume a type with two elements. They play the role of booleans. + The main theorem under the current assumptions is that [T=F] *) +Variable Bool: Prop. +Variable T: Bool. +Variable F: Bool. + +(** The powerset operator *) +Definition pow [P:Prop] :=P->Bool. + + +(** A piece of theory about retracts *) +Section Retracts. + +Variable A,B: Prop. + +Record retract : Prop := { + i: A->B; + j: B->A; + inv: (a:A)(j (i a))==a + }. + +Record retract_cond : Prop := { + i2: A->B; + j2: B->A; + inv2: retract -> (a:A)(j2 (i2 a))==a + }. + + +(** The dependent elimination above implies the axiom of choice: *) +Lemma AC: (r:retract_cond) retract -> (a:A)((j2 r) ((i2 r) a))==a. +Proof. +Intros r. +Case r; Simpl. +Trivial. +Qed. + +End Retracts. + +(** This lemma is basically a commutation of implication and existential + quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) + which is provable in classical logic ( => is already provable in + intuitionnistic logic). *) + +Lemma L1 : (A,B:Prop)(retract_cond (pow A) (pow B)). +Proof. +Intros A B. +Elim (EM (retract (pow A) (pow B))). +Intros (f0, g0, e). +Exists f0 g0. +Trivial. + +Intros hf. +Exists ([x:(pow A); y:B]F) ([x:(pow B); y:A]F). +Intros; Elim hf; Auto. +Qed. + + +(** The paradoxical set *) +Definition U := (P:Prop)(pow P). + +(** Bijection between [U] and [(pow U)] *) +Definition f : U -> (pow U) := + [u](u U). + +Definition g : (pow U) -> U := + [h,X] + let lX = (j2 (L1 X U)) in + let rU = (i2 (L1 U U)) in + (lX (rU h)). + +(** We deduce that the powerset of [U] is a retract of [U]. + This lemma is stated in Berardi's article, but is not used + afterwards. *) +Lemma retract_pow_U_U : (retract (pow U) U). +Proof. +Exists g f. +Intro a. +Unfold f g; Simpl. +Apply AC. +Exists ([x:(pow U)]x) ([x:(pow U)]x). +Trivial. +Qed. + +(** Encoding of Russel's paradox *) + +(** The boolean negation. *) +Definition Not_b := [b:Bool](IFProp b==T F T). + +(** the set of elements not belonging to itself *) +Definition R : U := (g ([u:U](Not_b (u U u)))). + + +Lemma not_has_fixpoint : (R R)==(Not_b (R R)). +Proof. +Unfold 1 R. +Unfold g. +Rewrite AC with r:=(L1 U U) a:=[u:U](Not_b (u U u)). +Trivial. +Exists ([x:(pow U)]x) ([x:(pow U)]x); Trivial. +Qed. + + +Theorem classical_proof_irrelevence : T==F. +Proof. +Generalize not_has_fixpoint. +Unfold Not_b. +Apply AC_IF. +Intros is_true is_false. +Elim is_true; Elim is_false; Trivial. + +Intros not_true is_true. +Elim not_true; Trivial. +Qed. + +End Berardis_paradox. diff --git a/theories7/Logic/ChoiceFacts.v b/theories7/Logic/ChoiceFacts.v new file mode 100644 index 00000000..5b7e002a --- /dev/null +++ b/theories7/Logic/ChoiceFacts.v @@ -0,0 +1,134 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ChoiceFacts.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(* We show that the functional formulation of the axiom of Choice + (usual formulation in type theory) is equivalent to its relational + formulation (only formulation of set theory) + the axiom of + (parametric) definite description (aka axiom of unique choice) *) + +(* This shows that the axiom of choice can be assumed (under its + relational formulation) without known inconsistency with classical logic, + though definite description conflicts with classical logic *) + +Definition RelationalChoice := + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) + -> (EXT R':A->B->Prop | + ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))). + +Definition FunctionalChoice := + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) -> (EX f:A->B | (x:A)(R x (f x))). + +Definition ParamDefiniteDescription := + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y'))) + -> (EX f:A->B | (x:A)(R x (f x))). + +Lemma description_rel_choice_imp_funct_choice : + ParamDefiniteDescription->RelationalChoice->FunctionalChoice. +Intros Descr RelCh. +Red; Intros A B R H. +NewDestruct (RelCh A B R H) as [R' H0]. +NewDestruct (Descr A B R') as [f H1]. +Intro x. +Elim (H0 x); Intros y [H2 [H3 H4]]; Exists y; Split; [Exact H3 | Exact H4]. +Exists f; Intro x. +Elim (H0 x); Intros y [H2 [H3 H4]]. +Rewrite <- (H4 (f x) (H1 x)). +Exact H2. +Qed. + +Lemma funct_choice_imp_rel_choice : + FunctionalChoice->RelationalChoice. +Intros FunCh. +Red; Intros A B R H. +NewDestruct (FunCh A B R H) as [f H0]. +Exists [x,y]y=(f x). +Intro x; Exists (f x); +Split; [Apply H0| Split;[Reflexivity| Intros y H1; Symmetry; Exact H1]]. +Qed. + +Lemma funct_choice_imp_description : + FunctionalChoice->ParamDefiniteDescription. +Intros FunCh. +Red; Intros A B R H. +NewDestruct (FunCh A B R) as [f H0]. +(* 1 *) +Intro x. +Elim (H x); Intros y [H0 H1]. +Exists y; Exact H0. +(* 2 *) +Exists f; Exact H0. +Qed. + +Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr : + FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription. +Split. +Intro H; Split; [ + Exact (funct_choice_imp_rel_choice H) + | Exact (funct_choice_imp_description H)]. +Intros [H H0]; Exact (description_rel_choice_imp_funct_choice H0 H). +Qed. + +(* We show that the guarded relational formulation of the axiom of Choice + comes from the non guarded formulation in presence either of the + independance of premises or proof-irrelevance *) + +Definition GuardedRelationalChoice := + (A:Type;B:Type;P:A->Prop;R: A->B->Prop) + ((x:A)(P x)->(EX y:B|(R x y))) + -> (EXT R':A->B->Prop | + ((x:A)(P x)->(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))). + +Definition ProofIrrelevance := (A:Prop)(a1,a2:A) a1==a2. + +Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : + RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice. +Proof. +Intros rel_choice proof_irrel. +Red; Intros A B P R H. +NewDestruct (rel_choice ? ? [x:(sigT ? P);y:B](R (projT1 ? ? x) y)) as [R' H0]. +Intros [x HPx]. +NewDestruct (H x HPx) as [y HRxy]. +Exists y; Exact HRxy. +Pose R'':=[x:A;y:B](EXT H:(P x) | (R' (existT ? P x H) y)). +Exists R''; Intros x HPx. +NewDestruct (H0 (existT ? P x HPx)) as [y [HRxy [HR'xy Huniq]]]. +Exists y. Split. + Exact HRxy. + Split. + Red; Exists HPx; Exact HR'xy. + Intros y' HR''xy'. + Apply Huniq. + Unfold R'' in HR''xy'. + NewDestruct HR''xy' as [H'Px HR'xy']. + Rewrite proof_irrel with a1:=HPx a2:=H'Px. + Exact HR'xy'. +Qed. + +Definition IndependenceOfPremises := + (A:Type)(P:A->Prop)(Q:Prop)(Q->(EXT x|(P x)))->(EXT x|Q->(P x)). + +Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice : + RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice. +Proof. +Intros RelCh IndPrem. +Red; Intros A B P R H. +NewDestruct (RelCh A B [x,y](P x)->(R x y)) as [R' H0]. + Intro x. Apply IndPrem. + Apply H. + Exists R'. + Intros x HPx. + NewDestruct (H0 x) as [y [H1 H2]]. + Exists y. Split. + Apply (H1 HPx). + Exact H2. +Qed. diff --git a/theories7/Logic/Classical.v b/theories7/Logic/Classical.v new file mode 100755 index 00000000..8d7fe1d1 --- /dev/null +++ b/theories7/Logic/Classical.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Classical.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Classical Logic *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Type. diff --git a/theories7/Logic/ClassicalChoice.v b/theories7/Logic/ClassicalChoice.v new file mode 100644 index 00000000..5419e958 --- /dev/null +++ b/theories7/Logic/ClassicalChoice.v @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ClassicalChoice.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** This file provides classical logic and functional choice *) + +(** This file extends ClassicalDescription.v with the axiom of choice. + As ClassicalDescription.v, it implies the double-negation of + excluded-middle in Set and implies a strongly classical + world. Especially it conflicts with impredicativity of Set, knowing + that true<>false in Set. +*) + +Require Export ClassicalDescription. +Require Export RelationalChoice. +Require ChoiceFacts. + +Theorem choice : + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) -> (EX f:A->B | (x:A)(R x (f x))). +Proof. +Apply description_rel_choice_imp_funct_choice. +Exact description. +Exact relational_choice. +Qed. diff --git a/theories7/Logic/ClassicalDescription.v b/theories7/Logic/ClassicalDescription.v new file mode 100644 index 00000000..85700c22 --- /dev/null +++ b/theories7/Logic/ClassicalDescription.v @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ClassicalDescription.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** This file provides classical logic and definite description *) + +(** Classical logic and definite description, as shown in [1], + implies the double-negation of excluded-middle in Set, hence it + implies a strongly classical world. Especially it conflicts with + impredicativity of Set, knowing that true<>false in Set. + + [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical + Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, + Lecture Notes in Computer Science 2646, Springer Verlag. +*) + +Require Export Classical. + +Axiom dependent_description : + (A:Type;B:A->Type;R: (x:A)(B x)->Prop) + ((x:A)(EX y:(B x)|(R x y)/\ ((y':(B x))(R x y') -> y=y'))) + -> (EX f:(x:A)(B x) | (x:A)(R x (f x))). + +(** Principle of definite descriptions (aka axiom of unique choice) *) + +Theorem description : + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y'))) + -> (EX f:A->B | (x:A)(R x (f x))). +Proof. +Intros A B. +Apply (dependent_description A [_]B). +Qed. + +(** The followig proof comes from [1] *) + +Theorem classic_set : (((P:Prop){P}+{~P}) -> False) -> False. +Proof. +Intro HnotEM. +Pose R:=[A,b]A/\true=b \/ ~A/\false=b. +Assert H:(EX f:Prop->bool|(A:Prop)(R A (f A))). +Apply description. +Intro A. +NewDestruct (classic A) as [Ha|Hnota]. + Exists true; Split. + Left; Split; [Assumption|Reflexivity]. + Intros y [[_ Hy]|[Hna _]]. + Assumption. + Contradiction. + Exists false; Split. + Right; Split; [Assumption|Reflexivity]. + Intros y [[Ha _]|[_ Hy]]. + Contradiction. + Assumption. +NewDestruct H as [f Hf]. +Apply HnotEM. +Intro P. +Assert HfP := (Hf P). +(* Elimination from Hf to Set is not allowed but from f to Set yes ! *) +NewDestruct (f P). + Left. + NewDestruct HfP as [[Ha _]|[_ Hfalse]]. + Assumption. + Discriminate. + Right. + NewDestruct HfP as [[_ Hfalse]|[Hna _]]. + Discriminate. + Assumption. +Qed. + diff --git a/theories7/Logic/ClassicalFacts.v b/theories7/Logic/ClassicalFacts.v new file mode 100644 index 00000000..1d37652e --- /dev/null +++ b/theories7/Logic/ClassicalFacts.v @@ -0,0 +1,214 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ClassicalFacts.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Some facts and definitions about classical logic *) + +(** [prop_degeneracy] (also referred as propositional completeness) *) +(* asserts (up to consistency) that there are only two distinct formulas *) +Definition prop_degeneracy := (A:Prop) A==True \/ A==False. + +(** [prop_extensionality] asserts equivalent formulas are equal *) +Definition prop_extensionality := (A,B:Prop) (A<->B) -> A==B. + +(** [excluded_middle] asserts we can reason by case on the truth *) +(* or falsity of any formula *) +Definition excluded_middle := (A:Prop) A \/ ~A. + +(** [proof_irrelevance] asserts equality of all proofs of a given formula *) +Definition proof_irrelevance := (A:Prop)(a1,a2:A) a1==a2. + +(** We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *) + +Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality. +Proof. +Intros H A B (Hab,Hba). +NewDestruct (H A); NewDestruct (H B). + Rewrite H1; Exact H0. + Absurd B. + Rewrite H1; Exact [H]H. + Apply Hab; Rewrite H0; Exact I. + Absurd A. + Rewrite H0; Exact [H]H. + Apply Hba; Rewrite H1; Exact I. + Rewrite H1; Exact H0. +Qed. + +Lemma prop_degen_em : prop_degeneracy -> excluded_middle. +Proof. +Intros H A. +NewDestruct (H A). + Left; Rewrite H0; Exact I. + Right; Rewrite H0; Exact [x]x. +Qed. + +Lemma prop_ext_em_degen : + prop_extensionality -> excluded_middle -> prop_degeneracy. +Proof. +Intros Ext EM A. +NewDestruct (EM A). + Left; Apply (Ext A True); Split; [Exact [_]I | Exact [_]H]. + Right; Apply (Ext A False); Split; [Exact H | Apply False_ind]. +Qed. + +(** We successively show that: + + [prop_extensionality] + implies equality of [A] and [A->A] for inhabited [A], which + implies the existence of a (trivial) retract from [A->A] to [A] + (just take the identity), which + implies the existence of a fixpoint operator in [A] + (e.g. take the Y combinator of lambda-calculus) +*) + +Definition inhabited [A:Prop] := A. + +Lemma prop_ext_A_eq_A_imp_A : + prop_extensionality->(A:Prop)(inhabited A)->(A->A)==A. +Proof. +Intros Ext A a. +Apply (Ext A->A A); Split; [ Exact [_]a | Exact [_;_]a ]. +Qed. + +Record retract [A,B:Prop] : Prop := { + f1: A->B; + f2: B->A; + f1_o_f2: (x:B)(f1 (f2 x))==x +}. + +Lemma prop_ext_retract_A_A_imp_A : + prop_extensionality->(A:Prop)(inhabited A)->(retract A A->A). +Proof. +Intros Ext A a. +Rewrite -> (prop_ext_A_eq_A_imp_A Ext A a). +Exists [x:A]x [x:A]x. +Reflexivity. +Qed. + +Record has_fixpoint [A:Prop] : Prop := { + F : (A->A)->A; + fix : (f:A->A)(F f)==(f (F f)) +}. + +Lemma ext_prop_fixpoint : + prop_extensionality->(A:Prop)(inhabited A)->(has_fixpoint A). +Proof. +Intros Ext A a. +Case (prop_ext_retract_A_A_imp_A Ext A a); Intros g1 g2 g1_o_g2. +Exists [f]([x:A](f (g1 x x)) (g2 [x](f (g1 x x)))). +Intro f. +Pattern 1 (g1 (g2 [x:A](f (g1 x x)))). +Rewrite (g1_o_g2 [x:A](f (g1 x x))). +Reflexivity. +Qed. + +(** Assume we have booleans with the property that there is at most 2 + booleans (which is equivalent to dependent case analysis). Consider + the fixpoint of the negation function: it is either true or false by + dependent case analysis, but also the opposite by fixpoint. Hence + proof-irrelevance. + + We then map bool proof-irrelevance to all propositions. +*) + +Section Proof_irrelevance_gen. + +Variable bool : Prop. +Variable true : bool. +Variable false : bool. +Hypothesis bool_elim : (C:Prop)C->C->bool->C. +Hypothesis bool_elim_redl : (C:Prop)(c1,c2:C)c1==(bool_elim C c1 c2 true). +Hypothesis bool_elim_redr : (C:Prop)(c1,c2:C)c2==(bool_elim C c1 c2 false). +Local bool_dep_induction := (P:bool->Prop)(P true)->(P false)->(b:bool)(P b). + +Lemma aux : prop_extensionality -> bool_dep_induction -> true==false. +Proof. +Intros Ext Ind. +Case (ext_prop_fixpoint Ext bool true); Intros G Gfix. +Pose neg := [b:bool](bool_elim bool false true b). +Generalize (refl_eqT ? (G neg)). +Pattern 1 (G neg). +Apply Ind with b:=(G neg); Intro Heq. +Rewrite (bool_elim_redl bool false true). +Change true==(neg true); Rewrite -> Heq; Apply Gfix. +Rewrite (bool_elim_redr bool false true). +Change (neg false)==false; Rewrite -> Heq; Symmetry; Apply Gfix. +Qed. + +Lemma ext_prop_dep_proof_irrel_gen : + prop_extensionality -> bool_dep_induction -> proof_irrelevance. +Proof. +Intros Ext Ind A a1 a2. +Pose f := [b:bool](bool_elim A a1 a2 b). +Rewrite (bool_elim_redl A a1 a2). +Change (f true)==a2. +Rewrite (bool_elim_redr A a1 a2). +Change (f true)==(f false). +Rewrite (aux Ext Ind). +Reflexivity. +Qed. + +End Proof_irrelevance_gen. + +(** In the pure Calculus of Constructions, we can define the boolean + proposition bool = (C:Prop)C->C->C but we cannot prove that it has at + most 2 elements. +*) + +Section Proof_irrelevance_CC. + +Definition BoolP := (C:Prop)C->C->C. +Definition TrueP := [C][c1,c2]c1 : BoolP. +Definition FalseP := [C][c1,c2]c2 : BoolP. +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) + := [C;c1,c2](refl_eqT C c1). +Definition BoolP_elim_redr : (C:Prop)(c1,c2:C)c2==(BoolP_elim C c1 c2 FalseP) + := [C;c1,c2](refl_eqT C c2). + +Definition BoolP_dep_induction := + (P:BoolP->Prop)(P TrueP)->(P FalseP)->(b:BoolP)(P b). + +Lemma ext_prop_dep_proof_irrel_cc : + prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. +Proof (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim + BoolP_elim_redl BoolP_elim_redr). + +End Proof_irrelevance_CC. + +(** In the Calculus of Inductive Constructions, inductively defined booleans + enjoy dependent case analysis, hence directly proof-irrelevance from + propositional extensionality. +*) + +Section Proof_irrelevance_CIC. + +Inductive boolP : Prop := trueP : boolP | falseP : boolP. +Definition boolP_elim_redl : (C:Prop)(c1,c2:C)c1==(boolP_ind C c1 c2 trueP) + := [C;c1,c2](refl_eqT C c1). +Definition boolP_elim_redr : (C:Prop)(c1,c2:C)c2==(boolP_ind C c1 c2 falseP) + := [C;c1,c2](refl_eqT C c2). +Scheme boolP_indd := Induction for boolP Sort Prop. + +Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. +Proof [pe](ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind + boolP_elim_redl boolP_elim_redr pe boolP_indd). + +End Proof_irrelevance_CIC. + +(** Can we state proof irrelevance from propositional degeneracy + (i.e. propositional extensionality + excluded middle) without + dependent case analysis ? + + Conjecture: it seems possible to build a model of CC interpreting + all non-empty types by the set of all lambda-terms. Such a model would + satisfy propositional degeneracy without satisfying proof-irrelevance + (nor dependent case analysis). This would imply that the previous + results cannot be refined. +*) diff --git a/theories7/Logic/Classical_Pred_Set.v b/theories7/Logic/Classical_Pred_Set.v new file mode 100755 index 00000000..b1c26e6d --- /dev/null +++ b/theories7/Logic/Classical_Pred_Set.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Classical_Pred_Set.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Classical Predicate Logic on Set*) + +Require Classical_Prop. + +Section Generic. +Variable U: Set. + +(** de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EX n:U | ~(P n)). +Proof. +Unfold not; Intros P notall. +Apply NNPP; Unfold not. +Intro abs. +Cut ((n:U)(P n)); Auto. +Intro n; Apply NNPP. +Unfold not; Intros. +Apply abs; Exists n; Trivial. +Qed. + +Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EX n:U |(P n)). +Proof. +Intros P H. +Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n. +Apply NNPP; Trivial. +Qed. + +Lemma not_ex_all_not : (P:U->Prop) (~(EX n:U |(P n))) -> (n:U)~(P n). +Proof. +Unfold not; Intros P notex n abs. +Apply notex. +Exists n; Trivial. +Qed. + +Lemma not_ex_not_all : (P:U->Prop)(~(EX n:U | ~(P n))) -> (n:U)(P n). +Proof. +Intros P H n. +Apply NNPP. +Red; Intro K; Apply H; Exists n; Trivial. +Qed. + +Lemma ex_not_not_all : (P:U->Prop) (EX n:U | ~(P n)) -> ~(n:U)(P n). +Proof. +Unfold not; Intros P exnot allP. +Elim exnot; Auto. +Qed. + +Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EX n:U |(P n)). +Proof. +Unfold not; Intros P allnot exP; Elim exP; Intros n p. +Apply allnot with n; Auto. +Qed. + +End Generic. diff --git a/theories7/Logic/Classical_Pred_Type.v b/theories7/Logic/Classical_Pred_Type.v new file mode 100755 index 00000000..69175ec7 --- /dev/null +++ b/theories7/Logic/Classical_Pred_Type.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Classical_Pred_Type.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Classical Predicate Logic on Type *) + +Require Classical_Prop. + +Section Generic. +Variable U: Type. + +(** de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EXT n:U | ~(P n)). +Proof. +Unfold not; Intros P notall. +Apply NNPP; Unfold not. +Intro abs. +Cut ((n:U)(P n)); Auto. +Intro n; Apply NNPP. +Unfold not; Intros. +Apply abs; Exists n; Trivial. +Qed. + +Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EXT n:U | (P n)). +Proof. +Intros P H. +Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n. +Apply NNPP; Trivial. +Qed. + +Lemma not_ex_all_not : (P:U->Prop)(~(EXT n:U | (P n))) -> (n:U)~(P n). +Proof. +Unfold not; Intros P notex n abs. +Apply notex. +Exists n; Trivial. +Qed. + +Lemma not_ex_not_all : (P:U->Prop)(~(EXT n:U | ~(P n))) -> (n:U)(P n). +Proof. +Intros P H n. +Apply NNPP. +Red; Intro K; Apply H; Exists n; Trivial. +Qed. + +Lemma ex_not_not_all : (P:U->Prop) (EXT n:U | ~(P n)) -> ~(n:U)(P n). +Proof. +Unfold not; Intros P exnot allP. +Elim exnot; Auto. +Qed. + +Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EXT n:U | (P n)). +Proof. +Unfold not; Intros P allnot exP; Elim exP; Intros n p. +Apply allnot with n; Auto. +Qed. + +End Generic. diff --git a/theories7/Logic/Classical_Prop.v b/theories7/Logic/Classical_Prop.v new file mode 100755 index 00000000..1dc7ec57 --- /dev/null +++ b/theories7/Logic/Classical_Prop.v @@ -0,0 +1,85 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Classical_Prop.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Classical Propositional Logic *) + +Require ProofIrrelevance. + +Hints Unfold not : core. + +Axiom classic: (P:Prop)(P \/ ~(P)). + +Lemma NNPP : (p:Prop)~(~(p))->p. +Proof. +Unfold not; Intros; Elim (classic p); Auto. +Intro NP; Elim (H NP). +Qed. + +Lemma not_imply_elim : (P,Q:Prop)~(P->Q)->P. +Proof. +Intros; Apply NNPP; Red. +Intro; Apply H; Intro; Absurd P; Trivial. +Qed. + +Lemma not_imply_elim2 : (P,Q:Prop)~(P->Q) -> ~Q. +Proof. +Intros; Elim (classic Q); Auto. +Qed. + +Lemma imply_to_or : (P,Q:Prop)(P->Q) -> ~P \/ Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma imply_to_and : (P,Q:Prop)~(P->Q) -> P /\ ~Q. +Proof. +Intros; Split. +Apply not_imply_elim with Q; Trivial. +Apply not_imply_elim2 with P; Trivial. +Qed. + +Lemma or_to_imply : (P,Q:Prop)(~P \/ Q) -> P->Q. +Proof. +Induction 1; Auto. +Intros H1 H2; Elim (H1 H2). +Qed. + +Lemma not_and_or : (P,Q:Prop)~(P/\Q)-> ~P \/ ~Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma or_not_and : (P,Q:Prop)(~P \/ ~Q) -> ~(P/\Q). +Proof. +Induction 1; Red; Induction 2; Auto. +Qed. + +Lemma not_or_and : (P,Q:Prop)~(P\/Q)-> ~P /\ ~Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma and_not_or : (P,Q:Prop)(~P /\ ~Q) -> ~(P\/Q). +Proof. +Induction 1; Red; Induction 3; Trivial. +Qed. + +Lemma imply_and_or: (P,Q:Prop)(P->Q) -> P \/ Q -> Q. +Proof. +Induction 2; Trivial. +Qed. + +Lemma imply_and_or2: (P,Q,R:Prop)(P->Q) -> P \/ R -> Q \/ R. +Proof. +Induction 2; Auto. +Qed. + +Lemma proof_irrelevance: (P:Prop)(p1,p2:P)p1==p2. +Proof (proof_irrelevance_cci classic). diff --git a/theories7/Logic/Classical_Type.v b/theories7/Logic/Classical_Type.v new file mode 100755 index 00000000..e34170cd --- /dev/null +++ b/theories7/Logic/Classical_Type.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Classical_Type.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Classical Logic for Type *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Type. diff --git a/theories7/Logic/Decidable.v b/theories7/Logic/Decidable.v new file mode 100644 index 00000000..537b5e88 --- /dev/null +++ b/theories7/Logic/Decidable.v @@ -0,0 +1,58 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(*i $Id: Decidable.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Properties of decidable propositions *) + +Definition decidable := [P:Prop] P \/ ~P. + +Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P. +Unfold decidable; Tauto. +Qed. + +Theorem dec_True: (decidable True). +Unfold decidable; Auto. +Qed. + +Theorem dec_False: (decidable False). +Unfold decidable not; Auto. +Qed. + +Theorem dec_or: (A,B:Prop)(decidable A) -> (decidable B) -> (decidable (A\/B)). +Unfold decidable; Tauto. +Qed. + +Theorem dec_and: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A/\B)). +Unfold decidable; Tauto. +Qed. + +Theorem dec_not: (A:Prop)(decidable A) -> (decidable ~A). +Unfold decidable; Tauto. +Qed. + +Theorem dec_imp: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A->B)). +Unfold decidable; Tauto. +Qed. + +Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P. +Unfold decidable; Tauto. Qed. + +Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B. +Tauto. Qed. + +Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B. +Unfold decidable; Tauto. Qed. + +Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B. +Unfold decidable;Tauto. +Qed. + +Theorem imp_simp : (A,B:Prop) (decidable A) -> (A -> B) -> ~A \/ B. +Unfold decidable; Tauto. +Qed. + diff --git a/theories7/Logic/Diaconescu.v b/theories7/Logic/Diaconescu.v new file mode 100644 index 00000000..9f5f91a0 --- /dev/null +++ b/theories7/Logic/Diaconescu.v @@ -0,0 +1,133 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Diaconescu.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory + entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner] + adapted the proof to show that the axiom of choice in equivalence + classes entails Excluded-Middle in Type Theory. + + This is an adaptatation of the proof by Hugo Herbelin to show that + the relational form of the Axiom of Choice + Extensionality for + predicates entails Excluded-Middle + + [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in + Proceedings of AMS, vol 51, pp 176-178, 1975. + + [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?, + preprint, 1999. + +*) + +Section PredExt_GuardRelChoice_imp_EM. + +(* The axiom of extensionality for predicates *) + +Definition PredicateExtensionality := + (P,Q:bool->Prop)((b:bool)(P b)<->(Q b))->P==Q. + +(* From predicate extensionality we get propositional extensionality + hence proof-irrelevance *) + +Require ClassicalFacts. + +Variable pred_extensionality : PredicateExtensionality. + +Lemma prop_ext : (A,B:Prop) (A<->B) -> A==B. +Proof. + Intros A B H. + Change ([_]A true)==([_]B true). + Rewrite pred_extensionality with P:=[_:bool]A Q:=[_:bool]B. + Reflexivity. + Intros _; Exact H. +Qed. + +Lemma proof_irrel : (A:Prop)(a1,a2:A) a1==a2. +Proof. + Apply (ext_prop_dep_proof_irrel_cic prop_ext). +Qed. + +(* From proof-irrelevance and relational choice, we get guarded + relational choice *) + +Require ChoiceFacts. + +Variable rel_choice : RelationalChoice. + +Lemma guarded_rel_choice : + (A:Type)(B:Type)(P:A->Prop)(R:A->B->Prop) + ((x:A)(P x)->(EX y:B|(R x y)))-> + (EXT R':A->B->Prop | + ((x:A)(P x)->(EX y:B|(R x y)/\(R' x y)/\ ((y':B)(R' x y') -> y=y')))). +Proof. + Exact + (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). +Qed. + +(* The form of choice we need: there is a functional relation which chooses + an element in any non empty subset of bool *) + +Require Bool. + +Lemma AC : + (EXT R:(bool->Prop)->bool->Prop | + (P:bool->Prop)(EX b : bool | (P b))-> + (EX b : bool | (P b) /\ (R P b) /\ ((b':bool)(R P b')->b=b'))). +Proof. + Apply guarded_rel_choice with + P:= [Q:bool->Prop](EX y | (Q y)) R:=[Q:bool->Prop;y:bool](Q y). + Exact [_;H]H. +Qed. + +(* The proof of the excluded middle *) +(* Remark: P could have been in Set or Type *) + +Theorem pred_ext_and_rel_choice_imp_EM : (P:Prop)P\/~P. +Proof. +Intro P. + +(* first we exhibit the choice functional relation R *) +NewDestruct AC as [R H]. + +Pose class_of_true := [b]b=true\/P. +Pose class_of_false := [b]b=false\/P. + +(* the actual "decision": is (R class_of_true) = true or false? *) +NewDestruct (H class_of_true) as [b0 [H0 [H0' H0'']]]. +Exists true; Left; Reflexivity. +NewDestruct H0. + +(* the actual "decision": is (R class_of_false) = true or false? *) +NewDestruct (H class_of_false) as [b1 [H1 [H1' H1'']]]. +Exists false; Left; Reflexivity. +NewDestruct H1. + +(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *) +Right. +Intro HP. +Assert Hequiv:(b:bool)(class_of_true b)<->(class_of_false b). +Intro b; Split. +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. +Rewrite <- H0. +Rewrite <- H1. +Rewrite <- H0''. Reflexivity. +Rewrite Heq. +Assumption. + +(* cases where P is true *) +Left; Assumption. +Left; Assumption. + +Qed. + +End PredExt_GuardRelChoice_imp_EM. diff --git a/theories7/Logic/Eqdep.v b/theories7/Logic/Eqdep.v new file mode 100755 index 00000000..fc2dfe52 --- /dev/null +++ b/theories7/Logic/Eqdep.v @@ -0,0 +1,183 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Eqdep.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** This file defines dependent equality and shows its equivalence with + equality on dependent pairs (inhabiting sigma-types). It axiomatizes + the invariance by substitution of reflexive equality proofs and + shows the equivalence between the 4 following statements + + - Invariance by Substitution of Reflexive Equality Proofs. + - Injectivity of Dependent Equality + - Uniqueness of Identity Proofs + - Uniqueness of Reflexive Identity Proofs + - Streicher's Axiom K + + These statements are independent of the calculus of constructions [2]. + + References: + + [1] T. Streicher, Semantical Investigations into Intensional Type Theory, + Habilitationsschrift, LMU München, 1993. + [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, + Proceedings of the meeting Twenty-five years of constructive + type theory, Venice, Oxford University Press, 1998 +*) + +Section Dependent_Equality. + +Variable U : Type. +Variable P : U->Type. + +(** Dependent equality *) + +Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop := + eq_dep_intro : (eq_dep p x p x). +Hint constr_eq_dep : core v62 := Constructors eq_dep. + +Lemma eq_dep_sym : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep q y p x). +Proof. +NewDestruct 1; Auto. +Qed. +Hints Immediate eq_dep_sym : core v62. + +Lemma eq_dep_trans : (p,q,r:U)(x:(P p))(y:(P q))(z:(P r)) + (eq_dep p x q y)->(eq_dep q y r z)->(eq_dep p x r z). +Proof. +NewDestruct 1; Auto. +Qed. + +Inductive eq_dep1 [p:U;x:(P p);q:U;y:(P q)] : Prop := + eq_dep1_intro : (h:q=p) + (x=(eq_rect U q P y p h))->(eq_dep1 p x q y). + +Scheme eq_indd := Induction for eq Sort Prop. + +Lemma eq_dep1_dep : + (p:U)(x:(P p))(q:U)(y:(P q))(eq_dep1 p x q y)->(eq_dep p x q y). +Proof. +NewDestruct 1 as [eq_qp H]. +NewDestruct eq_qp using eq_indd. +Rewrite H. +Apply eq_dep_intro. +Qed. + +Lemma eq_dep_dep1 : + (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y). +Proof. +NewDestruct 1. +Apply eq_dep1_intro with (refl_equal U p). +Simpl; Trivial. +Qed. + +(** Invariance by Substitution of Reflexive Equality Proofs *) + +Axiom eq_rect_eq : (p:U)(Q:U->Type)(x:(Q p))(h:p=p) + x=(eq_rect U p Q x p h). + +(** Injectivity of Dependent Equality is a consequence of *) +(** Invariance by Substitution of Reflexive Equality Proof *) + +Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y. +Proof. +Destruct 1; Intro. +Rewrite <- eq_rect_eq; Auto. +Qed. + +Lemma eq_dep_eq : (p:U)(x,y:(P p))(eq_dep p x p y)->x=y. +Proof. +Intros; Apply eq_dep1_eq; Apply eq_dep_dep1; Trivial. +Qed. + +End Dependent_Equality. + +(** Uniqueness of Identity Proofs (UIP) is a consequence of *) +(** Injectivity of Dependent Equality *) + +Lemma UIP : (U:Type)(x,y:U)(p1,p2:x=y)p1=p2. +Proof. +Intros; Apply eq_dep_eq with P:=[y]x=y. +Elim p2 using eq_indd. +Elim p1 using eq_indd. +Apply eq_dep_intro. +Qed. + +(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *) + +Lemma UIP_refl : (U:Type)(x:U)(p:x=x)p=(refl_equal U x). +Proof. +Intros; Apply UIP. +Qed. + +(** Streicher axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + +Lemma Streicher_K : (U:Type)(x:U)(P:x=x->Prop) + (P (refl_equal ? x))->(p:x=x)(P p). +Proof. +Intros; Rewrite UIP_refl; Assumption. +Qed. + +(** We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *) + +Lemma eq_rec_eq : (U:Type)(P:U->Set)(p:U)(x:(P p))(h:p=p) + x=(eq_rec U p P x p h). +Proof. +Intros. +Apply Streicher_K with p:=h. +Reflexivity. +Qed. + +(** Dependent equality is equivalent to equality on dependent pairs *) + +Lemma equiv_eqex_eqdep : (U:Set)(P:U->Set)(p,q:U)(x:(P p))(y:(P q)) + (existS U P p x)=(existS U P q y) <-> (eq_dep U P p x q y). +Proof. +Split. +(* -> *) +Intro H. +Change p with (projS1 U P (existS U P p x)). +Change 2 x with (projS2 U P (existS U P p x)). +Rewrite H. +Apply eq_dep_intro. +(* <- *) +NewDestruct 1; Reflexivity. +Qed. + +(** UIP implies the injectivity of equality on dependent pairs *) + +Lemma inj_pair2: (U:Set)(P:U->Set)(p:U)(x,y:(P p)) + (existS U P p x)=(existS U P p y)-> x=y. +Proof. +Intros. +Apply (eq_dep_eq U P). +Generalize (equiv_eqex_eqdep U P p p x y) . +Induction 1. +Intros. +Auto. +Qed. + +(** UIP implies the injectivity of equality on dependent pairs *) + +Lemma inj_pairT2: (U:Type)(P:U->Type)(p:U)(x,y:(P p)) + (existT U P p x)=(existT U P p y)-> x=y. +Proof. +Intros. +Apply (eq_dep_eq U P). +Change 1 p with (projT1 U P (existT U P p x)). +Change 2 x with (projT2 U P (existT U P p x)). +Rewrite H. +Apply eq_dep_intro. +Qed. + +(** The main results to be exported *) + +Hints Resolve eq_dep_intro eq_dep_eq : core v62. +Hints Immediate eq_dep_sym : core v62. +Hints Resolve inj_pair2 inj_pairT2 : core. diff --git a/theories7/Logic/Eqdep_dec.v b/theories7/Logic/Eqdep_dec.v new file mode 100644 index 00000000..959395e3 --- /dev/null +++ b/theories7/Logic/Eqdep_dec.v @@ -0,0 +1,149 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Eqdep_dec.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** 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. + A corollary of this theorem is the equality of the right projections + of two equal dependent pairs. + + Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego + adapted to Coq by B. Barras + + Credit: Proofs up to [K_dec] follows an outline by Michael Hedberg +*) + + +(** We need some dependent elimination schemes *) + +Set Implicit Arguments. + + (** Bijection between [eq] and [eqT] *) + Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y := + [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end. + + Definition eqT2eq: (A:Set)(x,y:A)x==y->x=y := + [A,x,_,eqTxy]<[y:A]x=y>Cases eqTxy of refl_eqT => (refl_equal ? x) end. + + Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)). +Intros. +Case p; Reflexivity. +Qed. + + Lemma eqT_eq_bij: (A:Set)(x,y:A)(p:x==y)p==(eq2eqT (eqT2eq p)). +Intros. +Case p; Reflexivity. +Qed. + + +Section DecidableEqDep. + + Variable A: Type. + + Local comp [x,y,y':A]: x==y->x==y'->y==y' := + [eq1,eq2](eqT_ind ? ? [a]a==y' eq2 ? eq1). + + Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y). +Intros. +Case u; Trivial. +Qed. + + + + Variable eq_dec: (x,y:A) x==y \/ ~x==y. + + Variable x: A. + + + Local nu [y:A]: x==y->x==y := + [u]Cases (eq_dec x y) of + (or_introl eqxy) => eqxy + | (or_intror neqxy) => (False_ind ? (neqxy u)) + end. + + Local nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v). +Intros. +Unfold nu. +Case (eq_dec x y); Intros. +Reflexivity. + +Case n; Trivial. +Qed. + + + Local nu_inv [y:A]: x==y->x==y := [v](comp (nu (refl_eqT ? x)) v). + + + Remark nu_left_inv : (y:A)(u:x==y) (nu_inv (nu u))==u. +Intros. +Case u; Unfold nu_inv. +Apply trans_sym_eqT. +Qed. + + + Theorem eq_proofs_unicity: (y:A)(p1,p2:x==y) p1==p2. +Intros. +Elim nu_left_inv with u:=p1. +Elim nu_left_inv with u:=p2. +Elim nu_constant with y p1 p2. +Reflexivity. +Qed. + + Theorem K_dec: (P:x==x->Prop)(P (refl_eqT ? x)) -> (p:x==x)(P p). +Intros. +Elim eq_proofs_unicity with x (refl_eqT ? x) p. +Trivial. +Qed. + + + (** The corollary *) + + Local proj: (P:A->Prop)(ExT P)->(P x)->(P x) := + [P,exP,def]Cases exP of + (exT_intro x' prf) => + Cases (eq_dec x' x) of + (or_introl eqprf) => (eqT_ind ? x' P prf x eqprf) + | _ => def + end + end. + + + Theorem inj_right_pair: (P:A->Prop)(y,y':(P x)) + (exT_intro ? P x y)==(exT_intro ? P x y') -> y==y'. +Intros. +Cut (proj (exT_intro A P x y) y)==(proj (exT_intro A P x y') y). +Simpl. +Case (eq_dec x x). +Intro e. +Elim e using K_dec; Trivial. + +Intros. +Case n; Trivial. + +Case H. +Reflexivity. +Qed. + +End DecidableEqDep. + + (** We deduce the [K] axiom for (decidable) Set *) + Theorem K_dec_set: (A:Set)((x,y:A){x=y}+{~x=y}) + ->(x:A)(P: x=x->Prop)(P (refl_equal ? x)) + ->(p:x=x)(P p). +Intros. +Rewrite eq_eqT_bij. +Elim (eq2eqT p) using K_dec. +Intros. +Case (H x0 y); Intros. +Elim e; Left ; Reflexivity. + +Right ; Red; Intro neq; Apply n; Elim neq; Reflexivity. + +Trivial. +Qed. diff --git a/theories7/Logic/Hurkens.v b/theories7/Logic/Hurkens.v new file mode 100644 index 00000000..066e51aa --- /dev/null +++ b/theories7/Logic/Hurkens.v @@ -0,0 +1,79 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Hurkens.v *) +(************************************************************************) + +(** This is Hurkens paradox [Hurkens] in system U-, adapted by Herman + Geuvers [Geuvers] to show the inconsistency in the pure calculus of + constructions of a retract from Prop into a small type. + + References: + + - [Hurkens] A. J. Hurkens, "A simplification of Girard's paradox", + Proceedings of the 2nd international conference Typed Lambda-Calculi + and Applications (TLCA'95), 1995. + + - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001 + (see www.cs.kun.nl/~herman/note.ps.gz). +*) + +Section Paradox. + +Variable bool : Prop. +Variable p2b : Prop -> bool. +Variable b2p : bool -> Prop. +Hypothesis p2p1 : (A:Prop)(b2p (p2b A))->A. +Hypothesis p2p2 : (A:Prop)A->(b2p (p2b A)). +Variable B:Prop. + +Definition V := (A:Prop)((A->bool)->(A->bool))->(A->bool). +Definition U := V->bool. +Definition sb : V -> V := [z][A;r;a](r (z A r) a). +Definition le : (U->bool)->(U->bool) := [i][x](x [A;r;a](i [v](sb v A r a))). +Definition induct : (U->bool)->Prop := [i](x:U)(b2p (le i x))->(b2p (i x)). +Definition WF : U := [z](p2b (induct (z U le))). +Definition I : U->Prop := + [x]((i:U->bool)(b2p (le i x))->(b2p (i [v](sb v U le x))))->B. + +Lemma Omega : (i:U->bool)(induct i)->(b2p (i WF)). +Proof. +Intros i y. +Apply y. +Unfold le WF induct. +Apply p2p2. +Intros x H0. +Apply y. +Exact H0. +Qed. + +Lemma lemma1 : (induct [u](p2b (I u))). +Proof. +Unfold induct. +Intros x p. +Apply (p2p2 (I x)). +Intro q. +Apply (p2p1 (I [v:V](sb v U le x)) (q [u](p2b (I u)) p)). +Intro i. +Apply q with i:=[y:?](i [v:V](sb v U le y)). +Qed. + +Lemma lemma2 : ((i:U->bool)(induct i)->(b2p (i WF)))->B. +Proof. +Intro x. +Apply (p2p1 (I WF) (x [u](p2b (I u)) lemma1)). +Intros i H0. +Apply (x [y](i [v](sb v U le y))). +Apply (p2p1 ? H0). +Qed. + +Theorem paradox : B. +Proof. +Exact (lemma2 Omega). +Qed. + +End Paradox. diff --git a/theories7/Logic/JMeq.v b/theories7/Logic/JMeq.v new file mode 100644 index 00000000..38dfa5e6 --- /dev/null +++ b/theories7/Logic/JMeq.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: JMeq.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** John Major's Equality as proposed by C. Mc Bride *) + +Set Implicit Arguments. + +Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := + JMeq_refl : (JMeq x x). +Reset JMeq_ind. + +Hints Resolve JMeq_refl. + +Lemma sym_JMeq : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). +NewDestruct 1; Trivial. +Qed. + +Hints Immediate sym_JMeq. + +Lemma trans_JMeq : (A,B,C:Set)(x:A)(y:B)(z:C) + (JMeq x y)->(JMeq y z)->(JMeq x z). +NewDestruct 1; Trivial. +Qed. + +Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y). + +Lemma JMeq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y). +Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial. +Qed. + +Lemma JMeq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y). +Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial. +Qed. + +Lemma JMeq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x). +Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial. +Qed. + +Lemma JMeq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x). +Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial. +Qed. + +(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *) + +Require Eqdep. + +Lemma JMeq_eq_dep : (A,B:Set)(x:A)(y:B)(JMeq x y)->(eq_dep Set [X]X A x B y). +Proof. +NewDestruct 1. +Apply eq_dep_intro. +Qed. + +Lemma eq_dep_JMeq : (A,B:Set)(x:A)(y:B)(eq_dep Set [X]X A x B y)->(JMeq x y). +Proof. +NewDestruct 1. +Apply JMeq_refl. +Qed. diff --git a/theories7/Logic/ProofIrrelevance.v b/theories7/Logic/ProofIrrelevance.v new file mode 100644 index 00000000..3f031ff7 --- /dev/null +++ b/theories7/Logic/ProofIrrelevance.v @@ -0,0 +1,113 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This is a proof in the pure Calculus of Construction that + classical logic in Prop + dependent elimination of disjunction entails + proof-irrelevance. + + Since, dependent elimination is derivable in the Calculus of + Inductive Constructions (CCI), we get proof-irrelevance from classical + logic in the CCI. + + Reference: + + - [Coquand] T. Coquand, "Metamathematical Investigations of a + Calculus of Constructions", Proceedings of Logic in Computer Science + (LICS'90), 1990. + + Proof skeleton: classical logic + dependent elimination of + disjunction + discrimination of proofs implies the existence of a + retract from Prop into bool, hence inconsistency by encoding any + paradox of system U- (e.g. Hurkens' paradox). +*) + +Require Hurkens. + +Section Proof_irrelevance_CC. + +Variable or : Prop -> Prop -> Prop. +Variable or_introl : (A,B:Prop)A->(or A B). +Variable or_intror : (A,B:Prop)B->(or A B). +Hypothesis or_elim : (A,B:Prop)(C:Prop)(A->C)->(B->C)->(or A B)->C. +Hypothesis or_elim_redl : + (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(a:A) + (f a)==(or_elim A B C f g (or_introl A B a)). +Hypothesis or_elim_redr : + (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(b:B) + (g b)==(or_elim A B C f g (or_intror A B b)). +Hypothesis or_dep_elim : + (A,B:Prop)(P:(or A B)->Prop) + ((a:A)(P (or_introl A B a))) -> + ((b:B)(P (or_intror A B b))) -> (b:(or A B))(P b). + +Hypothesis em : (A:Prop)(or A ~A). +Variable B : Prop. +Variable b1,b2 : B. + +(** [p2b] and [b2p] form a retract if [~b1==b2] *) + +Definition p2b [A] := (or_elim A ~A B [_]b1 [_]b2 (em A)). +Definition b2p [b] := b1==b. + +Lemma p2p1 : (A:Prop) A -> (b2p (p2b A)). +Proof. + Unfold p2b; Intro A; Apply or_dep_elim with b:=(em A); Unfold b2p; Intros. + Apply (or_elim_redl A ~A B [_]b1 [_]b2). + NewDestruct (b H). +Qed. +Lemma p2p2 : ~b1==b2->(A:Prop) (b2p (p2b A)) -> A. +Proof. + Intro not_eq_b1_b2. + Unfold p2b; Intro A; Apply or_dep_elim with b:=(em A); Unfold b2p; Intros. + Assumption. + NewDestruct not_eq_b1_b2. + Rewrite <- (or_elim_redr A ~A B [_]b1 [_]b2) in H. + Assumption. +Qed. + +(** Using excluded-middle a second time, we get proof-irrelevance *) + +Theorem proof_irrelevance_cc : b1==b2. +Proof. + Refine (or_elim ? ? ? ? ? (em b1==b2));Intro H. + Trivial. + Apply (paradox B p2b b2p (p2p2 H) p2p1). +Qed. + +End Proof_irrelevance_CC. + + +(** The Calculus of Inductive Constructions (CCI) enjoys dependent + elimination, hence classical logic in CCI entails proof-irrelevance. +*) + +Section Proof_irrelevance_CCI. + +Hypothesis em : (A:Prop) A \/ ~A. + +Definition or_elim_redl : + (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(a:A) + (f a)==(or_ind A B C f g (or_introl A B a)) + := [A,B,C;f;g;a](refl_eqT C (f a)). +Definition or_elim_redr : + (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(b:B) + (g b)==(or_ind A B C f g (or_intror A B b)) + := [A,B,C;f;g;b](refl_eqT C (g b)). +Scheme or_indd := Induction for or Sort Prop. + +Theorem proof_irrelevance_cci : (B:Prop)(b1,b2:B)b1==b2. +Proof + (proof_irrelevance_cc or or_introl or_intror or_ind + or_elim_redl or_elim_redr or_indd em). + +End Proof_irrelevance_CCI. + +(** Remark: in CCI, [bool] can be taken in [Set] as well in the + paradox and since [~true=false] for [true] and [false] in + [bool], we get the inconsistency of [em : (A:Prop){A}+{~A}] in CCI +*) diff --git a/theories7/Logic/RelationalChoice.v b/theories7/Logic/RelationalChoice.v new file mode 100644 index 00000000..e61f3582 --- /dev/null +++ b/theories7/Logic/RelationalChoice.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: RelationalChoice.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(* This file axiomatizes the relational form of the axiom of choice *) + +Axiom relational_choice : + (A:Type;B:Type;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) + -> (EXT R':A->B->Prop | + ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))). |