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, 0 insertions, 1662 deletions
diff --git a/theories7/Logic/Berardi.v b/theories7/Logic/Berardi.v deleted file mode 100644 index db9007ec..00000000 --- a/theories7/Logic/Berardi.v +++ /dev/null @@ -1,170 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 5b7e002a..00000000 --- a/theories7/Logic/ChoiceFacts.v +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100755 index 8d7fe1d1..00000000 --- a/theories7/Logic/Classical.v +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 5419e958..00000000 --- a/theories7/Logic/ClassicalChoice.v +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 85700c22..00000000 --- a/theories7/Logic/ClassicalDescription.v +++ /dev/null @@ -1,76 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 1d37652e..00000000 --- a/theories7/Logic/ClassicalFacts.v +++ /dev/null @@ -1,214 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100755 index b1c26e6d..00000000 --- a/theories7/Logic/Classical_Pred_Set.v +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100755 index 69175ec7..00000000 --- a/theories7/Logic/Classical_Pred_Type.v +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100755 index 1dc7ec57..00000000 --- a/theories7/Logic/Classical_Prop.v +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100755 index e34170cd..00000000 --- a/theories7/Logic/Classical_Type.v +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 537b5e88..00000000 --- a/theories7/Logic/Decidable.v +++ /dev/null @@ -1,58 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 9f5f91a0..00000000 --- a/theories7/Logic/Diaconescu.v +++ /dev/null @@ -1,133 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100755 index fc2dfe52..00000000 --- a/theories7/Logic/Eqdep.v +++ /dev/null @@ -1,183 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 959395e3..00000000 --- a/theories7/Logic/Eqdep_dec.v +++ /dev/null @@ -1,149 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 066e51aa..00000000 --- a/theories7/Logic/Hurkens.v +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 38dfa5e6..00000000 --- a/theories7/Logic/JMeq.v +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index 3f031ff7..00000000 --- a/theories7/Logic/ProofIrrelevance.v +++ /dev/null @@ -1,113 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index e61f3582..00000000 --- a/theories7/Logic/RelationalChoice.v +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* 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')))). |