diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 09:14:53 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 09:14:53 +0000 |
commit | f292b6df725fdd8615ae75452b118376d2f0fe21 (patch) | |
tree | 6725de58ab89c059bea71afd13f19873558bba33 /theories/Logic/ProofIrrelevance.v | |
parent | 34e53d5418fa08e69c8f599bb55a89eae027b9b5 (diff) |
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
Diffstat (limited to 'theories/Logic/ProofIrrelevance.v')
-rw-r--r-- | theories/Logic/ProofIrrelevance.v | 118 |
1 files changed, 118 insertions, 0 deletions
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v new file mode 100644 index 000000000..5435ba532 --- /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 +*) |