diff options
author | 2003-11-29 17:28:49 +0000 | |
---|---|---|
committer | 2003-11-29 17:28:49 +0000 | |
commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Logic/Decidable.v | |
parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) |
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Decidable.v')
-rw-r--r-- | theories/Logic/Decidable.v | 54 |
1 files changed, 28 insertions, 26 deletions
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 82464b3af..ebc21f755 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -9,50 +9,52 @@ (** Properties of decidable propositions *) -Definition decidable := [P:Prop] P \/ ~P. +Definition decidable (P:Prop) := P \/ ~ P. -Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P. -Unfold decidable; Tauto. +Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P. +unfold decidable in |- *; tauto. Qed. -Theorem dec_True: (decidable True). -Unfold decidable; Auto. +Theorem dec_True : decidable True. +unfold decidable in |- *; auto. Qed. -Theorem dec_False: (decidable False). -Unfold decidable not; Auto. +Theorem dec_False : decidable False. +unfold decidable, not in |- *; auto. Qed. -Theorem dec_or: (A,B:Prop)(decidable A) -> (decidable B) -> (decidable (A\/B)). -Unfold decidable; Tauto. +Theorem dec_or : + forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B). +unfold decidable in |- *; tauto. Qed. -Theorem dec_and: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A/\B)). -Unfold decidable; Tauto. +Theorem dec_and : + forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B). +unfold decidable in |- *; tauto. Qed. -Theorem dec_not: (A:Prop)(decidable A) -> (decidable ~A). -Unfold decidable; Tauto. +Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A). +unfold decidable in |- *; tauto. Qed. -Theorem dec_imp: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A->B)). -Unfold decidable; Tauto. +Theorem dec_imp : + forall A B:Prop, decidable A -> decidable B -> decidable (A -> B). +unfold decidable in |- *; tauto. Qed. -Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P. -Unfold decidable; Tauto. Qed. +Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. +unfold decidable in |- *; tauto. Qed. -Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B. -Tauto. Qed. +Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B. +tauto. Qed. -Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B. -Unfold decidable; Tauto. Qed. +Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B. +unfold decidable in |- *; tauto. Qed. -Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B. -Unfold decidable;Tauto. +Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B. +unfold decidable in |- *; tauto. Qed. -Theorem imp_simp : (A,B:Prop) (decidable A) -> (A -> B) -> ~A \/ B. -Unfold decidable; Tauto. +Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B. +unfold decidable in |- *; tauto. Qed. - |