From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- theories/Arith/Arith.v | 5 ++--- theories/Init/Notations.v | 6 +++--- theories/Logic/Berardi.v | 6 +++--- theories/Logic/ChoiceFacts.v | 8 ++++---- theories/Logic/Diaconescu.v | 28 ++++++++++++++-------------- theories/Logic/JMeq.v | 13 ++++++++++--- theories/Logic/RelationalChoice.v | 4 ++-- theories/ZArith/ZArith.v | 3 +-- 8 files changed, 39 insertions(+), 34 deletions(-) (limited to 'theories') diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index d44efb56..114a60ee 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Arith.v,v 1.11.2.1 2004/07/16 19:30:59 herbelin Exp $ i*) +(*i $Id: Arith.v,v 1.11.2.2 2004/08/03 17:42:42 herbelin Exp $ i*) Require Export Le. Require Export Lt. @@ -15,7 +15,6 @@ Require Export Gt. Require Export Minus. Require Export Mult. Require Export Between. -Require Export Minus. Require Export Peano_dec. Require Export Compare_dec. -Require Export Factorial. \ No newline at end of file +Require Export Factorial. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 2e7cb1fc..e0a18747 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Notations.v,v 1.24.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*) -(** These are the notations whose level and associativity is imposed by Coq *) +(** These are the notations whose level and associativity are imposed by Coq *) -(** Notations for logical connectives *) +(** Notations for propositional connectives *) Reserved Notation "x <-> y" (at level 95, no associativity). Reserved Notation "x /\ y" (at level 80, right associativity). diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 7e950c17..0fe8a87d 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -6,11 +6,11 @@ (* * 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*) +(*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 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). + choice (AC) imply proof irrelevance (PI). Here, the axiom of choice is not necessary because of the use of inductive types. << @@ -156,4 +156,4 @@ intros not_true is_true. elim not_true; trivial. Qed. -End Berardis_paradox. \ No newline at end of file +End Berardis_paradox. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index a1f4417c..87d8a70e 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -6,14 +6,14 @@ (* * 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*) +(*i $Id: ChoiceFacts.v,v 1.7.2.2 2004/08/01 09:29:59 herbelin Exp $ i*) -(* We show that the functional formulation of the axiom of Choice +(** 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 +(** 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 *) @@ -80,7 +80,7 @@ intro H; split; 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 +(** 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 *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 55eed096..2b982963 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -6,9 +6,9 @@ (* * 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*) +(*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*) -(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory +(** 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. @@ -27,12 +27,12 @@ Section PredExt_GuardRelChoice_imp_EM. -(* The axiom of extensionality for predicates *) +(** 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 +(** From predicate extensionality we get propositional extensionality hence proof-irrelevance *) Require Import ClassicalFacts. @@ -54,7 +54,7 @@ Proof. apply (ext_prop_dep_proof_irrel_cic prop_ext). Qed. -(* From proof-irrelevance and relational choice, we get guarded +(** From proof-irrelevance and relational choice, we get guarded relational choice *) Require Import ChoiceFacts. @@ -73,8 +73,8 @@ Proof. (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 *) +(** 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. @@ -90,30 +90,30 @@ Proof. exact (fun _ H => H). Qed. -(* The proof of the excluded middle *) -(* Remark: P could have been in Set or Type *) +(** 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 *) +(** 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? *) +(** 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? *) +(** 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 *) +(** 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). @@ -129,7 +129,7 @@ rewrite <- H0''. reflexivity. rewrite Heq. assumption. -(* cases where P is true *) +(** cases where P is true *) left; assumption. left; assumption. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 5b7528be..4666d9b4 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,9 +6,16 @@ (* * 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*) +(*i $Id: JMeq.v,v 1.8.2.2 2004/08/03 17:42:32 herbelin Exp $ i*) -(** John Major's Equality as proposed by C. Mc Bride *) +(** John Major's Equality as proposed by C. Mc Bride + + Reference: + + [McBride] Elimination with a Motive, Proceedings of TYPES 2000, + LNCS 2277, pp 197-216, 2002. + +*) Set Implicit Arguments. @@ -65,4 +72,4 @@ Lemma eq_dep_JMeq : Proof. destruct 1. apply JMeq_refl. -Qed. \ No newline at end of file +Qed. diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index ca7b760e..08873aa5 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -6,9 +6,9 @@ (* * 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*) +(*i $Id: RelationalChoice.v,v 1.3.2.2 2004/08/01 09:29:59 herbelin Exp $ i*) -(* This file axiomatizes the relational form of the axiom of choice *) +(** This file axiomatizes the relational form of the axiom of choice *) Axiom relational_choice : diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 78295591..7e361621 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZArith.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*) +(*i $Id: ZArith.v,v 1.5.2.2 2004/08/03 17:56:30 herbelin Exp $ i*) (** Library for manipulating integers based on binary encoding *) @@ -19,4 +19,3 @@ Require Export Zsqrt. Require Export Zpower. Require Export Zdiv. Require Export Zlogarithm. -Require Export Zbool. \ No newline at end of file -- cgit v1.2.3