diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rwxr-xr-x | theories/Logic/Classical.v | 3 | ||||
| -rwxr-xr-x | theories/Logic/Classical_Prop.v | 13 |
3 files changed, 16 insertions, 2 deletions
@@ -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 |