From bc4e7b8c2317b2536eb42efb7cbf37d748ceb7c6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 13 Aug 2002 13:40:48 +0000 Subject: Preuves dans CC de MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit dégénérescence des propositions <-> tiers-exclu /\ extensionnalité propositionnelle et dans CCI de extensionnalité propositionnelle -> indiscernabilité des preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2960 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/ClassicalFacts.v | 215 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 215 insertions(+) create mode 100644 theories/Logic/ClassicalFacts.v (limited to 'theories/Logic') diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v new file mode 100644 index 000000000..44f09c265 --- /dev/null +++ b/theories/Logic/ClassicalFacts.v @@ -0,0 +1,215 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* B) -> A==B. + +(** [excluded_middle] asserts we can reason by case on the truth *) +(* or falsity of any formula *) +Definition excluded_middle := (A:Prop) A \/ ~A. + +(** [proof_irrelevance] asserts equality of all proofs of a given formula *) +Definition proof_irrelevance := (A:Prop)(a1,a2:A) a1==a2. + +(** We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *) + +Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality. +Proof. +Intros H A B (Hab,Hba). +NewDestruct (H A); NewDestruct (H B). + Rewrite H1; Exact H0. + Absurd B. + Rewrite H1; Exact [H]H. + Apply Hab; Rewrite H0; Exact I. + Absurd A. + Rewrite H0; Exact [H]H. + Apply Hba; Rewrite H1; Exact I. + Rewrite H1; Exact H0. +Qed. + +Lemma prop_degen_em : prop_degeneracy -> excluded_middle. +Proof. +Intros H A. +NewDestruct (H A). + Left; Rewrite H0; Exact I. + Right; Rewrite H0; Exact [x]x. +Qed. + +Lemma prop_ext_em_degen : + prop_extensionality -> excluded_middle -> prop_degeneracy. +Proof. +Intros Ext EM A. +NewDestruct (EM A). + Left; Apply (Ext A True); Split; [Exact [_]I | Exact [_]H]. + Right; Apply (Ext A False); Split; [Exact H | Apply False_ind]. +Qed. + +(** We successively show that: + + [prop_extensionality] + implies equality of [A] and [A->A] for inhabited [A], which + implies the existence of a (trivial) retract from [A->A] to [A] + (just take the identity), which + implies the existence of a fixpoint operator in [A] + (e.g. take the Y combinator of lambda-calculus) +*) + +Definition inhabited [A:Prop] := A. + +Lemma prop_ext_A_eq_A_imp_A : + prop_extensionality->(A:Prop)(inhabited A)->(A->A)==A. +Proof. +Intros Ext A a. +Apply (Ext A->A A); Split; [ Exact [_]a | Exact [_;_]a ]. +Qed. + +Record retract [A,B:Prop] : Prop := { + f1: A->B; + f2: B->A; + f1_o_f2: (x:B)(f1 (f2 x))==x +}. + +Lemma prop_ext_retract_A_A_imp_A : + prop_extensionality->(A:Prop)(inhabited A)->(retract A A->A). +Proof. +Intros Ext A a. +Rewrite -> (prop_ext_A_eq_A_imp_A Ext A a). +Exists [x:A]x [x:A]x. +Reflexivity. +Qed. + +Record has_fixpoint [A:Prop] : Prop := { + F : (A->A)->A; + fix : (f:A->A)(F f)==(f (F f)) +}. + +Lemma ext_prop_fixpoint : + prop_extensionality->(A:Prop)(inhabited A)->(has_fixpoint A). +Proof. +Intros Ext A a. +Case (prop_ext_retract_A_A_imp_A Ext A a); Intros g1 g2 g1_o_g2. +Exists [f]([x:A](f (g1 x x)) (g2 [x](f (g1 x x)))). +Intro f. +Pattern 1 (g1 (g2 [x:A](f (g1 x x)))). +Rewrite (g1_o_g2 [x:A](f (g1 x x))). +Reflexivity. +Qed. + +(** Assume we have booleans with the property that there is at most 2 + booleans (which is equivalent to dependent case analysis). Consider + the fixpoint of the negation function: it is either true or false by + dependent case analysis, but also the opposite by fixpoint. Hence + proof-irrelevance. + + We then map bool proof-irrelevance to all propositions. +*) + +Section Proof_irrelevance_gen. + +Variable bool : Prop. +Variable true : bool. +Variable false : bool. +Hypothesis bool_elim : (C:Prop)C->C->bool->C. +Hypothesis bool_elim_redl : (C:Prop)(c1,c2:C)c1==(bool_elim C c1 c2 true). +Hypothesis bool_elim_redr : (C:Prop)(c1,c2:C)c2==(bool_elim C c1 c2 false). +Local bool_dep_induction := (P:bool->Prop)(P true)->(P false)->(b:bool)(P b). + +Lemma aux : prop_extensionality -> bool_dep_induction -> true==false. +Proof. +Intros Ext Ind. +Case (ext_prop_fixpoint Ext bool true); Intros G Gfix. +Pose neg := [b:bool](bool_elim bool false true b). +Generalize (refl_eqT ? (G neg)). +Pattern 1 (G neg). +Apply Ind with b:=(G neg); Intro Heq. +Rewrite (bool_elim_redl bool false true). +Change true==(neg true); Rewrite -> Heq; Apply Gfix. +Rewrite (bool_elim_redr bool false true). +Change (neg false)==false; Rewrite -> Heq; Symmetry; Apply Gfix. +Qed. + +Lemma ext_prop_dep_proof_irrel_gen : + prop_extensionality -> bool_dep_induction -> proof_irrelevance. +Proof. +Intros Ext Ind A a1 a2. +Pose f := [b:bool](bool_elim A a1 a2 b). +Rewrite (bool_elim_redl A a1 a2). +Change (f true)==a2. +Rewrite (bool_elim_redr A a1 a2). +Change (f true)==(f false). +Rewrite (aux Ext Ind). +Reflexivity. +Qed. + +End Proof_irrelevance_gen. + +(** In the pure Calculus of Constructions, we can define the boolean + proposition bool = (C:Prop)C->C->C but we cannot prove that it has at + most 2 elements. +*) + +Section Proof_irrelevance_CC. + +Definition Bool := (C:Prop)C->C->C. +Definition True := [C][c1,c2]c1 : Bool. +Definition False := [C][c1,c2]c2 : Bool. +Definition Bool_elim := [C][c1,c2][b:Bool](b C c1 c2). +Definition Bool_elim_redl : (C:Prop)(c1,c2:C)c1==(Bool_elim C c1 c2 True) + := [C;c1,c2](refl_eqT C c1). +Definition Bool_elim_redr : (C:Prop)(c1,c2:C)c2==(Bool_elim C c1 c2 False) + := [C;c1,c2](refl_eqT C c2). + +Definition Bool_dep_induction := + (P:Bool->Prop)(P True)->(P False)->(b:Bool)(P b). + +Lemma ext_prop_dep_proof_irrel_cc : + prop_extensionality -> Bool_dep_induction -> proof_irrelevance. +Proof (ext_prop_dep_proof_irrel_gen Bool True False Bool_elim + Bool_elim_redl Bool_elim_redr). + +End Proof_irrelevance_CC. + +(** In the Calculus of Inductive Constructions, inductively defined booleans + enjoy dependent case analysis, hence directly proof-irrelevance from + propositional extensionality. +*) + +Section Proof_irrelevance_CIC. + +Inductive bool : Prop := true : bool | false : bool. +Definition bool_elim_redl : (C:Prop)(c1,c2:C)c1==(bool_ind C c1 c2 true) + := [C;c1,c2](refl_eqT C c1). +Definition bool_elim_redr : (C:Prop)(c1,c2:C)c2==(bool_ind C c1 c2 false) + := [C;c1,c2](refl_eqT C c2). +Scheme bool_indd := Induction for bool Sort Prop. + +Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. +Proof [pe](ext_prop_dep_proof_irrel_gen bool true false bool_ind + bool_elim_redl bool_elim_redr pe bool_indd). + +End Proof_irrelevance_CIC. + +(** Can we state proof irrelevance from propositional degeneracy + (i.e. propositional extensionality + excluded middle) without + dependent case analysis ? + + Conjecture: it seems possible to build a model of CC interpreting + all non-empty types by the set of all lambda-terms. Such a model would + satisfy propositional degeneracy without satisfying proof-irrelevance + (nor dependent case analysis). This would imply that the previous + results cannot be refined. +*) + -- cgit v1.2.3