diff options
Diffstat (limited to 'theories7/Logic/ProofIrrelevance.v')
-rw-r--r-- | theories7/Logic/ProofIrrelevance.v | 113 |
1 files changed, 0 insertions, 113 deletions
diff --git a/theories7/Logic/ProofIrrelevance.v b/theories7/Logic/ProofIrrelevance.v deleted file mode 100644 index 3f031ff7..00000000 --- a/theories7/Logic/ProofIrrelevance.v +++ /dev/null @@ -1,113 +0,0 @@ -(************************************************************************) -(* 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 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 -*) |