diff options
author | Robert Sloan <varomodt@gmail.com> | 2016-06-22 14:06:28 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 14:06:28 -0400 |
commit | 2f44fe53e1a598b524e11cda3dc9ce7a04534247 (patch) | |
tree | 47a77eb4ed8fea3ac5ec99c5bf5ad9131ba44fd9 /coqprime-8.5/Coqprime/Tactic.v | |
parent | e101fc5dd8783d029d7a4933c7ccca4a67ed3874 (diff) | |
parent | 3d8afe1c9bd905e3a62523e87a2aa7e5d9f5093d (diff) |
Merge with plv/master
Diffstat (limited to 'coqprime-8.5/Coqprime/Tactic.v')
-rw-r--r-- | coqprime-8.5/Coqprime/Tactic.v | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/coqprime-8.5/Coqprime/Tactic.v b/coqprime-8.5/Coqprime/Tactic.v new file mode 100644 index 000000000..93a244149 --- /dev/null +++ b/coqprime-8.5/Coqprime/Tactic.v @@ -0,0 +1,84 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + + +(********************************************************************** + Tactic.v + Useful tactics + **********************************************************************) + +(************************************** + A simple tactic to end a proof +**************************************) +Ltac finish := intros; auto; trivial; discriminate. + + +(************************************** + A tactic for proof by contradiction + with contradict H + H: ~A |- B gives |- A + H: ~A |- ~ B gives H: B |- A + H: A |- B gives |- ~ A + H: A |- B gives |- ~ A + H: A |- ~ B gives H: A |- ~ A +**************************************) + +Ltac contradict name := + let term := type of name in ( + match term with + (~_) => + match goal with + |- ~ _ => let x := fresh in + (intros x; case name; + generalize x; clear x name; + intro name) + | |- _ => case name; clear name + end + | _ => + match goal with + |- ~ _ => let x := fresh in + (intros x; absurd term; + [idtac | exact name]; generalize x; clear x name; + intros name) + | |- _ => generalize name; absurd term; + [idtac | exact name]; clear name + end + end). + + +(************************************** + A tactic to do case analysis keeping the equality +**************************************) + +Ltac case_eq name := + generalize (refl_equal name); pattern name at -1 in |- *; case name. + + +(************************************** + A tactic to use f_equal? theorems +**************************************) + +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) + | |- (?g _ _ = ?g _ _) => apply f_equal2 with (f := g) + | |- (?g ?X ?Y _ = ?g ?X ?Y _) => apply f_equal with (f := g X Y) + | |- (?g ?X _ _ = ?g ?X _ _) => apply f_equal2 with (f := g X) + | |- (?g _ _ _ = ?g _ _ _) => apply f_equal3 with (f := g) + | |- (?g ?X ?Y ?Z _ = ?g ?X ?Y ?Z _) => apply f_equal with (f := g X Y Z) + | |- (?g ?X ?Y _ _ = ?g ?X ?Y _ _) => apply f_equal2 with (f := g X Y) + | |- (?g ?X _ _ _ = ?g ?X _ _ _) => apply f_equal3 with (f := g X) + | |- (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g) + end. + +(************************************** + A stupid tactic that tries auto also after applying sym_equal +**************************************) + +Ltac sauto := (intros; apply sym_equal; auto; fail) || auto. |