Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2712 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 204 insertions, 1 deletions

diff --git a/Makefile b/Makefile
index 33d5bc5460..b933ce3cc9 100644
--- a/Makefile
+++ b/Makefile
@@ -380,7 +380,8 @@ states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTIC
 clean::
 	rm -f states/*.coq
 
-LOGICVO=theories/Logic/Classical.vo          theories/Logic/Classical_Type.vo \
+LOGICVO=theories/Logic/Hurkens.vo          theories/Logic/ProofIrrelevance.vo\
+      theories/Logic/Classical.vo          theories/Logic/Classical_Type.vo \
       theories/Logic/Classical_Pred_Set.vo   theories/Logic/Eqdep.vo          \
       theories/Logic/Classical_Pred_Type.vo  theories/Logic/Classical_Prop.vo \
       theories/Logic/Berardi.vo       	     theories/Logic/Eqdep_dec.vo \
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 539eb4dcbd..0a5987d012 100755
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -10,6 +10,8 @@
 
 (** Classical Propositional Logic *)
 
+Require ProofIrrelevance.
+
 Hints Unfold not : core.
 
 Axiom classic: (P:Prop)(P \/ ~(P)).
@@ -78,3 +80,6 @@ Lemma imply_and_or2: (P,Q,R:Prop)(P->Q) -> P \/ R -> Q \/ R.
 Proof.
 Induction 2; Auto.
 Qed.
+
+Lemma proof_irrelevance: (P:Prop)(p1,p2:P)p1==p2.
+Proof (proof_irrelevance_cci classic).
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
new file mode 100644
index 0000000000..0cb2ef5da5
--- /dev/null
+++ b/theories/Logic/Hurkens.v
@@ -0,0 +1,79 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                            Projet LogiCal                                *)
+(*                                                                          *)
+(*                     INRIA                        LRI-CNRS                *)
+(*              Rocquencourt                        Orsay                   *)
+(*                                                                          *)
+(*                              May 29th 2002                               *)
+(*                                                                          *)
+(****************************************************************************)
+(*                                Hurkens.v                                 *)
+(****************************************************************************)
+
+(** This is Hurkens paradox [Hurkens] in system U-, adapted by Herman
+    Geuvers [Geuvers] to show the inconsistency in the pure calculus of
+    constructions of a retract from Prop into a small type.
+
+    References:
+
+    - [Hurkens] A. J. Hurkens, "A simplification of Girard's paradox",
+      Proceedings of the 2nd international conference Typed Lambda-Calculi
+      and Applications (TLCA'95), 1995.
+
+    - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001
+      (see www.cs.kun.nl/~herman/note.ps.gz).
+*)
+
+Section Paradox.
+
+Variable bool : Prop.
+Variable p2b : Prop -> bool.     
+Variable b2p : bool -> Prop.
+Hypothesis p2p1 : (A:Prop)(b2p (p2b A))->A.
+Hypothesis p2p2 : (A:Prop)A->(b2p (p2b A)).
+Variable B:Prop.
+
+Definition V := (A:Prop)((A->bool)->(A->bool))->(A->bool).
+Definition U := V->bool.
+Definition sb : V -> V := [z][A;r;a](r (z A r) a).
+Definition le : (U->bool)->(U->bool) := [i][x](x [A;r;a](i [v](sb v A r a))).
+Definition induct : (U->bool)->Prop := [i](x:U)(b2p (le i x))->(b2p (i x)).
+Definition WF : U := [z](p2b (induct (z U le))).
+Definition I : U->Prop :=
+  [x]((i:U->bool)(b2p (le i x))->(b2p (i [v](sb v U le x))))->B.
+
+Lemma Omega : (i:U->bool)(induct i)->(b2p (i WF)).
+Intros i y.
+Apply y.
+Unfold le WF induct.
+Apply p2p2.
+Intros x H0.
+Apply y.
+Exact H0.
+Qed.
+
+Lemma lemma : (induct [u](p2b (I u))).
+Unfold induct.
+Intros x p.
+Apply (p2p2 (I x)).
+Intro q.
+Apply (p2p1 (I [v:V](sb v U le x)) (q [u](p2b (I u)) p)).
+Intro i.
+Apply q with i:=[y:?](i [v:V](sb v U le y)).
+Qed.
+
+Lemma lemma2 : ((i:U->bool)(induct i)->(b2p (i WF)))->B.
+Intro x.
+Apply (p2p1 (I WF) (x [u](p2b (I u)) lemma)).
+Intros i H0.
+Apply (x [y](i [v](sb v U le y))).
+Apply (p2p1 ? H0).
+Qed.
+
+Lemma paradox : B.
+Exact (lemma2 Omega).
+Qed.
+
+End Paradox.
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
new file mode 100644
index 0000000000..5435ba5329
--- /dev/null
+++ b/theories/Logic/ProofIrrelevance.v
@@ -0,0 +1,118 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                            Projet LogiCal                                *)
+(*                                                                          *)
+(*                     INRIA                        LRI-CNRS                *)
+(*              Rocquencourt                        Orsay                   *)
+(*                                                                          *)
+(*                              May 29th 2002                               *)
+(*                                                                          *)
+(****************************************************************************)
+(*                                Hurkens.v                                 *)
+(****************************************************************************)
+(** This section shows in the pure Calculus of Construction that
+    classical logic + dependent elimination of disjunction entails
+    proof-irrelevance.
+
+    Since, dependent elimination is derivable in the Calculus of
+    Inductive Constructions (CCI), we get proof-irrelevance from classical
+    logic in the CCI.
+
+    Reference:
+
+    - [Coquand] T. Coquand, "Metamathematical Investigations of a
+      Calculus of Constructions", Proceedings of Logic in Computer Science
+      (LICS'90), 1990.
+
+   Proof skeleton: classical logic + dependent elimination of
+   disjunction + discrimination of proofs implies the existence of a
+   retract from Prop into bool, hence inconsistency by encoding any
+   paradox of system U- (e.g. Hurkens' paradox).
+*)
+
+Require Hurkens.
+
+Section Proof_irrelevance_CC.
+
+Variable or : Prop -> Prop -> Prop.
+Variable or_introl : (A,B:Prop)A->(or A B).
+Variable or_intror : (A,B:Prop)B->(or A B).
+Hypothesis or_elim : (A,B:Prop)(C:Prop)(A->C)->(B->C)->(or A B)->C.
+Hypothesis or_elim_redl :
+  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(a:A)
+  (f a)==(or_elim A B C f g (or_introl A B a)).
+Hypothesis or_elim_redr :
+  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(b:B)
+  (g b)==(or_elim A B C f g (or_intror A B b)).
+Hypothesis or_dep_elim :
+ (A,B:Prop)(P:(or A B)->Prop)
+ ((a:A)(P (or_introl A B a))) ->
+ ((b:B)(P (or_intror A B b))) -> (b:(or A B))(P b).
+
+Hypothesis em : (A:Prop)(or A ~A).
+Variable B : Prop.
+Variable b1,b2 : B.
+
+(** [p2b] and [b2p] form a retract if [~b1==b2] *)
+
+Definition p2b [A] := (or_elim A ~A B [_]b1 [_]b2 (em A)).
+Definition b2p [b] := b1==b.
+
+Lemma p2p1 : (A:Prop) A -> (b2p (p2b A)).
+Proof.
+  Unfold p2b; Intro A; Apply or_dep_elim with b:=(em A); Unfold b2p; Intros.
+  Apply (or_elim_redl A ~A B [_]b1 [_]b2).
+  NewDestruct (b H).
+Qed.
+Lemma p2p2 :  ~b1==b2->(A:Prop) (b2p (p2b A)) -> A.
+Proof.
+  Intro not_eq_b1_b2.
+  Unfold p2b; Intro A; Apply or_dep_elim with b:=(em A); Unfold b2p; Intros.
+  Assumption.
+  NewDestruct not_eq_b1_b2.
+  Rewrite <- (or_elim_redr A ~A B [_]b1 [_]b2) in H.
+  Assumption.
+Qed.
+
+(** Using excluded-middle a second time, we get proof-irrelevance *)
+
+Theorem proof_irrelevance_cc : b1==b2.
+Proof.
+  Refine (or_elim ? ? ? ? ? (em b1==b2));Intro H.
+    Trivial.
+  Apply (paradox B p2b b2p (p2p2 H) p2p1).
+Qed.
+
+End Proof_irrelevance_CC.
+
+
+(** The Calculus of Inductive Constructions (CCI) enjoys dependent
+    elimination, hence classical logic in CCI entails proof-irrelevance.
+*)
+
+Section Proof_irrelevance_CCI.
+
+Hypothesis em : (A:Prop) A \/ ~A.
+
+Definition or_elim_redl :
+  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(a:A)
+  (f a)==(or_ind A B C f g (or_introl A B a))
+  := [A,B,C;f;g;a](refl_eqT C (f a)).
+Definition or_elim_redr :
+  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(b:B)
+  (g b)==(or_ind A B C f g (or_intror A B b))
+  := [A,B,C;f;g;b](refl_eqT C (g b)).
+Scheme or_indd := Induction for or Sort Prop.
+
+Theorem proof_irrelevance_cci : (B:Prop)(b1,b2:B)b1==b2.
+Proof
+  (proof_irrelevance_cc or or_introl or_intror or_ind
+     or_elim_redl or_elim_redr or_indd em).
+
+End Proof_irrelevance_CCI.
+
+(** Remark: in CCI, [bool] can be taken in [Set] as well in the
+    paradox and since [~true=false] for [true] and [false] in
+    [bool], we get the inconsistency of [em : (A:Prop){A}+{~A}] in CCI
+*)