diff options
Diffstat (limited to 'coqprime/Coqprime/Tactic.v')
| -rw-r--r-- | coqprime/Coqprime/Tactic.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/coqprime/Coqprime/Tactic.v b/coqprime/Coqprime/Tactic.v index 93a244149..b0f8f4f28 100644 --- a/coqprime/Coqprime/Tactic.v +++ b/coqprime/Coqprime/Tactic.v @@ -8,19 +8,19 @@ (********************************************************************** - Tactic.v - Useful tactics + Tactic.v + Useful tactics **********************************************************************) (************************************** - A simple tactic to end a proof + A simple tactic to end a proof **************************************) Ltac finish := intros; auto; trivial; discriminate. (************************************** A tactic for proof by contradiction - with contradict H + with contradict H H: ~A |- B gives |- A H: ~A |- ~ B gives H: B |- A H: A |- B gives |- ~ A @@ -28,19 +28,19 @@ Ltac finish := intros; auto; trivial; discriminate. H: A |- ~ B gives H: A |- ~ A **************************************) -Ltac contradict name := +Ltac contradict name := let term := type of name in ( - match term with - (~_) => - match goal with + match term with + (~_) => + match goal with |- ~ _ => let x := fresh in - (intros x; case name; + (intros x; case name; generalize x; clear x name; intro name) | |- _ => case name; clear name end - | _ => - match goal with + | _ => + match goal with |- ~ _ => let x := fresh in (intros x; absurd term; [idtac | exact name]; generalize x; clear x name; @@ -60,10 +60,10 @@ Ltac case_eq name := (************************************** - A tactic to use f_equal? theorems + A tactic to use f_equal? theorems **************************************) -Ltac eq_tac := +Ltac eq_tac := match goal with |- (?g _ = ?g _) => apply f_equal with (f := g) | |- (?g ?X _ = ?g ?X _) => apply f_equal with (f := g X) @@ -77,7 +77,7 @@ Ltac eq_tac := | |- (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g) end. -(************************************** +(************************************** A stupid tactic that tries auto also after applying sym_equal **************************************) |