Utility Ltac tactics.
Require Import Bool.
Ltac dauto :=
auto with datatypes.
Ltac deauto :=
eauto with datatypes.
Tactic Notation "
refl" :=
reflexivity.
Tactic Notation "
asmp" :=
assumption.
Tactic Notation "
contra" :=
contradiction.
Tactic Notation "
cong" :=
congruence.
Tactic Notation "
disc" :=
discriminate.
Ltac inv H :=
inversion H;
clear H;
subst.
Ltac false_invert_tactic :=
match goal with H:
_ |-
_ =>
solve [
inversion H
|
clear H;
false_invert_tactic
|
fail 2 ]
end.
Tactic Notation "
false_invert" :=
false_invert_tactic.
Ltac nsolve :=
solve [
contradiction |
congruence |
tauto |
false_invert].
Ltac boolrw :=
match goal with
| [ |- ?
G ] =>
match G with
|
context [
_ &&
_ =
true ] =>
rewrite andb_true_iff;
boolrw
|
context [
_ &&
_ =
false ] =>
rewrite andb_false_iff;
boolrw
|
context [
_ ||
_ =
true ] =>
rewrite orb_true_iff;
boolrw
|
context [
_ ||
_ =
false ] =>
rewrite orb_false_iff;
boolrw
|
context [
negb _ =
true ] =>
rewrite negb_true_iff;
boolrw
|
context [
negb _ =
false ] =>
rewrite negb_false_iff;
boolrw
end
| [
H : ?
X |-
_ ] =>
match X with
|
context [
_ &&
_ =
true ] =>
rewrite andb_true_iff in H;
boolrw
|
context [
_ &&
_ =
false ] =>
rewrite andb_false_iff in H;
boolrw
|
context [
_ ||
_ =
true ] =>
rewrite orb_true_iff in H;
boolrw
|
context [
_ ||
_ =
false ] =>
rewrite orb_false_iff in H;
boolrw
|
context [
negb _ =
true ] =>
rewrite negb_true_iff;
boolrw
|
context [
negb _ =
false ] =>
rewrite negb_false_iff;
boolrw
end
|
_ =>
idtac
end.
Ltac trim :=
try nsolve.
Ltac simpls :=
simpl in *.
Tactic Notation "
inv"
constr(
H) :=
inversion H;
clear H;
subst.
Tactic Notation "
inv"
constr(
H) "
as"
simple_intropattern(
L) :=
inversion H as L;
clear H;
subst.
Tactic Notation "
gen"
constr(
H) :=
generalize H;
intro.
Tactic Notation "
gen"
constr(
H) "
as"
simple_intropattern(
Name) :=
generalize H;
intro Name.
Tactic Notation "
dec_destruct"
constr(
H) :=
generalize H;
let H' :=
fresh in intro H';
destruct H'.
Tactic Notation "
dec_destruct"
constr(
H) "
as"
simple_intropattern(
Name) :=
generalize H;
let H' :=
fresh in intro H';
destruct H'
as Name.
Tactic Notation "
introsv" :=
intros until 0.
Tactic Notation "
introsv"
simple_intropattern(
I1) :=
introsv;
intros I1.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2) :=
introsv I1;
introsv I2.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3) :=
introsv I1;
introsv I2 I3.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4) :=
introsv I1;
introsv I2 I3 I4.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5) :=
introsv I1;
introsv I2 I3 I4 I5.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6) :=
introsv I1;
introsv I2 I3 I4 I5 I6.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6)
simple_intropattern(
I7) :=
introsv I1;
introsv I2 I3 I4 I5 I6 I7.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6)
simple_intropattern(
I7)
simple_intropattern(
I8) :=
introsv I1;
introsv I2 I3 I4 I5 I6 I7 I8.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6)
simple_intropattern(
I7)
simple_intropattern(
I8)
simple_intropattern(
I9) :=
introsv I1;
introsv I2 I3 I4 I5 I6 I7 I8 I9.
Tactic Notation "
introsv"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6)
simple_intropattern(
I7)
simple_intropattern(
I8)
simple_intropattern(
I9)
simple_intropattern(
I10) :=
introsv I1;
introsv I2 I3 I4 I5 I6 I7 I8 I9 I10.
Require Import Omega.
Require Import Psatz.
Ltac lia2 :=
zify;
unfold Zsucc in *;
lia.
Tactic Notation "
dup"
constr(
H) :=
assert (
H);
trivial.
Require String.
Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
|
H :
_ |-
_ =>
try move x after H
end.
Tactic Notation "
assert_eq"
ident(
x)
constr(
v) :=
let H :=
fresh in
assert (
x =
v)
as H by reflexivity;
clear H.
Tactic Notation "
Case_aux"
ident(
x)
constr(
name) :=
first [
set (
x :=
name);
move_to_top x
|
assert_eq x name;
move_to_top x
|
fail 1 "
because we are working on a different case" ].
Ltac Case name :=
Case_aux Case name.
Ltac SCase name :=
Case_aux SCase name.
Ltac SSCase name :=
Case_aux SSCase name.
Ltac SSSCase name :=
Case_aux SSSCase name.
Ltac SSSSCase name :=
Case_aux SSSSCase name.
Ltac SSSSSCase name :=
Case_aux SSSSSCase name.
Ltac SSSSSSCase name :=
Case_aux SSSSSSCase name.
Ltac SSSSSSSCase name :=
Case_aux SSSSSSSCase name.
Ltac simpl_hyps :=
match goal with
| [
H1: ?
a -> ?
b,
H2: ?
a |-
_ ] =>
let H3 :=
fresh in assert (
H3:
b)
by tauto;
clear H1;
rename H3 into H1
end.
Tactic Notation "
dup "
hyp(
OldH)
ident(
NewH) :=
generalize OldH;
intro NewH.
Ltac clear_dup :=
match goal with
| [
H : ?
X |-
_ ] =>
match goal with
| [
H' : ?
Y |-
_ ] =>
match H with
|
H' =>
fail 2
|
_ =>
unify X Y ; (
clear H' ||
clear H)
end
end
end.
Ltac clear_dups :=
repeat clear_dup.
Tactic Notation "
decs "
hyp(
H) :=
decompose [
ex and or]
H;
clear H.
Ltac gendep H :=
generalize dependent H.
Tactic Notation "
case_match"
constr(
C) "
as"
simple_intropattern(
N) :=
case_eq C;
introsv N;
rewrite N.
Tactic Notation "
case_match"
constr(
C) "
as"
simple_intropattern(
N) "
in"
hyp(
H) :=
case_eq C;
introsv N;
rewrite N in H.
Require Import Coq.Bool.Bool.
Tactic Notation "
split" "&&" :=
rewrite andb_true_iff;
split.
Tactic Notation "
destruct" "&&"
hyp(
H) :=
rewrite andb_true_iff in H;
destruct H.
Require Import Errors.
Ltac optDecG :=
match goal with
| [ |- ?
G ] =>
match G with
|
context [
if ?
x then _ else _] =>
destruct x
|
context [
match ?
x with
|
left _ =>
_
|
right _ =>
_
end] =>
destruct x
|
context [
match ?
x with
|
Some _ =>
_
|
None =>
_
end] =>
destruct x
|
context [
match ?
x with
|
OK _ =>
_
|
Error _ =>
_
end] =>
destruct x
|
context [
match ?
x with
|
nil =>
_
|
cons _ _ =>
_
end] =>
destruct x
end
end.
Ltac optDecGN N :=
match goal with
| [ |- ?
G ] =>
match G with
|
context [
if ?
x then _ else _] =>
case_eq x;
introsv N
|
context [
match ?
x with
|
left _ =>
_
|
right _ =>
_
end] =>
case_eq x;
introsv N
|
context [
match ?
x with
|
Some _ =>
_
|
None =>
_
end] =>
case_eq x;
introsv N
|
context [
match ?
x with
|
OK _ =>
_
|
Error _ =>
_
end] =>
case_eq x;
introsv N
|
context [
match ?
x with
|
nil =>
_
|
cons _ _ =>
_
end] =>
case_eq x;
introsv N
end
end.
Ltac rw :=
match goal with
| [ |- ?
G ] =>
match G with
|
context [
if ?
x then _ else _] =>
match goal with
| [
H:
x =
_ |-
_ ] =>
rewrite H
end
|
context [
match ?
x with
|
left _ =>
_
|
right _ =>
_
end] =>
match goal with
| [
H:
x =
_ |-
_ ] =>
rewrite H
end
|
context [
match ?
x with
|
Some _ =>
_
|
None =>
_
end] =>
match goal with
| [
H:
x =
_ |-
_ ] =>
rewrite H
end
|
context [
match ?
x with
|
OK _ =>
_
|
Error _ =>
_
end] =>
match goal with
| [
H:
x =
_ |-
_ ] =>
rewrite H
end
end
end.
Ltac rws H :=
rewrite H in *.
Ltac optDec H :=
match type of H with
|
context [
if ?
x then _ else _] =>
destruct x
|
context [
match ?
x with
|
left _ =>
_
|
right _ =>
_
end] =>
destruct x
|
context [
match ?
x with
|
Some _ =>
_
|
None =>
_
end] =>
destruct x
|
context [
match ?
x with
|
OK _ =>
_
|
Error _ =>
_
end] =>
destruct x
|
context [
match ?
x with
|
nil =>
_
|
cons _ _ =>
_
end] =>
destruct x
end.
Ltac optDecN H N :=
match type of H with
|
context [
if ?
x then _ else _] =>
case_match x as N in H
|
context [
match ?
x with
|
left _ =>
_
|
right _ =>
_
end] =>
case_match x as N in H
|
context [
match ?
x with
|
Some _ =>
_
|
None =>
_
end] =>
case_match x as N in H
|
context [
match ?
x with
|
OK _ =>
_
|
Error _ =>
_
end] =>
case_match x as N in H
|
context [
match ?
x with
|
nil =>
_
|
cons _ _ =>
_
end] =>
case_match x as N in H
end.
Imported from Software Foundations
get_head E is a tactic that returns the head constant of the
term E, ie, when applied to a term of the form P x1 ... xN
it returns P. If E is not an application, it returns E.
Warning: the tactic seems to loop in some cases when the goal is
a product and one uses the result of this function.
Ltac get_head E :=
match E with
| ?
P _ _ _ _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ =>
constr:(
P)
| ?
P _ _ =>
constr:(
P)
| ?
P _ =>
constr:(
P)
| ?
P =>
constr:(
P)
end.
unfolds unfolds the head definition in the goal, i.e. if the
goal has form P x1 ... xN then it calls unfold P.
If the goal is an equality, it tries to unfold the head constant
on the left-hand side, and otherwise tries on the right-hand side.
If the goal is a product, it calls intros first.
Ltac apply_to_head_of E cont :=
let go E :=
let P :=
get_head E in cont P in
match E with
|
forall _,
_ =>
intros;
apply_to_head_of E cont
| ?
A = ?
B =>
first [
go A |
go B ]
| ?
A =>
go A
end.
Ltac unfolds_base :=
match goal with |- ?
G =>
apply_to_head_of G ltac:(
fun P =>
unfold P)
end.
Tactic Notation "
unfolds" :=
unfolds_base.
unfolds in H unfolds the head definition of hypothesis H, i.e. if
H has type P x1 ... xN then it calls unfold P in H.
Ltac unfolds_in_base H :=
match type of H with ?
G =>
apply_to_head_of G ltac:(
fun P =>
unfold P in H)
end.
Tactic Notation "
unfolds" "
in"
hyp(
H) :=
unfolds_in_base H.
unfolds P1,..,PN is a shortcut for unfold P1,..,PN in *.
Tactic Notation "
unfolds"
reference(
F1) :=
unfold F1 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2) :=
unfold F1,
F2 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2)
","
reference(
F3) :=
unfold F1,
F2,
F3 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2)
","
reference(
F3) ","
reference(
F4) :=
unfold F1,
F2,
F3,
F4 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2)
","
reference(
F3) ","
reference(
F4) ","
reference(
F5) :=
unfold F1,
F2,
F3,
F4,
F5 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2)
","
reference(
F3) ","
reference(
F4) ","
reference(
F5) ","
reference(
F6) :=
unfold F1,
F2,
F3,
F4,
F5,
F6 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2)
","
reference(
F3) ","
reference(
F4) ","
reference(
F5)
","
reference(
F6) ","
reference(
F7) :=
unfold F1,
F2,
F3,
F4,
F5,
F6,
F7 in *.
Tactic Notation "
unfolds"
reference(
F1) ","
reference(
F2)
","
reference(
F3) ","
reference(
F4) ","
reference(
F5)
","
reference(
F6) ","
reference(
F7) ","
reference(
F8) :=
unfold F1,
F2,
F3,
F4,
F5,
F6,
F7,
F8 in *.
Ltac projInv H :=
unfolds in H;
optDec H;
trim.
Tactic Notation "
substs" :=
repeat (
match goal with H: ?
x = ?
y |-
_ =>
first [
subst x |
subst y ]
end).
Tactic Notation "
generalizes"
hyp(
X) :=
generalize X;
clear X.
Tactic Notation "
generalizes"
hyp(
X1)
hyp(
X2) :=
generalizes X1;
generalizes X2.
Tactic Notation "
generalizes"
hyp(
X1)
hyp(
X2)
hyp(
X3) :=
generalizes X1 X2;
generalizes X3.
Tactic Notation "
generalizes"
hyp(
X1)
hyp(
X2)
hyp(
X3)
hyp(
X4) :=
generalizes X1 X2 X3;
generalizes X4.
Ltac substs_below limit :=
match goal with H: ?
T |-
_ =>
match T with
|
limit =>
idtac
| ?
x = ?
y =>
first [
subst x;
substs_below limit
|
subst y;
substs_below limit
|
generalizes H;
substs_below limit;
intro ]
end end.
Ltac invs H :=
inversion H;
clear H;
substs.
Tactic Notation "
inv_clear"
constr(
H) :=
inversion H;
clear H.
Tactic Notation "
inv_clear"
constr(
H) "
as"
simple_intropattern(
L) :=
inversion H as L;
clear H.