sTactic.v

(**************************************************************************** IEEE754 : sTactic Laurent Thery ***************************************************************************** My favorite tactics *)

Theorem Contradict1: (a, b:Prop) b -> (a ->~ b) ->~ a.
Intuition.
Qed.

Theorem Contradict2: (a, b:Prop) b -> ~ b ->a.
Intuition.
Qed.

Theorem Contradict3: (a:Prop) a ->~ (~ a).
Auto.
Qed.

Tactic Definition Contradict [$a] :=
[<:tactic:<
(Apply [a:Prop](Contradict1 a ? $a); Clear $a; Intros $a)
Orelse (Apply [a:Prop](Contradict2 a ? $a); Clear $a); Try Apply Contradict3
>>].

Tactic Definition CaseEq [$a] :=
[<:tactic:< Generalize (refl_equal ? $a); Pattern -1 $a; Case $a >>].

Tactic Definition Casec [$a] :=
[<:tactic:< Case $a; Clear $a >>].

Tactic Definition Elimc [$a] :=
[<:tactic:< Elim $a; Clear $a >>].