From 14e850d63d17d9a7094a23d2a59ca9f968b5976a Mon Sep 17 00:00:00 2001 From: narboux Date: Fri, 15 Jul 2005 15:27:42 +0000 Subject: add a left and right tactic for classical logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 2 ++ theories/Logic/Classical.v | 3 ++- theories/Logic/Classical_Prop.v | 13 ++++++++++++- 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 8369a25850..dcd395e68a 100644 --- a/CHANGES +++ b/CHANGES @@ -45,6 +45,8 @@ Tactics - Added "autorewrite with ... in hyp [using ...]" (doc TODO). - Added entry constr_may_eval for tactic extensions (new syntax). - Fixed a "fold" bug (non critical and possible source of incompatibilities). +- Added classical_left and classical_right which transforms |- A \/ B into + ~B |- A and ~A |- B respectively. Modules diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 9dd9d4d913..1c2b97ce76 100755 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -11,4 +11,5 @@ (** Classical Logic *) Require Export Classical_Prop. -Require Export Classical_Pred_Type. \ No newline at end of file +Require Export Classical_Pred_Type. + diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index fa509a3c02..1df6a354bd 100755 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -82,4 +82,15 @@ simple induction 2; auto. Qed. Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. -Proof proof_irrelevance_cci classic. \ No newline at end of file +Proof proof_irrelevance_cci classic. + +(* classical_left transforms |- A \/ B into ~B |- A *) +(* classical_right transforms |- A \/ B into ~A |- B *) + +Ltac classical_right := match goal with + | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +end. + +Ltac classical_left := match goal with +| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +end. \ No newline at end of file -- cgit v1.2.3