Library GenTacs
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
This file contains generic tactics for making the proofs more concise. Some of these
are truly generic e.g. eliminating conjunctions, others are more speicialised for this
development.
Require Import Arith.
Turn a < into a <=.
Ltac ltToLe H := apply le_S in H; apply le_S_n in H.
Adds H to the context.
Ltac addHyp H := generalize H; intro.
Adds H to the context as Q
Ltac addHypAs H Q := generalize H; intro Q.
Inverts and then clears a hypothesis.
Ltac invertClear H := inversion H; clear H.
Ltac swapRename A B := let H := fresh in rename A into H; rename B into A; rename H into B.
Ltac introz U := repeat let H := fresh U in intro H.
Ltac appDisj H := destruct H; try apply H.
Ltac doappsnd t H := t;[ | apply H].
Ltac swapRename A B := let H := fresh in rename A into H; rename B into A; rename H into B.
Ltac introz U := repeat let H := fresh U in intro H.
Ltac appDisj H := destruct H; try apply H.
Ltac doappsnd t H := t;[ | apply H].
If the hypothesis in question is invertible into exactly one other hypothesis, then
this tactic changes the current hypothesis to the inverted hypothesis. It does this by a
regular inversion, then a clear, then a rename.
Ltac invertChange H := let IVC := fresh in inversion H as [IVC];
clear H; rename IVC into H.
Ltac unwrap_apply2 d := let x := fresh in let y := fresh in
destruct d as [x y]; apply y.
Ltac unwrap2_apply2 d := let x := fresh in destruct d as [x];
unwrap_apply2 x.
Ltac replace_nontriv x y := first [is_evar x |
(replace x with y; [ |try reflexivity])].
Ltac my_applys_eq1 H :=
match goal with
| [ |- ?F ?x1] =>
match type of H with
| (?G ?y1) =>
replace_nontriv x1 y1
end;
[apply H |..]
end.
Ltac my_applys_eq2 H :=
match goal with
| [ |- ?F ?x1 ?x2] =>
match type of H with
| (?G ?y1 ?y2) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq3 H :=
match goal with
| [ |- ?F ?x1 ?x2 ?x3] =>
match type of H with
| (?G ?y1 ?y2 ?y3) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..];
[replace_nontriv x3 y3 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq4 H :=
match goal with
| [ |- ?F ?x1 ?x2 ?x3 ?x4] =>
match type of H with
| (?G ?y1 ?y2 ?y3 ?y4) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..];
[replace_nontriv x3 y3 | ..]; [replace_nontriv x4 y4 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq5 H :=
match goal with
| [ |- ?F ?x1 ?x2 ?x3 ?x4 ?x5] =>
match type of H with
| (?G ?y1 ?y2 ?y3 ?y4 ?y5) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..];
[replace_nontriv x3 y3 | ..]; [replace_nontriv x4 y4 | ..];
[replace_nontriv x5 y5 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq H := first [my_applys_eq5 H | my_applys_eq4 H |
my_applys_eq3 H | my_applys_eq2 H | my_applys_eq1 H].
Ltac invertClearAs1 H U := inversion H as [U]; clear H.
Ltac invertClearAs2 H U V := inversion H as [U V]; clear H.
Ltac invertClearAs3 H U V W := inversion H as [U V W]; clear H.
Ltac invertClearAs4 H U V W X := inversion H as [U V W X]; clear H.
Ltac elim_intro H H1 H2 := elim H; [intro H1 | intro H2]; clear H.
Ltac decompOr3 P P1 P2 P3 := let H := fresh in elim_intro P P1 H;[ |
elim_intro H P2 P3].
Ltac elimOr2 P U := let U1 := fresh U in elim_intro P U1 U1.
Ltac elimOr3 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr2 H U].
Ltac elimOr4 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr3 H U].
Ltac elimOr5 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr4 H U].
Ltac elimOr6 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr5 H U].
Ltac decompAnd2 H H1 H2 := elim H; intros H1 H2; clear H.
Ltac decompAnd3 H H1 H2 H3 := let Q := fresh in elim H; intros H1 Q; clear H;
decompAnd2 Q H2 H3.
Ltac and_flat_step W :=
let V1 := fresh W in
let V2 := fresh W in
match goal with
[ H : ?P /\ ?Q |- _] => decompAnd2 H V1 V2
end.
Ltac andflat W := repeat and_flat_step W.
Ltac decompEx2 H a b Q := let H1 := fresh in invertClearAs2 H a H1;
invertClearAs2 H1 b Q.
Ltac decompEx3 H a b c Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx2 H1 b c Q.
Ltac decompEx4 H a b c d Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx3 H1 b c d Q.
Ltac decompEx5 H a b c d e Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx4 H1 b c d e Q.
Ltac decompEx6 H a b c d e f Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx5 H1 b c d e f Q.
Ltac dofirst2 t := t;[t |..].
Ltac dofirst3 t := t;[dofirst2 t |..].
Ltac dofirst4 t := t;[dofirst3 t |..].
Ltac dofirst5 t := t;[dofirst4 t |..].
Ltac dofirst6 t := t;[dofirst5 t |..].
Ltac decompExAnd H x H1 H2 := let Q := fresh in destruct H as [x Q]; decompAnd2 Q H1 H2.
Ltac unfold_somewhere f :=
first [progress unfold f |
match goal with [U : context[f] |- _] =>
unfold f in U end].
clear H; rename IVC into H.
Ltac unwrap_apply2 d := let x := fresh in let y := fresh in
destruct d as [x y]; apply y.
Ltac unwrap2_apply2 d := let x := fresh in destruct d as [x];
unwrap_apply2 x.
Ltac replace_nontriv x y := first [is_evar x |
(replace x with y; [ |try reflexivity])].
Ltac my_applys_eq1 H :=
match goal with
| [ |- ?F ?x1] =>
match type of H with
| (?G ?y1) =>
replace_nontriv x1 y1
end;
[apply H |..]
end.
Ltac my_applys_eq2 H :=
match goal with
| [ |- ?F ?x1 ?x2] =>
match type of H with
| (?G ?y1 ?y2) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq3 H :=
match goal with
| [ |- ?F ?x1 ?x2 ?x3] =>
match type of H with
| (?G ?y1 ?y2 ?y3) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..];
[replace_nontriv x3 y3 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq4 H :=
match goal with
| [ |- ?F ?x1 ?x2 ?x3 ?x4] =>
match type of H with
| (?G ?y1 ?y2 ?y3 ?y4) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..];
[replace_nontriv x3 y3 | ..]; [replace_nontriv x4 y4 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq5 H :=
match goal with
| [ |- ?F ?x1 ?x2 ?x3 ?x4 ?x5] =>
match type of H with
| (?G ?y1 ?y2 ?y3 ?y4 ?y5) =>
replace_nontriv x1 y1; [replace_nontriv x2 y2 | ..];
[replace_nontriv x3 y3 | ..]; [replace_nontriv x4 y4 | ..];
[replace_nontriv x5 y5 | ..]
end;
[apply H |..]
end.
Ltac my_applys_eq H := first [my_applys_eq5 H | my_applys_eq4 H |
my_applys_eq3 H | my_applys_eq2 H | my_applys_eq1 H].
Ltac invertClearAs1 H U := inversion H as [U]; clear H.
Ltac invertClearAs2 H U V := inversion H as [U V]; clear H.
Ltac invertClearAs3 H U V W := inversion H as [U V W]; clear H.
Ltac invertClearAs4 H U V W X := inversion H as [U V W X]; clear H.
Ltac elim_intro H H1 H2 := elim H; [intro H1 | intro H2]; clear H.
Ltac decompOr3 P P1 P2 P3 := let H := fresh in elim_intro P P1 H;[ |
elim_intro H P2 P3].
Ltac elimOr2 P U := let U1 := fresh U in elim_intro P U1 U1.
Ltac elimOr3 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr2 H U].
Ltac elimOr4 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr3 H U].
Ltac elimOr5 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr4 H U].
Ltac elimOr6 P U := let H := fresh in let U1 := fresh U in
elim_intro P U1 H;[ | elimOr5 H U].
Ltac decompAnd2 H H1 H2 := elim H; intros H1 H2; clear H.
Ltac decompAnd3 H H1 H2 H3 := let Q := fresh in elim H; intros H1 Q; clear H;
decompAnd2 Q H2 H3.
Ltac and_flat_step W :=
let V1 := fresh W in
let V2 := fresh W in
match goal with
[ H : ?P /\ ?Q |- _] => decompAnd2 H V1 V2
end.
Ltac andflat W := repeat and_flat_step W.
Ltac decompEx2 H a b Q := let H1 := fresh in invertClearAs2 H a H1;
invertClearAs2 H1 b Q.
Ltac decompEx3 H a b c Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx2 H1 b c Q.
Ltac decompEx4 H a b c d Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx3 H1 b c d Q.
Ltac decompEx5 H a b c d e Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx4 H1 b c d e Q.
Ltac decompEx6 H a b c d e f Q := let H1 := fresh in invertClearAs2 H a H1;
decompEx5 H1 b c d e f Q.
Ltac dofirst2 t := t;[t |..].
Ltac dofirst3 t := t;[dofirst2 t |..].
Ltac dofirst4 t := t;[dofirst3 t |..].
Ltac dofirst5 t := t;[dofirst4 t |..].
Ltac dofirst6 t := t;[dofirst5 t |..].
Ltac decompExAnd H x H1 H2 := let Q := fresh in destruct H as [x Q]; decompAnd2 Q H1 H2.
Ltac unfold_somewhere f :=
first [progress unfold f |
match goal with [U : context[f] |- _] =>
unfold f in U end].
Used to solve the goal which is an inequality between two objects.
Ltac neq_inversion := unfold not; let Q := fresh in intro Q; inversion Q.
Ltac eassertArg Y := let P := fresh in
evar (P:Prop); assert P as Y;[unfold P; clear P
| unfold P in Y; clear P].
Ltac eassert := let H := fresh in eassertArg H.
Tactic Notation "eassert" "as" ident(Y) := eassertArg Y.
Ltac genDep2 x1 x2 := generalize dependent x1; generalize dependent x2.
Ltac genDep3 x1 x2 x3 := genDep2 x1 x2; generalize dependent x3.
Ltac genDep4 x1 x2 x3 x4:= genDep3 x1 x2 x3; generalize dependent x4.
Ltac genDep5 a b c d e := genDep4 a b c d; generalize dependent e.
Ltac uncurry_aux H := intro H; intros; apply H;
repeat (split;[assumption | ]); assumption.
Ltac uncurry_step :=
let H := fresh in
match goal with
| [ |- ?P1 -> ?P2 -> ?Q] =>
cut (P1 /\ P2 -> Q); [uncurry_aux H | ]
end.
Ltac uncurry := repeat uncurry_step.
Ltac eexists_safe := match goal with [ |- ex _] => eexists end.
Ltac name_evars := repeat match goal with |- context[?V] => is_evar V; set V end.
Ltac eassertArg Y := let P := fresh in
evar (P:Prop); assert P as Y;[unfold P; clear P
| unfold P in Y; clear P].
Ltac eassert := let H := fresh in eassertArg H.
Tactic Notation "eassert" "as" ident(Y) := eassertArg Y.
Ltac genDep2 x1 x2 := generalize dependent x1; generalize dependent x2.
Ltac genDep3 x1 x2 x3 := genDep2 x1 x2; generalize dependent x3.
Ltac genDep4 x1 x2 x3 x4:= genDep3 x1 x2 x3; generalize dependent x4.
Ltac genDep5 a b c d e := genDep4 a b c d; generalize dependent e.
Ltac uncurry_aux H := intro H; intros; apply H;
repeat (split;[assumption | ]); assumption.
Ltac uncurry_step :=
let H := fresh in
match goal with
| [ |- ?P1 -> ?P2 -> ?Q] =>
cut (P1 /\ P2 -> Q); [uncurry_aux H | ]
end.
Ltac uncurry := repeat uncurry_step.
Ltac eexists_safe := match goal with [ |- ex _] => eexists end.
Ltac name_evars := repeat match goal with |- context[?V] => is_evar V; set V end.
Given an equality U : a = b, this tactic first tries to rewrite U
in the goal, then if this does not work rewrites it in a hypothesis.
Ltac subst_once U :=
first [rewrite U |
match type of U with ?a = ?b =>
match goal with [U1 : context[a] |- _] =>
rewrite U in U1
end
end].
first [rewrite U |
match type of U with ?a = ?b =>
match goal with [U1 : context[a] |- _] =>
rewrite U in U1
end
end].
Given a hypothesis a = b, substitutes all occurrences of a with b, then
clears the hypothesis.
Ltac subst_all U := match type of U with ?a = ?b =>
move U at top; repeat subst_once U; clear U end.
Ltac neq_symmetry H := let U := fresh in
match type of H with (?a <> ?b) => assert (b <> a) as U; [unfold not;
intro; apply H; symmetry; assumption | ]; try (clear H; rename U into H)
end.
Ltac or_flat_step W :=
let V1 := fresh W in
let V2 := fresh W in
match goal with
[ H : ?P \/ ?Q |- _] => elim_intro H V1 V2
end.
Ltac or_flat_step_norm := let OR := fresh "OR" in or_flat_step OR.
Ltac or_flat := repeat or_flat_step_norm.
Ltac and_flat := let A := fresh "AND" in andflat A.
move U at top; repeat subst_once U; clear U end.
Ltac neq_symmetry H := let U := fresh in
match type of H with (?a <> ?b) => assert (b <> a) as U; [unfold not;
intro; apply H; symmetry; assumption | ]; try (clear H; rename U into H)
end.
Ltac or_flat_step W :=
let V1 := fresh W in
let V2 := fresh W in
match goal with
[ H : ?P \/ ?Q |- _] => elim_intro H V1 V2
end.
Ltac or_flat_step_norm := let OR := fresh "OR" in or_flat_step OR.
Ltac or_flat := repeat or_flat_step_norm.
Ltac and_flat := let A := fresh "AND" in andflat A.
Every time it encounters an existential, decomposes that existential
into a fresh hypothesis and a variable based on "x".
Ltac ex_flat := repeat
let U := fresh in let x := fresh "x" in
match goal with
[U1 : context[ex] |- _] => invertClearAs2 U1 x U
end.
Ltac unfold_all_step r := match goal with [V : context[r] |- _] =>
unfold r in V end.
Ltac unfold_all r := repeat unfold_all_step r.
Ltac exand_flat := repeat (progress (ex_flat; and_flat)).
Ltac state_pred_elim U1 U2 := inversion U1; subst; inversion U2.
Ltac state_pred_net_destr U :=
let e := fresh "e" in let U1 := fresh in let U2 := fresh in
inversion U as [e U1 U2]; inversion U1; subst.
Ltac listGen H l := remember l as LG; repeat (destruct LG as [LG|]; invertChange H);
clear H.
Ltac netprottrip H U q l h k:=
let U1 := fresh in let U2 := fresh U in let e := fresh in
destruct H as [e U1 U2];
let p := fresh in let U3 := fresh in
destruct U1 as [p l h k U3];
let q0 := fresh q in let q1 := fresh q in let q2 := fresh q in let U4 := fresh U in
destruct U3 as [q0 q1 q2 U4].
let U := fresh in let x := fresh "x" in
match goal with
[U1 : context[ex] |- _] => invertClearAs2 U1 x U
end.
Ltac unfold_all_step r := match goal with [V : context[r] |- _] =>
unfold r in V end.
Ltac unfold_all r := repeat unfold_all_step r.
Ltac exand_flat := repeat (progress (ex_flat; and_flat)).
Ltac state_pred_elim U1 U2 := inversion U1; subst; inversion U2.
Ltac state_pred_net_destr U :=
let e := fresh "e" in let U1 := fresh in let U2 := fresh in
inversion U as [e U1 U2]; inversion U1; subst.
Ltac listGen H l := remember l as LG; repeat (destruct LG as [LG|]; invertChange H);
clear H.
Ltac netprottrip H U q l h k:=
let U1 := fresh in let U2 := fresh U in let e := fresh in
destruct H as [e U1 U2];
let p := fresh in let U3 := fresh in
destruct U1 as [p l h k U3];
let q0 := fresh q in let q1 := fresh q in let q2 := fresh q in let U4 := fresh U in
destruct U3 as [q0 q1 q2 U4].
This page has been generated by coqdoc