Library sTactic




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

Theorem Contradict2 : forall a b : Prop, b -> ~ b -> a.
intuition.
Qed.

Theorem Contradict3 : forall a : Prop, a -> ~ ~ a.
auto.
Qed.

Ltac Contradict name :=
  (apply (fun a : Prop => Contradict1 a _ name); clear name; intros name) ||
    (apply (fun a : Prop => Contradict2 a _ name); clear name);
   try apply Contradict3.


Ltac CaseEq name :=
  generalize (refl_equal name); pattern name at -1 in |- *; case name.

Ltac Casec name := case name; clear name.

Ltac Elimc name := elim name; clear name.
Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (4 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (3 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

Global Index

C

Contradict1 [lemma, in sTactic]
Contradict2 [lemma, in sTactic]
Contradict3 [lemma, in sTactic]


S

sTactic [library]



Lemma Index

C

Contradict1 [in sTactic]
Contradict2 [in sTactic]
Contradict3 [in sTactic]



Library Index

S

sTactic



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (4 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (3 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

This page has been generated by coqdoc