diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-21 18:42:22 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-21 18:42:22 +0000 |
commit | 40183da6b54d8deef242bac074079617d4a657c2 (patch) | |
tree | 4e70870a5b1e36ba65965f6e87cd8141d01d8d75 /theories/Logic/Classical_Prop.v | |
parent | 249c6b5e1e2d00549dde9093e134df2f25a68609 (diff) |
gros commit de tout ce que j'ai fait pendant les vacances :
- tactics/Equality
- debug du discharge
- constr_of_compattern implante vite fait / mal fait en attendant mieux
- theories/Logic (ne passe pas entierrement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Classical_Prop.v')
-rwxr-xr-x | theories/Logic/Classical_Prop.v | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v new file mode 100755 index 000000000..f9afd26b0 --- /dev/null +++ b/theories/Logic/Classical_Prop.v @@ -0,0 +1,73 @@ + +(* $Id$ *) + +(* Classical Propositional Logic *) + +Hints Unfold not : core. + +Axiom classic: (P:Prop)(P \/ ~(P)). + +Lemma NNPP : (p:Prop)~(~(p))->p. +Proof. +Unfold not; Intros; Elim (classic p); Auto. +Intro NP; Elim (H NP). +Qed. + +Lemma not_imply_elim : (P,Q:Prop)~(P->Q)->P. +Proof. +Intros; Apply NNPP; Red. +Intro; Apply H; Intro; Absurd P; Trivial. +Qed. + +Lemma not_imply_elim2 : (P,Q:Prop)~(P->Q) -> ~Q. +Proof. +Intros; Elim (classic Q); Auto. +Qed. + +Lemma imply_to_or : (P,Q:Prop)(P->Q) -> ~P \/ Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma imply_to_and : (P,Q:Prop)~(P->Q) -> P /\ ~Q. +Proof. +Intros; Split. +Apply not_imply_elim with Q; Trivial. +Apply not_imply_elim2 with P; Trivial. +Qed. + +Lemma or_to_imply : (P,Q:Prop)(~P \/ Q) -> P->Q. +Proof. +Induction 1; Auto. +Intros H1 H2; Elim (H1 H2). +Qed. + +Lemma not_and_or : (P,Q:Prop)~(P/\Q)-> ~P \/ ~Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma or_not_and : (P,Q:Prop)(~P \/ ~Q) -> ~(P/\Q). +Proof. +Induction 1; Red; Induction 2; Auto. +Qed. + +Lemma not_or_and : (P,Q:Prop)~(P\/Q)-> ~P /\ ~Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma and_not_or : (P,Q:Prop)(~P /\ ~Q) -> ~(P\/Q). +Proof. +Induction 1; Red; Induction 3; Trivial. +Qed. + +Lemma imply_and_or: (P,Q:Prop)(P->Q) -> P \/ Q -> Q. +Proof. +Induction 2; Trivial. +Qed. + +Lemma imply_and_or2: (P,Q,R:Prop)(P->Q) -> P \/ R -> Q \/ R. +Proof. +Induction 2; Auto. +Qed. |