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/Decidable.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Logic/Decidable.v')
-rw-r--r-- | theories/Logic/Decidable.v | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v new file mode 100644 index 00000000..08babda9 --- /dev/null +++ b/theories/Logic/Decidable.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* 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: Decidable.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) + +(** Properties of decidable propositions *) + +Definition decidable (P:Prop) := P \/ ~ P. + +Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P. +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_True : decidable True. +unfold decidable in |- *; auto. +Qed. + +Theorem dec_False : decidable False. +unfold decidable, not in |- *; auto. +Qed. + +Theorem dec_or : + forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B). +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_and : + forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B). +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A). +unfold decidable in |- *; tauto. +Qed. + +Theorem dec_imp : + forall A B:Prop, decidable A -> decidable B -> decidable (A -> B). +unfold decidable in |- *; tauto. +Qed. + +Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. +unfold decidable in |- *; tauto. Qed. + +Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B. +tauto. Qed. + +Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B. +unfold decidable in |- *; tauto. Qed. + +Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B. +unfold decidable in |- *; tauto. +Qed. + +Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B. +unfold decidable in |- *; tauto. +Qed. |