1 files changed, 6 insertions, 102 deletions
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.