diff options
Diffstat (limited to 'theories7/Logic/ClassicalFacts.v')
-rw-r--r-- | theories7/Logic/ClassicalFacts.v | 214 |
1 files changed, 214 insertions, 0 deletions
diff --git a/theories7/Logic/ClassicalFacts.v b/theories7/Logic/ClassicalFacts.v new file mode 100644 index 00000000..1d37652e --- /dev/null +++ b/theories7/Logic/ClassicalFacts.v @@ -0,0 +1,214 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: ClassicalFacts.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ i*) + +(** Some facts and definitions about classical logic *) + +(** [prop_degeneracy] (also referred as propositional completeness) *) +(* asserts (up to consistency) that there are only two distinct formulas *) +Definition prop_degeneracy := (A:Prop) A==True \/ A==False. + +(** [prop_extensionality] asserts equivalent formulas are equal *) +Definition prop_extensionality := (A,B:Prop) (A<->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 BoolP := (C:Prop)C->C->C. +Definition TrueP := [C][c1,c2]c1 : BoolP. +Definition FalseP := [C][c1,c2]c2 : BoolP. +Definition BoolP_elim := [C][c1,c2][b:BoolP](b C c1 c2). +Definition BoolP_elim_redl : (C:Prop)(c1,c2:C)c1==(BoolP_elim C c1 c2 TrueP) + := [C;c1,c2](refl_eqT C c1). +Definition BoolP_elim_redr : (C:Prop)(c1,c2:C)c2==(BoolP_elim C c1 c2 FalseP) + := [C;c1,c2](refl_eqT C c2). + +Definition BoolP_dep_induction := + (P:BoolP->Prop)(P TrueP)->(P FalseP)->(b:BoolP)(P b). + +Lemma ext_prop_dep_proof_irrel_cc : + prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. +Proof (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim + BoolP_elim_redl BoolP_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 boolP : Prop := trueP : boolP | falseP : boolP. +Definition boolP_elim_redl : (C:Prop)(c1,c2:C)c1==(boolP_ind C c1 c2 trueP) + := [C;c1,c2](refl_eqT C c1). +Definition boolP_elim_redr : (C:Prop)(c1,c2:C)c2==(boolP_ind C c1 c2 falseP) + := [C;c1,c2](refl_eqT C c2). +Scheme boolP_indd := Induction for boolP Sort Prop. + +Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. +Proof [pe](ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind + boolP_elim_redl boolP_elim_redr pe boolP_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. +*) |