diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Logic/ProofIrrelevance.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Logic/ProofIrrelevance.v')
-rw-r--r-- | theories/Logic/ProofIrrelevance.v | 114 |
1 files changed, 114 insertions, 0 deletions
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v new file mode 100644 index 00000000..afdc0ffe --- /dev/null +++ b/theories/Logic/ProofIrrelevance.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* 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 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 +*) |