diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Berardi.v | 159 | ||||
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 139 | ||||
| -rwxr-xr-x | theories/Logic/Classical.v | 14 | ||||
| -rw-r--r-- | theories/Logic/ClassicalChoice.v | 32 | ||||
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 78 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 219 | ||||
| -rwxr-xr-x | theories/Logic/Classical_Pred_Set.v | 70 | ||||
| -rwxr-xr-x | theories/Logic/Classical_Pred_Type.v | 70 | ||||
| -rwxr-xr-x | theories/Logic/Classical_Prop.v | 85 | ||||
| -rwxr-xr-x | theories/Logic/Classical_Type.v | 14 | ||||
| -rw-r--r-- | theories/Logic/Decidable.v | 60 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 138 | ||||
| -rwxr-xr-x | theories/Logic/Eqdep.v | 188 | ||||
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 158 | ||||
| -rw-r--r-- | theories/Logic/Hurkens.v | 81 | ||||
| -rw-r--r-- | theories/Logic/JMeq.v | 68 | ||||
| -rw-r--r-- | theories/Logic/ProofIrrelevance.v | 114 | ||||
| -rw-r--r-- | theories/Logic/RelationalChoice.v | 20 | ||||
| -rwxr-xr-x | theories/Logic/intro.tex | 8 |
19 files changed, 1715 insertions, 0 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v new file mode 100644 index 00000000..7e950c17 --- /dev/null +++ b/theories/Logic/Berardi.v @@ -0,0 +1,159 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:06 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 : forall P:Prop, P \/ ~ P. + +(** Conditional on any proposition. *) +Definition IFProp (P B:Prop) (e1 e2:P) := + match EM B with + | or_introl _ => e1 + | or_intror _ => e2 + end. + +(** Axiom of choice applied to disjunction. + Provable in Coq because of dependent elimination. *) +Lemma AC_IF : + forall (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 in |- *. +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. + +Variables A B : Prop. + +Record retract : Prop := + {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. + +Record retract_cond : Prop := + {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. + + +(** The dependent elimination above implies the axiom of choice: *) +Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. +Proof. +intros r. +case r; simpl in |- *. +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 : forall 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 (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F). +intros; elim hf; auto. +Qed. + + +(** The paradoxical set *) +Definition U := forall P:Prop, pow P. + +(** Bijection between [U] and [(pow U)] *) +Definition f (u:U) : pow U := u U. + +Definition g (h:pow U) : U := + fun 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 in |- *; simpl in |- *. +apply AC. +exists (fun x:pow U => x) (fun 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 (fun u:U => Not_b (u U u)). + + +Lemma not_has_fixpoint : R R = Not_b (R R). +Proof. +unfold R at 1 in |- *. +unfold g in |- *. +rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). +trivial. +exists (fun x:pow U => x) (fun x:pow U => x); trivial. +Qed. + + +Theorem classical_proof_irrelevence : T = F. +Proof. +generalize not_has_fixpoint. +unfold Not_b in |- *. +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.
\ No newline at end of file diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v new file mode 100644 index 00000000..a1f4417c --- /dev/null +++ b/theories/Logic/ChoiceFacts.v @@ -0,0 +1,139 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:06 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 := + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, + exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). + +Definition FunctionalChoice := + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). + +Definition ParamDefiniteDescription := + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> + exists f : A -> B, (forall x:A, R x (f x)). + +Lemma description_rel_choice_imp_funct_choice : + ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice. +intros Descr RelCh. +red in |- *; intros A B R H. +destruct (RelCh A B R H) as [R' H0]. +destruct (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 in |- *; intros A B R H. +destruct (FunCh A B R H) as [f H0]. +exists (fun x y => y = f x). +intro x; exists (f x); split; + [ apply H0 + | split; [ reflexivity | intros y H1; symmetry in |- *; exact H1 ] ]. +Qed. + +Lemma funct_choice_imp_description : + FunctionalChoice -> ParamDefiniteDescription. +intros FunCh. +red in |- *; intros A B R H. +destruct (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 := + forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), + (forall x:A, P x -> exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, + P x -> + exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). + +Definition ProofIrrelevance := forall (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 in |- *; intros A B P R H. +destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0]. +intros [x HPx]. +destruct (H x HPx) as [y HRxy]. +exists y; exact HRxy. +set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). +exists R''; intros x HPx. +destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]]. +exists y. split. + exact HRxy. + split. + red in |- *; exists HPx; exact HR'xy. + intros y' HR''xy'. + apply Huniq. + unfold R'' in HR''xy'. + destruct HR''xy' as [H'Px HR'xy']. + rewrite proof_irrel with (a1 := HPx) (a2 := H'Px). + exact HR'xy'. +Qed. + +Definition IndependenceOfPremises := + forall (A:Type) (P:A -> Prop) (Q:Prop), + (Q -> exists x : _, P x) -> exists x : _, Q -> P x. + +Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice : + RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice. +Proof. +intros RelCh IndPrem. +red in |- *; intros A B P R H. +destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0]. + intro x. apply IndPrem. + apply H. + exists R'. + intros x HPx. + destruct (H0 x) as [y [H1 H2]]. + exists y. split. + apply (H1 HPx). + exact H2. +Qed. diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v new file mode 100755 index 00000000..044cee17 --- /dev/null +++ b/theories/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.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Classical Logic *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Type.
\ No newline at end of file diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v new file mode 100644 index 00000000..51f758e2 --- /dev/null +++ b/theories/Logic/ClassicalChoice.v @@ -0,0 +1,32 @@ +(************************************************************************) +(* 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.4.2.1 2004/07/16 19:31:06 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 Import ChoiceFacts. + +Theorem choice : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). +Proof. +apply description_rel_choice_imp_funct_choice. +exact description. +exact relational_choice. +Qed.
\ No newline at end of file diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v new file mode 100644 index 00000000..6602cd73 --- /dev/null +++ b/theories/Logic/ClassicalDescription.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:06 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 : + forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), + (forall x:A, + exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -> + exists f : forall x:A, B x, (forall x:A, R x (f x)). + +(** Principle of definite descriptions (aka axiom of unique choice) *) + +Theorem description : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> + exists f : A -> B, (forall x:A, R x (f x)). +Proof. +intros A B. +apply (dependent_description A (fun _ => B)). +Qed. + +(** The followig proof comes from [1] *) + +Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. +Proof. +intro HnotEM. +set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). +assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). +apply description. +intro A. +destruct (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. +destruct 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 ! *) +destruct (f P). + left. + destruct HfP as [[Ha _]| [_ Hfalse]]. + assumption. + discriminate. + right. + destruct HfP as [[_ Hfalse]| [Hna _]]. + discriminate. + assumption. +Qed. + diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v new file mode 100644 index 00000000..cb14fb0e --- /dev/null +++ b/theories/Logic/ClassicalFacts.v @@ -0,0 +1,219 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:06 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 := forall A:Prop, A = True \/ A = False. + +(** [prop_extensionality] asserts equivalent formulas are equal *) +Definition prop_extensionality := forall 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 := forall A:Prop, A \/ ~ A. + +(** [proof_irrelevance] asserts equality of all proofs of a given formula *) +Definition proof_irrelevance := forall (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]. +destruct (H A); destruct (H B). + rewrite H1; exact H0. + absurd B. + rewrite H1; exact (fun H => H). + apply Hab; rewrite H0; exact I. + absurd A. + rewrite H0; exact (fun 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. +destruct (H A). + left; rewrite H0; exact I. + right; rewrite H0; exact (fun x => x). +Qed. + +Lemma prop_ext_em_degen : + prop_extensionality -> excluded_middle -> prop_degeneracy. +Proof. +intros Ext EM A. +destruct (EM A). + left; apply (Ext A True); split; + [ exact (fun _ => I) | exact (fun _ => 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 -> forall A:Prop, inhabited A -> (A -> A) = A. +Proof. +intros Ext A a. +apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. +Qed. + +Record retract (A B:Prop) : Prop := + {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}. + +Lemma prop_ext_retract_A_A_imp_A : + prop_extensionality -> forall 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 (fun x:A => x) (fun x:A => x). +reflexivity. +Qed. + +Record has_fixpoint (A:Prop) : Prop := + {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}. + +Lemma ext_prop_fixpoint : + prop_extensionality -> forall 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 (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). +intro f. +pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. +rewrite (g1_o_g2 (fun 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 : forall C:Prop, C -> C -> bool -> C. +Hypothesis + bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. +Hypothesis + bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. +Let bool_dep_induction := + forall P:bool -> Prop, P true -> P false -> forall 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. +set (neg := fun b:bool => bool_elim bool false true b). +generalize (refl_equal (G neg)). +pattern (G neg) at 1 in |- *. +apply Ind with (b := G neg); intro Heq. +rewrite (bool_elim_redl bool false true). +change (true = neg true) in |- *; rewrite Heq; apply Gfix. +rewrite (bool_elim_redr bool false true). +change (neg false = false) in |- *; rewrite Heq; symmetry in |- *; + apply Gfix. +Qed. + +Lemma ext_prop_dep_proof_irrel_gen : + prop_extensionality -> bool_dep_induction -> proof_irrelevance. +Proof. +intros Ext Ind A a1 a2. +set (f := fun b:bool => bool_elim A a1 a2 b). +rewrite (bool_elim_redl A a1 a2). +change (f true = a2) in |- *. +rewrite (bool_elim_redr A a1 a2). +change (f true = f false) in |- *. +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 := forall C:Prop, C -> C -> C. +Definition TrueP : BoolP := fun C c1 c2 => c1. +Definition FalseP : BoolP := fun C c1 c2 => c2. +Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. +Definition BoolP_elim_redl (C:Prop) (c1 c2:C) : + c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. +Definition BoolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. + +Definition BoolP_dep_induction := + forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall 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 := refl_equal c1. +Definition boolP_elim_redr (C:Prop) (c1 c2:C) : + c2 = boolP_ind C c1 c2 falseP := refl_equal c2. +Scheme boolP_indd := Induction for boolP Sort Prop. + +Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. +Proof + fun 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/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v new file mode 100755 index 00000000..c8f87fe8 --- /dev/null +++ b/theories/Logic/Classical_Pred_Set.v @@ -0,0 +1,70 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Classical Predicate Logic on Set*) + +Require Import Classical_Prop. + +Section Generic. +Variable U : Set. + +(** de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. +Proof. +unfold not in |- *; intros P notall. +apply NNPP; unfold not in |- *. +intro abs. +cut (forall n:U, P n); auto. +intro n; apply NNPP. +unfold not in |- *; intros. +apply abs; exists n; trivial. +Qed. + +Lemma not_all_not_ex : + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. +Proof. +intros P H. +elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. +apply NNPP; trivial. +Qed. + +Lemma not_ex_all_not : + forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. +Proof. +unfold not in |- *; intros P notex n abs. +apply notex. +exists n; trivial. +Qed. + +Lemma not_ex_not_all : + forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. +Proof. +intros P H n. +apply NNPP. +red in |- *; intro K; apply H; exists n; trivial. +Qed. + +Lemma ex_not_not_all : + forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). +Proof. +unfold not in |- *; intros P exnot allP. +elim exnot; auto. +Qed. + +Lemma all_not_not_ex : + forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). +Proof. +unfold not in |- *; intros P allnot exP; elim exP; intros n p. +apply allnot with n; auto. +Qed. + +End Generic.
\ No newline at end of file diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v new file mode 100755 index 00000000..804ff32d --- /dev/null +++ b/theories/Logic/Classical_Pred_Type.v @@ -0,0 +1,70 @@ +(************************************************************************) +(* 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.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Classical Predicate Logic on Type *) + +Require Import Classical_Prop. + +Section Generic. +Variable U : Type. + +(** de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. +Proof. +unfold not in |- *; intros P notall. +apply NNPP; unfold not in |- *. +intro abs. +cut (forall n:U, P n); auto. +intro n; apply NNPP. +unfold not in |- *; intros. +apply abs; exists n; trivial. +Qed. + +Lemma not_all_not_ex : + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. +Proof. +intros P H. +elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. +apply NNPP; trivial. +Qed. + +Lemma not_ex_all_not : + forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. +Proof. +unfold not in |- *; intros P notex n abs. +apply notex. +exists n; trivial. +Qed. + +Lemma not_ex_not_all : + forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. +Proof. +intros P H n. +apply NNPP. +red in |- *; intro K; apply H; exists n; trivial. +Qed. + +Lemma ex_not_not_all : + forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). +Proof. +unfold not in |- *; intros P exnot allP. +elim exnot; auto. +Qed. + +Lemma all_not_not_ex : + forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). +Proof. +unfold not in |- *; intros P allnot exP; elim exP; intros n p. +apply allnot with n; auto. +Qed. + +End Generic.
\ No newline at end of file diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v new file mode 100755 index 00000000..ccc26df1 --- /dev/null +++ b/theories/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.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Classical Propositional Logic *) + +Require Import ProofIrrelevance. + +Hint Unfold not: core. + +Axiom classic : forall P:Prop, P \/ ~ P. + +Lemma NNPP : forall p:Prop, ~ ~ p -> p. +Proof. +unfold not in |- *; intros; elim (classic p); auto. +intro NP; elim (H NP). +Qed. + +Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P. +Proof. +intros; apply NNPP; red in |- *. +intro; apply H; intro; absurd P; trivial. +Qed. + +Lemma not_imply_elim2 : forall P Q:Prop, ~ (P -> Q) -> ~ Q. +Proof. +intros; elim (classic Q); auto. +Qed. + +Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q. +Proof. +intros; elim (classic P); auto. +Qed. + +Lemma imply_to_and : forall 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 : forall P Q:Prop, ~ P \/ Q -> P -> Q. +Proof. +simple induction 1; auto. +intros H1 H2; elim (H1 H2). +Qed. + +Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q. +Proof. +intros; elim (classic P); auto. +Qed. + +Lemma or_not_and : forall P Q:Prop, ~ P \/ ~ Q -> ~ (P /\ Q). +Proof. +simple induction 1; red in |- *; simple induction 2; auto. +Qed. + +Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q. +Proof. +intros; elim (classic P); auto. +Qed. + +Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q). +Proof. +simple induction 1; red in |- *; simple induction 3; trivial. +Qed. + +Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q. +Proof. +simple induction 2; trivial. +Qed. + +Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R. +Proof. +simple induction 2; auto. +Qed. + +Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Proof proof_irrelevance_cci classic.
\ No newline at end of file diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v new file mode 100755 index 00000000..753b8590 --- /dev/null +++ b/theories/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.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Classical Logic for Type *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Type.
\ No newline at end of file diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v new file mode 100644 index 00000000..08babda9 --- /dev/null +++ b/theories/Logic/Decidable.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(*i $Id: Decidable.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Properties of decidable propositions *) + +Definition decidable (P:Prop) := P \/ ~ P. + +Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P. +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_True : decidable True. +unfold decidable in |- *; auto. +Qed. + +Theorem dec_False : decidable False. +unfold decidable, not in |- *; auto. +Qed. + +Theorem dec_or : + forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B). +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_and : + forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B). +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A). +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_imp : + forall A B:Prop, decidable A -> decidable B -> decidable (A -> B). +unfold decidable in |- *; tauto. +Qed. + +Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. +unfold decidable in |- *; tauto. Qed. + +Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B. +tauto. Qed. + +Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B. +unfold decidable in |- *; tauto. Qed. + +Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B. +unfold decidable in |- *; tauto. +Qed. + +Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B. +unfold decidable in |- *; tauto. +Qed. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v new file mode 100644 index 00000000..55eed096 --- /dev/null +++ b/theories/Logic/Diaconescu.v @@ -0,0 +1,138 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:06 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 := + forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q. + +(* From predicate extensionality we get propositional extensionality + hence proof-irrelevance *) + +Require Import ClassicalFacts. + +Variable pred_extensionality : PredicateExtensionality. + +Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B. +Proof. + intros A B H. + change ((fun _ => A) true = (fun _ => B) true) in |- *. + rewrite + pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B). + reflexivity. + intros _; exact H. +Qed. + +Lemma proof_irrel : forall (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 Import ChoiceFacts. + +Variable rel_choice : RelationalChoice. + +Lemma guarded_rel_choice : + forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), + (forall x:A, P x -> exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, + P x -> + exists y : B, R x y /\ R' x y /\ (forall 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 Import Bool. + +Lemma AC : + exists R : (bool -> Prop) -> bool -> Prop, + (forall P:bool -> Prop, + (exists b : bool, P b) -> + exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). +Proof. + apply guarded_rel_choice with + (P := fun Q:bool -> Prop => exists y : _, Q y) + (R := fun (Q:bool -> Prop) (y:bool) => Q y). + exact (fun _ 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 : forall P:Prop, P \/ ~ P. +Proof. +intro P. + +(* first we exhibit the choice functional relation R *) +destruct AC as [R H]. + +set (class_of_true := fun b => b = true \/ P). +set (class_of_false := fun b => b = false \/ P). + +(* the actual "decision": is (R class_of_true) = true or false? *) +destruct (H class_of_true) as [b0 [H0 [H0' H0'']]]. +exists true; left; reflexivity. +destruct H0. + +(* the actual "decision": is (R class_of_false) = true or false? *) +destruct (H class_of_false) as [b1 [H1 [H1' H1'']]]. +exists false; left; reflexivity. +destruct H1. + +(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *) +right. +intro HP. +assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b). +intro b; split. +unfold class_of_false in |- *; right; assumption. +unfold class_of_true in |- *; right; assumption. +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/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v new file mode 100755 index 00000000..24905039 --- /dev/null +++ b/theories/Logic/Eqdep.v @@ -0,0 +1,188 @@ +(************************************************************************) +(* 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.10.2.1 2004/07/16 19:31:06 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) : forall q:U, P q -> Prop := + eq_dep_intro : eq_dep p x p x. +Hint Constructors eq_dep: core v62. + +Lemma eq_dep_sym : + forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x. +Proof. +destruct 1; auto. +Qed. +Hint Immediate eq_dep_sym: core v62. + +Lemma eq_dep_trans : + forall (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. +destruct 1; auto. +Qed. + +Scheme eq_indd := Induction for eq Sort Prop. + +Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop := + eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y. + +Lemma eq_dep1_dep : + forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y. +Proof. +destruct 1 as (eq_qp, H). +destruct eq_qp using eq_indd. +rewrite H. +apply eq_dep_intro. +Qed. + +Lemma eq_dep_dep1 : + forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. +Proof. +destruct 1. +apply eq_dep1_intro with (refl_equal p). +simpl in |- *; trivial. +Qed. + +(** Invariance by Substitution of Reflexive Equality Proofs *) + +Axiom eq_rect_eq : + forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + +(** Injectivity of Dependent Equality is a consequence of *) +(** Invariance by Substitution of Reflexive Equality Proof *) + +Lemma eq_dep1_eq : forall (p:U) (x y:P p), eq_dep1 p x p y -> x = y. +Proof. +simple destruct 1; intro. +rewrite <- eq_rect_eq; auto. +Qed. + +Lemma eq_dep_eq : forall (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 : forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2. +Proof. +intros; apply eq_dep_eq with (P := fun 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 : forall (U:Type) (x:U) (p:x = x), p = refl_equal x. +Proof. +intros; apply UIP. +Qed. + +(** Streicher axiom K is a direct consequence of Uniqueness of + Reflexive Identity Proofs *) + +Lemma Streicher_K : + forall (U:Type) (x:U) (P:x = x -> Prop), + P (refl_equal x) -> forall 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 : + forall (U:Type) (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec 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 : + forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), + existS P p x = existS P q y <-> eq_dep U P p x q y. +Proof. +split. +(* -> *) +intro H. +change p with (projS1 (existS P p x)) in |- *. +change x at 2 with (projS2 (existS P p x)) in |- *. +rewrite H. +apply eq_dep_intro. +(* <- *) +destruct 1; reflexivity. +Qed. + +(** UIP implies the injectivity of equality on dependent pairs *) + +Lemma inj_pair2 : + forall (U:Set) (P:U -> Set) (p:U) (x y:P p), + existS P p x = existS P p y -> x = y. +Proof. +intros. +apply (eq_dep_eq U P). +generalize (equiv_eqex_eqdep U P p p x y). +simple induction 1. +intros. +auto. +Qed. + +(** UIP implies the injectivity of equality on dependent pairs *) + +Lemma inj_pairT2 : + forall (U:Type) (P:U -> Type) (p:U) (x y:P p), + existT P p x = existT P p y -> x = y. +Proof. +intros. +apply (eq_dep_eq U P). +change p at 1 with (projT1 (existT P p x)) in |- *. +change x at 2 with (projT2 (existT P p x)) in |- *. +rewrite H. +apply eq_dep_intro. +Qed. + +(** The main results to be exported *) + +Hint Resolve eq_dep_intro eq_dep_eq: core v62. +Hint Immediate eq_dep_sym: core v62. +Hint Resolve inj_pair2 inj_pairT2: core. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v new file mode 100644 index 00000000..7caf403c --- /dev/null +++ b/theories/Logic/Eqdep_dec.v @@ -0,0 +1,158 @@ +(************************************************************************) +(* 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.14.2.1 2004/07/16 19:31:06 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) (eqxy:x = y) : + x = y := + match eqxy in (_ = y) return x = y with + | refl_equal => refl_equal x + end. + + Definition eqT2eq (A:Set) (x y:A) (eqTxy:x = y) : + x = y := + match eqTxy in (_ = y) return x = y with + | refl_equal => refl_equal x + end. + + Lemma eq_eqT_bij : forall (A:Set) (x y:A) (p:x = y), p = eqT2eq (eq2eqT p). +intros. +case p; reflexivity. +Qed. + + Lemma eqT_eq_bij : forall (A:Set) (x y:A) (p:x = y), p = eq2eqT (eqT2eq p). +intros. +case p; reflexivity. +Qed. + + +Section DecidableEqDep. + + Variable A : Type. + + Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' := + eq_ind _ (fun a => a = y') eq2 _ eq1. + + Remark trans_sym_eqT : forall (x y:A) (u:x = y), comp u u = refl_equal y. +intros. +case u; trivial. +Qed. + + + + Variable eq_dec : forall x y:A, x = y \/ x <> y. + + Variable x : A. + + + Let nu (y:A) (u:x = y) : x = y := + match eq_dec x y with + | or_introl eqxy => eqxy + | or_intror neqxy => False_ind _ (neqxy u) + end. + + Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v. +intros. +unfold nu in |- *. +case (eq_dec x y); intros. +reflexivity. + +case n; trivial. +Qed. + + + Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v. + + + Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u. +intros. +case u; unfold nu_inv in |- *. +apply trans_sym_eqT. +Qed. + + + Theorem eq_proofs_unicity : forall (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 : + forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p. +intros. +elim eq_proofs_unicity with x (refl_equal x) p. +trivial. +Qed. + + + (** The corollary *) + + Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x := + match exP with + | ex_intro x' prf => + match eq_dec x' x with + | or_introl eqprf => eq_ind x' P prf x eqprf + | _ => def + end + end. + + + Theorem inj_right_pair : + forall (P:A -> Prop) (y y':P x), + ex_intro P x y = ex_intro P x y' -> y = y'. +intros. +cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). +simpl in |- *. +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 : + forall A:Set, + (forall x y:A, {x = y} + {x <> y}) -> + forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. +intros. +rewrite eq_eqT_bij. +elim (eq2eqT p) using K_dec. +intros. +case (H x0 y); intros. +elim e; left; reflexivity. + +right; red in |- *; intro neq; apply n; elim neq; reflexivity. + +trivial. +Qed.
\ No newline at end of file diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v new file mode 100644 index 00000000..46a57432 --- /dev/null +++ b/theories/Logic/Hurkens.v @@ -0,0 +1,81 @@ +(************************************************************************) +(* 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 : forall A:Prop, b2p (p2b A) -> A. +Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A). +Variable B : Prop. + +Definition V := forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool. +Definition U := V -> bool. +Definition sb (z:V) : V := fun A r a => r (z A r) a. +Definition le (i:U -> bool) (x:U) : bool := + x (fun A r a => i (fun v => sb v A r a)). +Definition induct (i:U -> bool) : Prop := + forall x:U, b2p (le i x) -> b2p (i x). +Definition WF : U := fun z => p2b (induct (z U le)). +Definition I (x:U) : Prop := + (forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B. + +Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF). +Proof. +intros i y. +apply y. +unfold le, WF, induct in |- *. +apply p2p2. +intros x H0. +apply y. +exact H0. +Qed. + +Lemma lemma1 : induct (fun u => p2b (I u)). +Proof. +unfold induct in |- *. +intros x p. +apply (p2p2 (I x)). +intro q. +apply (p2p1 (I (fun v:V => sb v U le x)) (q (fun u => p2b (I u)) p)). +intro i. +apply q with (i := fun y => i (fun v:V => sb v U le y)). +Qed. + +Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B. +Proof. +intro x. +apply (p2p1 (I WF) (x (fun u => p2b (I u)) lemma1)). +intros i H0. +apply (x (fun y => i (fun v => sb v U le y))). +apply (p2p1 _ H0). +Qed. + +Theorem paradox : B. +Proof. +exact (lemma2 Omega). +Qed. + +End Paradox. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v new file mode 100644 index 00000000..5b7528be --- /dev/null +++ b/theories/Logic/JMeq.v @@ -0,0 +1,68 @@ +(************************************************************************) +(* 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.8.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** John Major's Equality as proposed by C. Mc Bride *) + +Set Implicit Arguments. + +Inductive JMeq (A:Set) (x:A) : forall B:Set, B -> Prop := + JMeq_refl : JMeq x x. +Reset JMeq_ind. + +Hint Resolve JMeq_refl. + +Lemma sym_JMeq : forall (A B:Set) (x:A) (y:B), JMeq x y -> JMeq y x. +destruct 1; trivial. +Qed. + +Hint Immediate sym_JMeq. + +Lemma trans_JMeq : + forall (A B C:Set) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z. +destruct 1; trivial. +Qed. + +Axiom JMeq_eq : forall (A:Set) (x y:A), JMeq x y -> x = y. + +Lemma JMeq_ind : forall (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 : forall (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 : + forall (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 : + forall (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 Import Eqdep. + +Lemma JMeq_eq_dep : + forall (A B:Set) (x:A) (y:B), JMeq x y -> eq_dep Set (fun X => X) A x B y. +Proof. +destruct 1. +apply eq_dep_intro. +Qed. + +Lemma eq_dep_JMeq : + forall (A B:Set) (x:A) (y:B), eq_dep Set (fun X => X) A x B y -> JMeq x y. +Proof. +destruct 1. +apply JMeq_refl. +Qed.
\ No newline at end of file diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v new file mode 100644 index 00000000..afdc0ffe --- /dev/null +++ b/theories/Logic/ProofIrrelevance.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* 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 Import Hurkens. + +Section Proof_irrelevance_CC. + +Variable or : Prop -> Prop -> Prop. +Variable or_introl : forall A B:Prop, A -> or A B. +Variable or_intror : forall A B:Prop, B -> or A B. +Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. +Hypothesis + or_elim_redl : + forall (A B 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 : + forall (A B 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 : + forall (A B:Prop) (P:or A B -> Prop), + (forall a:A, P (or_introl A B a)) -> + (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. + +Hypothesis em : forall A:Prop, or A (~ A). +Variable B : Prop. +Variables b1 b2 : B. + +(** [p2b] and [b2p] form a retract if [~b1=b2] *) + +Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). +Definition b2p b := b1 = b. + +Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). +Proof. + unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); + unfold b2p in |- *; intros. + apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)). + destruct (b H). +Qed. +Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. +Proof. + intro not_eq_b1_b2. + unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A); + unfold b2p in |- *; intros. + assumption. + destruct not_eq_b1_b2. + rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => 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 : forall A:Prop, A \/ ~ A. + +Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) + (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). +Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) + (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). +Scheme or_indd := Induction for or Sort Prop. + +Theorem proof_irrelevance_cci : forall (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 : forall A:Prop, {A}+{~A}] in CCI +*) diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v new file mode 100644 index 00000000..ca7b760e --- /dev/null +++ b/theories/Logic/RelationalChoice.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* 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.3.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(* This file axiomatizes the relational form of the axiom of choice *) + +Axiom + relational_choice : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, + exists y : B, + R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex new file mode 100755 index 00000000..1fb294f2 --- /dev/null +++ b/theories/Logic/intro.tex @@ -0,0 +1,8 @@ +\section{Logic}\label{Logic} + +This library deals with classical logic and its properties. +The main file is {\tt Classical.v}. + +This library also provides some facts on equalities for dependent +types. See the files {\tt Eqdep.v} and {\tt JMeq.v}. + |