summaryrefslogtreecommitdiff
path: root/theories/Logic
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/Berardi.v14
-rw-r--r--theories/Logic/ChoiceFacts.v140
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical.v5
-rw-r--r--theories/Logic/ClassicalChoice.v11
-rw-r--r--theories/Logic/ClassicalDescription.v2
-rw-r--r--theories/Logic/ClassicalFacts.v363
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Pred_Set.v47
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Pred_Type.v37
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Prop.v57
-rw-r--r--[-rwxr-xr-x]theories/Logic/Classical_Type.v6
-rw-r--r--theories/Logic/Decidable.v2
-rw-r--r--theories/Logic/Diaconescu.v10
-rw-r--r--[-rwxr-xr-x]theories/Logic/Eqdep.v182
-rw-r--r--theories/Logic/EqdepFacts.v351
-rw-r--r--theories/Logic/Eqdep_dec.v230
-rw-r--r--theories/Logic/JMeq.v4
-rw-r--r--theories/Logic/ProofIrrelevance.v108
-rw-r--r--theories/Logic/ProofIrrelevanceFacts.v62
-rw-r--r--theories/Logic/RelationalChoice.v2
19 files changed, 1173 insertions, 460 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 0fe8a87d..9eaef07a 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*)
+(*i $Id: Berardi.v 8122 2006-03-04 19:26:40Z herbelin $ i*)
(** This file formalizes Berardi's paradox which says that in
the calculus of constructions, excluded middle (EM) and axiom of
@@ -92,14 +92,10 @@ End Retracts.
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.
+destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
+ exists f0 g0; trivial.
+ exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
+ destruct hf; auto.
Qed.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 87d8a70e..bc892ca9 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ChoiceFacts.v,v 1.7.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
+(*i $Id: ChoiceFacts.v 8132 2006-03-05 10:59:47Z herbelin $ i*)
(** We show that the functional formulation of the axiom of Choice
(usual formulation in type theory) is equivalent to its relational
@@ -17,29 +17,33 @@
relational formulation) without known inconsistency with classical logic,
though definite description conflicts with classical logic *)
+Section ChoiceEquivalences.
+
+Variables A B :Type.
+
Definition RelationalChoice :=
- forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
+ forall (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')).
+ 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) ->
+ forall (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')) ->
+ forall (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].
+red in |- *; intros R H.
+destruct (RelCh R H) as [R' H0].
+destruct (Descr 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.
@@ -50,8 +54,8 @@ 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].
+red in |- *; intros R H.
+destruct (FunCh R H) as [f H0].
exists (fun x y => y = f x).
intro x; exists (f x); split;
[ apply H0
@@ -61,8 +65,8 @@ 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].
+red in |- *; intros R H.
+destruct (FunCh R) as [f H0].
(* 1 *)
intro x.
elim (H x); intros y [H0 H1].
@@ -80,22 +84,25 @@ intro H; split;
intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
Qed.
+End ChoiceEquivalences.
+
(** 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) ->
+Definition GuardedRelationalChoice (A B:Type) :=
+ forall (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')).
+ 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.
+ (forall A B, RelationalChoice A B)
+ -> ProofIrrelevance -> (forall A B, GuardedRelationalChoice A B).
Proof.
intros rel_choice proof_irrel.
red in |- *; intros A B P R H.
@@ -103,7 +110,7 @@ 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).
+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.
@@ -118,16 +125,17 @@ exists y. split.
exact HR'xy'.
Qed.
-Definition IndependenceOfPremises :=
+Definition IndependenceOfGeneralPremises :=
forall (A:Type) (P:A -> Prop) (Q:Prop),
- (Q -> exists x : _, P x) -> exists x : _, Q -> P x.
+ (Q -> exists x, P x) -> exists x, Q -> P x.
-Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
- RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
+Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
+ forall A B, RelationalChoice A B ->
+ IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
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].
+intros A B RelCh IndPrem.
+red in |- *; intros P R H.
+destruct (RelCh (fun x y => P x -> R x y)) as [R' H0].
intro x. apply IndPrem.
apply H.
exists R'.
@@ -137,3 +145,79 @@ destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
apply (H1 HPx).
exact H2.
Qed.
+
+
+(** Countable codomains, such as [nat], can be equipped with a
+ well-order, which implies the existence of a least element on
+ inhabited decidable subsets. As a consequence, the relational form of
+ the axiom of choice is derivable on [nat] for decidable relations.
+
+ We show instead that definite description and the functional form
+ of the axiom of choice are equivalent on decidable relation with [nat]
+ as codomain
+*)
+
+Require Import Wf_nat.
+Require Import Compare_dec.
+Require Import Decidable.
+Require Import Arith.
+
+Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
+ (exists x, (P x /\ forall x', P x' -> R x x')
+ /\ forall x', P x' /\ (forall x'', P x'' -> R x' x'') -> x=x').
+
+Lemma dec_inh_nat_subset_has_unique_least_element :
+ forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
+ (exists n, P n) -> has_unique_least_element nat le P.
+Proof.
+intros P Pdec (n0,HPn0).
+assert
+ (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
+ \/(forall n', P n' -> n<=n')).
+ induction n.
+ right.
+ intros n' Hn'.
+ apply le_O_n.
+ destruct IHn.
+ left; destruct H as (n', (Hlt', HPn')).
+ exists n'; split.
+ apply lt_S; assumption.
+ assumption.
+ destruct (Pdec n).
+ left; exists n; split.
+ apply lt_n_Sn.
+ split; assumption.
+ right.
+ intros n' Hltn'.
+ destruct (le_lt_eq_dec n n') as [Hltn|Heqn].
+ apply H; assumption.
+ assumption.
+ destruct H0.
+ rewrite Heqn; assumption.
+destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
+ repeat split;
+ assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
+Qed.
+
+Definition FunctionalChoice_on (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)).
+
+Lemma classical_denumerable_description_imp_fun_choice :
+ forall A:Type,
+ ParamDefiniteDescription A nat ->
+ forall R, (forall x y, decidable (R x y)) -> FunctionalChoice_on A nat R.
+Proof.
+intros A Descr.
+red in |- *; intros R Rdec H.
+set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y').
+destruct (Descr R') as [f Hf].
+ intro x.
+ apply (dec_inh_nat_subset_has_unique_least_element (R x)).
+ apply Rdec.
+ apply (H x).
+exists f.
+intros x.
+destruct (Hf x) as [Hfx _].
+assumption.
+Qed.
diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v
index 044cee17..523c9245 100755..100644
--- a/theories/Logic/Classical.v
+++ b/theories/Logic/Classical.v
@@ -6,9 +6,10 @@
(* * 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*)
+(*i $Id: Classical.v 8642 2006-03-17 10:09:02Z notin $ i*)
(** Classical Logic *)
Require Export Classical_Prop.
-Require Export Classical_Pred_Type. \ No newline at end of file
+Require Export Classical_Pred_Type.
+
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 51f758e2..5a633f84 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -6,7 +6,7 @@
(* * 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*)
+(*i $Id: ClassicalChoice.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
(** This file provides classical logic and functional choice *)
@@ -23,10 +23,11 @@ Require Import ChoiceFacts.
Theorem choice :
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B, R x y) ->
+ (forall x:A, exists y : B, R x y) ->
exists f : A -> B, (forall x:A, R x (f x)).
Proof.
+intros A B.
apply description_rel_choice_imp_funct_choice.
-exact description.
-exact relational_choice.
-Qed. \ No newline at end of file
+exact (description A B).
+exact (relational_choice A B).
+Qed.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 6602cd73..ce3e279c 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,7 +6,7 @@
(* * 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*)
+(*i $Id: ClassicalDescription.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** This file provides classical logic and definite description *)
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index cb14fb0e..91056250 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -6,24 +6,56 @@
(* * 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*)
+(*i $Id: ClassicalFacts.v 8136 2006-03-05 21:57:47Z herbelin $ i*)
-(** Some facts and definitions about classical logic *)
+(** ** 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 *)
+Table of contents:
+
+A. Propositional degeneracy = excluded-middle + propositional extensionality
+
+B. Classical logic and proof-irrelevance
+
+B. 1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint
+
+B. 2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance
+
+B. 3. CIC |- prop. ext. -> proof-irrelevance
+
+B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance
+
+B. 5. CIC |- excluded-middle -> proof-irrelevance
+
+C. Weak classical axioms
+
+C. 1. Weak excluded middle
+
+C. 2. Gödel-Dummet axiom and right distributivity of implication over
+ disjunction
+
+C. 3. Independence of general premises and drinker's paradox
+
+*)
+
+(************************************************************************)
+(** *** A. Prop degeneracy = excluded-middle + prop extensionality *)
+(**
+ i.e. [(forall A, A=True \/ A=False)
+ <->
+ (forall A, A\/~A) /\ (forall A B, (A<->B) -> A=B)]
+*)
+
+(** [prop_degeneracy] (also referred to 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 *)
+(** [prop_extensionality] asserts that 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 *)
+(** [excluded_middle] asserts that 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.
@@ -58,6 +90,12 @@ destruct (EM A).
right; apply (Ext A False); split; [ exact H | apply False_ind ].
Qed.
+(************************************************************************)
+(** *** B. Classical logic and proof-irrelevance *)
+
+(************************************************************************)
+(** **** B. 1. CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *)
+
(** We successively show that:
[prop_extensionality]
@@ -104,13 +142,20 @@ 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
+(************************************************************************)
+(** **** B. 2. CC |- prop_ext /\ dep elim on bool -> proof-irrelevance *)
+
+(** [proof_irrelevance] asserts equality of all proofs of a given formula *)
+Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
+
+(** Assume that 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.
+ We then map equality of boolean proofs to proof irrelevance in all
+ propositions.
*)
Section Proof_irrelevance_gen.
@@ -161,7 +206,7 @@ End Proof_irrelevance_gen.
most 2 elements.
*)
-Section Proof_irrelevance_CC.
+Section Proof_irrelevance_Prop_Ext_CC.
Definition BoolP := forall C:Prop, C -> C -> C.
Definition TrueP : BoolP := fun C c1 c2 => c1.
@@ -181,7 +226,10 @@ Proof
ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl
BoolP_elim_redr.
-End Proof_irrelevance_CC.
+End Proof_irrelevance_Prop_Ext_CC.
+
+(************************************************************************)
+(** **** B. 3. CIC |- prop. ext. -> proof-irrelevance *)
(** In the Calculus of Inductive Constructions, inductively defined booleans
enjoy dependent case analysis, hence directly proof-irrelevance from
@@ -211,9 +259,286 @@ End Proof_irrelevance_CIC.
(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.
+ Berardi [[Berardi90]] built a model of CC interpreting inhabited
+ types by the set of all untyped lambda-terms. This model satisfies
+ propositional degeneracy without satisfying proof-irrelevance (nor
+ dependent case analysis). This implies that the previous results
+ cannot be refined.
+
+ [[Berardi90]] Stefano Berardi, "Type dependence and constructive
+ mathematics", Ph. D. thesis, Dipartimento Matematica, Università di
+ Torino, 1990.
*)
+
+(************************************************************************)
+(** **** B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance *)
+
+(** This is a proof in the pure Calculus of Construction that
+ classical logic in [Prop] + dependent elimination of disjunction entails
+ proof-irrelevance.
+
+ Reference:
+
+ [[Coquand90]] 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_EM_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_EM_CC.
+
+(** Remark: Hurkens' paradox still holds with a retract from the
+ _negative_ fragment of [Prop] into [bool], hence weak classical
+ logic, i.e. [forall A, ~A\/~~A], is enough for deriving
+ proof-irrelevance.
+*)
+
+(************************************************************************)
+(** **** B. 5. CIC |- excluded-middle -> proof-irrelevance *)
+
+(**
+ Since, dependent elimination is derivable in the Calculus of
+ Inductive Constructions (CCI), we get proof-irrelevance from classical
+ logic in the CCI.
+*)
+
+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 the Set-impredicative CCI, Hurkens' paradox still holds with
+ [bool] in [Set] and since [~true=false] for [true] and [false]
+ in [bool] from [Set], we get the inconsistency of
+ [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI.
+*)
+
+(** *** C. Weak classical axioms *)
+
+(** We show the following increasing in the strength of axioms:
+ - weak excluded-middle
+ - right distributivity of implication over disjunction and Gödel-Dummet axiom
+ - independence of general premises and drinker's paradox
+ - excluded-middle
+*)
+
+(** **** C. 1. Weak excluded-middle *)
+
+(** The weak classical logic based on [~~A \/ ~A] is referred to with
+ name KC in {[ChagrovZakharyaschev97]]
+
+ [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael
+ Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
+*)
+
+Definition weak_excluded_middle :=
+ forall A:Prop, ~~A \/ ~A.
+
+(** The interest in the equivalent variant
+ [weak_generalized_excluded_middle] is that it holds even in logic
+ without a primitive [False] connective (like Gödel-Dummett axiom) *)
+
+Definition weak_generalized_excluded_middle :=
+ forall A B:Prop, ((A -> B) -> B) \/ (A -> B).
+
+(** **** C. 2. Gödel-Dummett axiom *)
+
+(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
+
+ [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus
+ with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol
+ 24 No. 2(1959), pp 97-103.
+
+ [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
+ Ergeb. Math. Koll. 4 (1933), pp. 34-38.
+ *)
+
+Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A).
+
+Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett.
+Proof.
+intros EM A B. destruct (EM B) as [HB|HnotB].
+ left; intros _; exact HB.
+ right; intros HB; destruct (HnotB HB).
+Qed.
+
+(** [(A->B) \/ (B->A)] is equivalent to [(C -> A\/B) -> (C->A) \/ (C->B)]
+ (proof from [[Dummett59]]) *)
+
+Definition RightDistributivityImplicationOverDisjunction :=
+ forall A B C:Prop, (C -> A\/B) -> (C->A) \/ (C->B).
+
+Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction :
+ GodelDummett <-> RightDistributivityImplicationOverDisjunction.
+Proof.
+split.
+ intros GD A B C HCAB.
+ destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC;
+ destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption.
+ intros Distr A B.
+ destruct (Distr A B (A\/B)) as [HABA|HABB].
+ intro HAB; exact HAB.
+ right; intro HB; apply HABA; right; assumption.
+ left; intro HA; apply HABB; left; assumption.
+Qed.
+
+(** [(A->B) \/ (B->A)] is stronger than the weak excluded middle *)
+
+Lemma Godel_Dummett_weak_excluded_middle :
+ GodelDummett -> weak_excluded_middle.
+Proof.
+intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA].
+ left; intro HnotA; apply (HnotA (HnotAA HnotA)).
+ right; intro HA; apply (HAnotA HA HA).
+Qed.
+
+(** **** C. 3. Independence of general premises and drinker's paradox *)
+
+(** Independence of general premises is the unconstrained, non
+ constructive, version of the Independence of Premises as
+ considered in [[Troelstra73]].
+
+ It is a generalization to predicate logic of the right
+ distributivity of implication over disjunction (hence of
+ Gödel-Dummett axiom) whose own constructive form (obtained by a
+ restricting the third formula to be negative) is called
+ Kreisel-Putnam principle [[KreiselPutnam57]].
+
+ [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine
+ Unableitsbarkeitsbeweismethode für den intuitionistischen
+ Aussagenkalkül". Archiv für Mathematische Logik und
+ Graundlagenforschung, 3:74- 78, 1957.
+
+ [[Troelstra73]], Anne Troelstra, editor. Metamathematical
+ Investigation of Intuitionistic Arithmetic and Analysis, volume
+ 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
+*)
+
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
+
+Definition IndependenceOfGeneralPremises :=
+ forall (A:Type) (P:A -> Prop) (Q:Prop),
+ inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x.
+
+Lemma
+ independence_general_premises_right_distr_implication_over_disjunction :
+ IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction.
+Proof.
+intros IP A B C HCAB.
+destruct (IP bool (fun b => if b then A else B) C true) as ([|],H).
+ intro HC; destruct (HCAB HC); [exists true|exists false]; assumption.
+ left; assumption.
+ right; assumption.
+Qed.
+
+Lemma independence_general_premises_Godel_Dummett :
+ IndependenceOfGeneralPremises -> GodelDummett.
+Proof.
+destruct Godel_Dummett_iff_right_distr_implication_over_disjunction.
+auto using independence_general_premises_right_distr_implication_over_disjunction.
+Qed.
+
+(** Independence of general premises is equivalent to the drinker's paradox *)
+
+Definition DrinkerParadox :=
+ forall (A:Type) (P:A -> Prop),
+ inhabited A -> exists x, (exists x, P x) -> P x.
+
+Lemma independence_general_premises_drinker :
+ IndependenceOfGeneralPremises <-> DrinkerParadox.
+Proof.
+split.
+ intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx.
+ intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx).
+ exists x; intro HQ; apply (Hx (H HQ)).
+Qed.
+
+(** Independence of general premises is weaker than (generalized)
+ excluded middle *)
+
+Definition generalized_excluded_middle :=
+ forall A B:Prop, A \/ (A -> B).
+
+Lemma excluded_middle_independence_general_premises :
+ generalized_excluded_middle -> DrinkerParadox.
+Proof.
+intros GEM A P x0.
+destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot].
+ exists x; intro; exact Hx.
+ exists x0; exact Hnot.
+Qed.
+
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index c8f87fe8..2a5f03ec 100755..100644
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -6,11 +6,14 @@
(* * 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*)
+(*i $Id: Classical_Pred_Set.v 8642 2006-03-17 10:09:02Z notin $ i*)
+
+(** This file is obsolete, use Classical_Pred_Type.v via Classical.v
+instead *)
(** Classical Predicate Logic on Set*)
-Require Import Classical_Prop.
+Require Import Classical_Pred_Type.
Section Generic.
Variable U : Set.
@@ -19,52 +22,26 @@ Variable U : Set.
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.
+Proof (Classical_Pred_Type.not_all_ex_not U).
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.
+Proof (Classical_Pred_Type.not_all_not_ex U).
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.
+Proof (Classical_Pred_Type.not_ex_all_not U).
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.
+Proof (Classical_Pred_Type.not_ex_not_all U).
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.
+Proof (Classical_Pred_Type.ex_not_not_all U).
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.
+Proof (Classical_Pred_Type.all_not_not_ex U).
-End Generic. \ No newline at end of file
+End Generic.
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 804ff32d..56ebf967 100755..100644
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -6,7 +6,7 @@
(* * 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*)
+(*i $Id: Classical_Pred_Type.v 8642 2006-03-17 10:09:02Z notin $ i*)
(** Classical Predicate Logic on Type *)
@@ -17,29 +17,30 @@ 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.
+Lemma not_all_not_ex :
+ 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 |- *.
+intros P notall.
+apply NNPP.
intro abs.
-cut (forall n:U, P n); auto.
-intro n; apply NNPP.
-unfold not in |- *; intros.
-apply abs; exists n; trivial.
+apply notall.
+intros n H.
+apply abs; exists n; exact H.
Qed.
-Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n.
+Lemma not_all_ex_not :
+ 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.
+intros P notall.
+apply not_all_not_ex with (P:=fun x => ~ P x).
+intro all; apply notall.
+intro n; apply NNPP.
+apply all.
Qed.
Lemma not_ex_all_not :
forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
-Proof.
+Proof. (* Intuitionistic *)
unfold not in |- *; intros P notex n abs.
apply notex.
exists n; trivial.
@@ -55,16 +56,16 @@ Qed.
Lemma ex_not_not_all :
forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
-Proof.
+Proof. (* Intuitionistic *)
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.
+Proof. (* Intuitionistic *)
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
+End Generic.
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index ccc26df1..f8b0e65b 100755..100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -6,11 +6,11 @@
(* * 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*)
+(*i $Id: Classical_Prop.v 8642 2006-03-17 10:09:02Z notin $ i*)
(** Classical Propositional Logic *)
-Require Import ProofIrrelevance.
+Require Import ClassicalFacts.
Hint Unfold not: core.
@@ -29,8 +29,8 @@ 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.
+Proof. (* Intuitionistic *)
+tauto.
Qed.
Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q.
@@ -46,9 +46,8 @@ 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).
+Proof. (* Intuitionistic *)
+tauto.
Qed.
Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q.
@@ -62,24 +61,50 @@ 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.
+Proof. (* Intuitionistic *)
+tauto.
Qed.
Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q).
-Proof.
-simple induction 1; red in |- *; simple induction 3; trivial.
+Proof. (* Intuitionistic *)
+tauto.
Qed.
Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q.
-Proof.
-simple induction 2; trivial.
+Proof. (* Intuitionistic *)
+tauto.
Qed.
Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R.
-Proof.
-simple induction 2; auto.
+Proof. (* Intuitionistic *)
+tauto.
Qed.
Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
-Proof proof_irrelevance_cci classic. \ No newline at end of file
+Proof proof_irrelevance_cci classic.
+
+(* classical_left transforms |- A \/ B into ~B |- A *)
+(* classical_right transforms |- A \/ B into ~A |- B *)
+
+Ltac classical_right := match goal with
+ | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
+end.
+
+Ltac classical_left := match goal with
+| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
+end.
+
+Require Export EqdepFacts.
+
+Module Eq_rect_eq.
+
+Lemma eq_rect_eq :
+ forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+Proof.
+intros; rewrite proof_irrelevance with (p1:=h) (p2:=refl_equal p); reflexivity.
+Qed.
+
+End Eq_rect_eq.
+
+Module EqdepTheory := EqdepTheory(Eq_rect_eq).
+Export EqdepTheory.
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
index 753b8590..9b1f4e19 100755..100644
--- a/theories/Logic/Classical_Type.v
+++ b/theories/Logic/Classical_Type.v
@@ -6,9 +6,11 @@
(* * 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*)
+(*i $Id: Classical_Type.v 8642 2006-03-17 10:09:02Z notin $ i*)
+
+(** This file is obsolete, use Classical.v instead *)
(** Classical Logic for Type *)
Require Export Classical_Prop.
-Require Export Classical_Pred_Type. \ No newline at end of file
+Require Export Classical_Pred_Type.
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 08babda9..8317f6bb 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -5,7 +5,7 @@
(* // * 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*)
+(*i $Id: Decidable.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Properties of decidable propositions *)
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 2b982963..3e94deda 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*)
+(*i $Id: Diaconescu.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
(** R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
@@ -59,18 +59,18 @@ Qed.
Require Import ChoiceFacts.
-Variable rel_choice : RelationalChoice.
+Variable rel_choice : forall A B:Type, RelationalChoice A B.
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,
+ 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).
+ apply
+ (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
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 24905039..2fe9d1a6 100755..100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -6,183 +6,29 @@
(* * 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*)
+(*i $Id: Eqdep.v 8642 2006-03-17 10:09:02Z notin $ 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
+(** This file axiomatizes the invariance by substitution of reflexive
+ equality proofs [[Streicher93]] and exports its consequences, such
+ as the injectivity of the projection of the dependent pair.
- - 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
+ [[Streicher93]] T. Streicher, Semantical Investigations into
+ Intensional Type Theory, Habilitationsschrift, LMU München, 1993.
*)
-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.
+Require Export EqdepFacts.
-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 *)
+Module Eq_rect_eq.
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.
+ forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
-(** UIP implies the injectivity of equality on dependent pairs *)
+End Eq_rect_eq.
-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.
+Module EqdepTheory := EqdepTheory(Eq_rect_eq).
+Export EqdepTheory.
-(** The main results to be exported *)
+(** Exported hints *)
-Hint Resolve eq_dep_intro eq_dep_eq: core v62.
-Hint Immediate eq_dep_sym: core v62.
+Hint Resolve eq_dep_eq: core v62.
Hint Resolve inj_pair2 inj_pairT2: core.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
new file mode 100644
index 00000000..7963555a
--- /dev/null
+++ b/theories/Logic/EqdepFacts.v
@@ -0,0 +1,351 @@
+(************************************************************************)
+(* 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: EqdepFacts.v 8674 2006-03-30 06:56:50Z herbelin $ i*)
+
+(** This file defines dependent equality and shows its equivalence with
+ equality on dependent pairs (inhabiting sigma-types). It derives
+ the consequence of axiomatizing 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
+
+Table of contents:
+
+A. Definition of dependent equality and equivalence with equality
+
+B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
+
+C. Definition of the functor that builds properties of dependent
+ equalities assuming axiom eq_rect_eq
+
+*)
+
+(************************************************************************)
+(** *** A. Definition of dependent equality and equivalence with equality of dependent pairs *)
+
+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_refl : forall (p:U) (x:P p), eq_dep p x p x.
+Proof eq_dep_intro.
+
+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.
+
+(** Equivalent definition of dependent equality expressed as a non
+ dependent inductive type *)
+
+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.
+
+End Dependent_Equality.
+
+Implicit Arguments eq_dep [U P].
+Implicit Arguments eq_dep1 [U P].
+
+(** Dependent equality is equivalent to equality on dependent pairs *)
+
+Lemma eq_sigS_eq_dep :
+ 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 p x q y.
+Proof.
+ intros.
+ dependent rewrite H.
+ apply eq_dep_intro.
+Qed.
+
+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 p x q y.
+Proof.
+split.
+ (* -> *)
+ apply eq_sigS_eq_dep.
+ (* <- *)
+ destruct 1; reflexivity.
+Qed.
+
+Lemma eq_sigT_eq_dep :
+ forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+ existT P p x = existT P q y -> eq_dep p x q y.
+Proof.
+ intros.
+ dependent rewrite H.
+ apply eq_dep_intro.
+Qed.
+
+Lemma eq_dep_eq_sigT :
+ forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+ eq_dep p x q y -> existT P p x = existT P q y.
+Proof.
+ destruct 1; reflexivity.
+Qed.
+
+(** Exported hints *)
+
+Hint Resolve eq_dep_intro: core v62.
+Hint Immediate eq_dep_sym: core v62.
+
+(************************************************************************)
+(** *** B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K *)
+
+Section Equivalences.
+
+Variable U:Type.
+
+(** Invariance by Substitution of Reflexive Equality Proofs *)
+
+Definition 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 *)
+
+Definition Eq_dep_eq :=
+ forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.
+
+(** Uniqueness of Identity Proofs (UIP) *)
+
+Definition UIP_ :=
+ forall (x y:U) (p1 p2:x = y), p1 = p2.
+
+(** Uniqueness of Reflexive Identity Proofs *)
+
+Definition UIP_refl_ :=
+ forall (x:U) (p:x = x), p = refl_equal x.
+
+(** Streicher's axiom K *)
+
+Definition Streicher_K_ :=
+ forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+
+(** Injectivity of Dependent Equality is a consequence of *)
+(** Invariance by Substitution of Reflexive Equality Proof *)
+
+Lemma eq_rect_eq__eq_dep1_eq :
+ Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
+Proof.
+ intro eq_rect_eq.
+ simple destruct 1; intro.
+ rewrite <- eq_rect_eq; auto.
+Qed.
+
+Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
+Proof.
+ intros eq_rect_eq; red; intros.
+ apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial.
+Qed.
+
+(** Uniqueness of Identity Proofs (UIP) is a consequence of *)
+(** Injectivity of Dependent Equality *)
+
+Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
+Proof.
+ intro eq_dep_eq; red.
+ 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__UIP_refl : UIP_ -> UIP_refl_.
+Proof.
+ intro UIP; red; intros; apply UIP.
+Qed.
+
+(** Streicher's axiom K is a direct consequence of Uniqueness of
+ Reflexive Identity Proofs *)
+
+Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.
+Proof.
+ intro UIP_refl; red; intros; rewrite UIP_refl; assumption.
+Qed.
+
+(** We finally recover from K the Invariance by Substitution of
+ Reflexive Equality Proofs *)
+
+Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
+Proof.
+ intro Streicher_K; red; intros.
+ apply Streicher_K with (p := h).
+ reflexivity.
+Qed.
+
+(** Remark: It is reasonable to think that [eq_rect_eq] is strictly
+ stronger than [eq_rec_eq] (which is [eq_rect_eq] restricted on [Set]):
+
+ [Definition Eq_rec_eq :=
+ forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.]
+
+ Typically, [eq_rect_eq] allows to prove UIP and Streicher's K what
+ does not seem possible with [eq_rec_eq]. In particular, the proof of [UIP]
+ requires to use [eq_rect_eq] on [fun y -> x=y] which is in [Type] but not
+ in [Set].
+*)
+
+End Equivalences.
+
+Section Corollaries.
+
+Variable U:Type.
+Variable V:Set.
+
+(** UIP implies the injectivity of equality on dependent pairs in Type *)
+
+Definition Inj_dep_pairT :=
+ forall (P:U -> Type) (p:U) (x y:P p),
+ existT P p x = existT P p y -> x = y.
+
+Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT.
+ Proof.
+ intro eq_dep_eq; red; intros.
+ apply eq_dep_eq.
+ apply eq_sigT_eq_dep.
+ assumption.
+ Qed.
+
+(** UIP implies the injectivity of equality on dependent pairs in Set *)
+
+Definition Inj_dep_pairS :=
+ forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y.
+
+Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS.
+Proof.
+ intro eq_dep_eq; red; intros.
+ apply eq_dep_eq.
+ apply eq_sigS_eq_dep.
+ assumption.
+Qed.
+
+End Corollaries.
+
+(************************************************************************)
+(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
+
+Module Type EqdepElimination.
+
+ Axiom eq_rect_eq :
+ forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
+ x = eq_rect p Q x p h.
+
+End EqdepElimination.
+
+Module EqdepTheory (M:EqdepElimination).
+
+Section Axioms.
+
+Variable U:Type.
+
+(** Invariance by Substitution of Reflexive Equality Proofs *)
+
+Lemma eq_rect_eq :
+ forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+Proof M.eq_rect_eq U.
+
+Lemma eq_rec_eq :
+ forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+Proof (fun p Q => M.eq_rect_eq U p Q).
+
+(** Injectivity of Dependent Equality *)
+
+Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.
+Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
+
+(** Uniqueness of Identity Proofs (UIP) is a consequence of *)
+(** Injectivity of Dependent Equality *)
+
+Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
+Proof (eq_dep_eq__UIP U eq_dep_eq).
+
+(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
+
+Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+Proof (UIP__UIP_refl U UIP).
+
+(** Streicher's axiom K is a direct consequence of Uniqueness of
+ Reflexive Identity Proofs *)
+
+Lemma Streicher_K :
+ forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+Proof (UIP_refl__Streicher_K U UIP_refl).
+
+End Axioms.
+
+(** UIP implies the injectivity of equality on dependent pairs in Type *)
+
+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 (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)).
+
+(** UIP implies the injectivity of equality on dependent pairs in Set *)
+
+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 (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)).
+
+End EqdepTheory.
+
+Implicit Arguments eq_dep [].
+Implicit Arguments eq_dep1 [].
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 7caf403c..7d71a1a6 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,56 +6,43 @@
(* * 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*)
+(*i $Id: Eqdep_dec.v 8136 2006-03-05 21:57:47Z herbelin $ 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.
+(** 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
+ 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
-*)
+ Credit: Proofs up to [K_dec] follow an outline by Michael Hedberg
+Table of contents:
-(** We need some dependent elimination schemes *)
+A. Streicher's K and injectivity of dependent pair hold on decidable types
-Set Implicit Arguments.
+B.1. Definition of the functor that builds properties of dependent equalities
+ from a proof of decidability of equality for a set in Type
- (** 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.
+B.2. Definition of the functor that builds properties of dependent equalities
+ from a proof of decidability of equality for a set in Set
- 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.
+(************************************************************************)
+(** *** A. Streicher's K and injectivity of dependent pair hold on decidable types *)
+Set Implicit Arguments.
-Section DecidableEqDep.
+Section EqdepDec.
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.
+ Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = refl_equal y.
intros.
case u; trivial.
Qed.
@@ -89,7 +76,7 @@ Qed.
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.
+apply trans_sym_eq.
Qed.
@@ -108,7 +95,6 @@ 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 :=
@@ -138,21 +124,173 @@ case H.
reflexivity.
Qed.
-End DecidableEqDep.
+End EqdepDec.
+
+Require Import EqdepFacts.
+
+ (** We deduce axiom [K] for (decidable) types *)
+ Theorem K_dec_type :
+ forall A:Type,
+ (forall x y:A, {x = y} + {x <> y}) ->
+ forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+intros A eq_dec x P H p.
+elim p using K_dec; intros.
+case (eq_dec x0 y); [left|right]; assumption.
+trivial.
+Qed.
- (** 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.
+ Proof fun A => K_dec_type (A:=A).
+
+ (** We deduce the [eq_rect_eq] axiom for (decidable) types *)
+ Theorem eq_rect_eq_dec :
+ forall A:Type,
+ (forall x y:A, {x = y} + {x <> y}) ->
+ forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+intros A eq_dec.
+apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
+Qed.
-right; red in |- *; intro neq; apply n; elim neq; reflexivity.
+Unset Implicit Arguments.
-trivial.
-Qed. \ No newline at end of file
+(************************************************************************)
+(** *** B.1. Definition of the functor that builds properties of dependent equalities on decidable sets in Type *)
+
+(** The signature of decidable sets in [Type] *)
+
+Module Type DecidableType.
+
+ Parameter U:Type.
+ Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
+
+End DecidableType.
+
+(** The module [DecidableEqDep] collects equality properties for decidable
+ set in [Type] *)
+
+Module DecidableEqDep (M:DecidableType).
+
+ Import M.
+
+ (** Invariance by Substitution of Reflexive Equality Proofs *)
+
+ Lemma eq_rect_eq :
+ forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+ Proof eq_rect_eq_dec eq_dec.
+
+ (** Injectivity of Dependent Equality *)
+
+ Theorem eq_dep_eq :
+ forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
+ Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
+
+ (** Uniqueness of Identity Proofs (UIP) *)
+
+ Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
+ Proof (eq_dep_eq__UIP U eq_dep_eq).
+
+ (** Uniqueness of Reflexive Identity Proofs *)
+
+ Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+ Proof (UIP__UIP_refl U UIP).
+
+ (** Streicher's axiom K *)
+
+ Lemma Streicher_K :
+ forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+ Proof (K_dec_type eq_dec).
+
+ (** Injectivity of equality on dependent pairs in [Type] *)
+
+ Lemma inj_pairT2 :
+ forall (P:U -> Type) (p:U) (x y:P p),
+ existT P p x = existT P p y -> x = y.
+ Proof eq_dep_eq__inj_pairT2 U eq_dep_eq.
+
+ (** Proof-irrelevance on subsets of decidable sets *)
+
+ Lemma inj_pairP2 :
+ forall (P:U -> Prop) (x:U) (p q:P x),
+ ex_intro P x p = ex_intro P x q -> p = q.
+ intros.
+ apply inj_right_pair with (A:=U).
+ intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
+ assumption.
+ Qed.
+
+End DecidableEqDep.
+
+(************************************************************************)
+(** *** B.2 Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
+
+(** The signature of decidable sets in [Set] *)
+
+Module Type DecidableSet.
+
+ Parameter U:Set.
+ Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
+
+End DecidableSet.
+
+(** The module [DecidableEqDepSet] collects equality properties for decidable
+ set in [Set] *)
+
+Module DecidableEqDepSet (M:DecidableSet).
+
+ Import M.
+ Module N:=DecidableEqDep(M).
+
+ (** Invariance by Substitution of Reflexive Equality Proofs *)
+
+ Lemma eq_rect_eq :
+ forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+ Proof eq_rect_eq_dec eq_dec.
+
+ (** Injectivity of Dependent Equality *)
+
+ Theorem eq_dep_eq :
+ forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
+ Proof N.eq_dep_eq.
+
+ (** Uniqueness of Identity Proofs (UIP) *)
+
+ Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
+ Proof N.UIP.
+
+ (** Uniqueness of Reflexive Identity Proofs *)
+
+ Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+ Proof N.UIP_refl.
+
+ (** Streicher's axiom K *)
+
+ Lemma Streicher_K :
+ forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+ Proof N.Streicher_K.
+
+ (** Injectivity of equality on dependent pairs with second component
+ in [Type] *)
+
+ Lemma inj_pairT2 :
+ forall (P:U -> Type) (p:U) (x y:P p),
+ existT P p x = existT P p y -> x = y.
+ Proof N.inj_pairT2.
+
+ (** Proof-irrelevance on subsets of decidable sets *)
+
+ Lemma inj_pairP2 :
+ forall (P:U -> Prop) (x:U) (p q:P x),
+ ex_intro P x p = ex_intro P x q -> p = q.
+ Proof N.inj_pairP2.
+
+ (** Injectivity of equality on dependent pairs in [Set] *)
+
+ Lemma inj_pair2 :
+ forall (P:U -> Set) (p:U) (x y:P p),
+ existS P p x = existS P p y -> x = y.
+ Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
+
+End DecidableEqDepSet.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 4666d9b4..4d365e32 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: JMeq.v,v 1.8.2.2 2004/08/03 17:42:32 herbelin Exp $ i*)
+(*i $Id: JMeq.v 6009 2004-08-03 17:42:55Z herbelin $ i*)
-(** John Major's Equality as proposed by C. Mc Bride
+(** John Major's Equality as proposed by Conor McBride
Reference:
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index afdc0ffe..44ab9a2e 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -6,109 +6,13 @@
(* * 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.
+(** This file axiomatizes proof-irrelevance and derives some consequences *)
- Since, dependent elimination is derivable in the Calculus of
- Inductive Constructions (CCI), we get proof-irrelevance from classical
- logic in the CCI.
+Require Import ProofIrrelevanceFacts.
- Reference:
+Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
- - [Coquand] T. Coquand, "Metamathematical Investigations of a
- Calculus of Constructions", Proceedings of Logic in Computer Science
- (LICS'90), 1990.
+Module PI. Definition proof_irrelevance := proof_irrelevance. End PI.
- 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
-*)
+Module ProofIrrelevanceTheory := ProofIrrelevanceTheory(PI).
+Export ProofIrrelevanceTheory.
diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v
new file mode 100644
index 00000000..dd3178eb
--- /dev/null
+++ b/theories/Logic/ProofIrrelevanceFacts.v
@@ -0,0 +1,62 @@
+(************************************************************************)
+(* 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 defines the functor that build consequences of proof-irrelevance *)
+
+Require Export EqdepFacts.
+
+Module Type ProofIrrelevance.
+
+ Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
+
+End ProofIrrelevance.
+
+Module ProofIrrelevanceTheory (M:ProofIrrelevance).
+
+ (** Proof-irrelevance implies uniqueness of reflexivity proofs *)
+
+ Module Eq_rect_eq.
+ Lemma eq_rect_eq :
+ forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
+ x = eq_rect p Q x p h.
+ Proof.
+ intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=refl_equal p).
+ reflexivity.
+ Qed.
+ End Eq_rect_eq.
+
+ (** Export the theory of injective dependent elimination *)
+
+ Module EqdepTheory := EqdepTheory(Eq_rect_eq).
+ Export EqdepTheory.
+
+ Scheme eq_indd := Induction for eq Sort Prop.
+
+ (** We derive the irrelevance of the membership property for subsets *)
+
+ Lemma subset_eq_compat :
+ forall (U:Set) (P:U->Prop) (x y:U) (p:P x) (q:P y),
+ x = y -> exist P x p = exist P y q.
+ Proof.
+ intros.
+ rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
+ elim H using eq_indd.
+ reflexivity.
+ Qed.
+
+ Lemma subsetT_eq_compat :
+ forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y),
+ x = y -> existT P x p = existT P y q.
+ Proof.
+ intros.
+ rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
+ elim H using eq_indd.
+ reflexivity.
+ Qed.
+
+End ProofIrrelevanceTheory.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 08873aa5..11979057 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RelationalChoice.v,v 1.3.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
+(*i $Id: RelationalChoice.v 6001 2004-08-01 09:27:26Z herbelin $ i*)
(** This file axiomatizes the relational form of the axiom of choice *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 19:51:39 +0000