GenericTactics - coq/coq GitHub Wiki
A tactic like auto
is powerful in theory, but in practice it too often can not do anything on the goal just because in a series of, say, 5 steps, the last can not be done by auto
. So in practice, it sometimes is more effective to write some domain-specific tactic t in Ltac, doing only some small invertible reasonning step and, to call repeat
t.
The following code elaborates on this idea: Ltac can be used to build a generic solver tactic, taking as arguments invertible and non-invertible tactics, and applying a standard iterative deepening search using non-invertible tactics and normalizing the goal at each depth using invertible tactics. You can think of it as a parameterized intuition
tactic (intuition
can be parameterized this facility is very limited : you can only customize the way it solves atoms; there is no way to add some specific behavior in order to, say, make it unfold some definitions or rewrite some terms, or ...)
I (JudicaelCourant) define some domain-specific tactics in my developments, extending the invertible and/or non-invertible tactics given in the next section and I apply the generic search tactic to my tactic. For instance, in a case study I am currently conducting with Jean-François Monin, I defined the following progress1
tactic:
Ltac progress1 g := match goal with
| [ |- step_up ?f ?z (?u::?x) ] => apply step_up_snoc2
| [ H : continuous ?f |- _ ] => unfold continuous in H
end
|| progress0 g.
Then I defined splitsolve1
as the following shorthand:
Ltac splitsolve1 n := splitsolve progress1 split0 noni0 n 0.
And I use splitsolve1 0
, ..., splitsolve1 2
to work on my goals.
Even with no customisation, splitsolve0
(given below) is surprisingly effective. For instance, in my current case study, I found that I could replace the following steps:
intros m H y.
simpl.
rewrite H.
ring.
with a single splitsolve0 0
(in fact, intros;simpl;omega
would also work, but I did not figure it out at first as the goal was quite complex; splitsolve0
did).
Require Omega.
(* A repeat tactical for one-argument tactics. Unlike repeat, the
tactic is applied at least once.
*)
Ltac repeat1 t g := t g; repeat (t g).
Ltac tacsum t1 t2 g := (t1 g; try t2 g) || t2 g.
(* A tactic is said invertible whenever its application does not
change the provability of the goal.
In the following we use the following terminology:
* progressing tactics: invertible tactics generating at most one
subgoal
* splitting tactics: invertible tactics potentially generating
several subgoal
* solving tactics: solve the goal or fail
* non-invertible tactics.
* non-invertible mapping: a parameterized tactic [t], taking as
argument a solver [s], applying some non-invertible tactic
followed by [s] on the generated subgoals.
*)
(* [rsplit pro spl] tries to solve the goal, using the progressing
tactic [pro] and the splitting tactic [spl]. [g] is a dummy
argument. This tactic is splitting.
*)
Ltac rsplit pro spl g :=
let t g := (spl g; try repeat1 pro g) in
let rt g := repeat1 t g in
let t2 g := repeat1 pro g in
tacsum t2 rt g.
Ltac myfail g := fail.
(* [solver_dfs pro spl noni n g] is a depth-first search solving
tactic, where:
* [pro] is progressing
* [spl] is splitting
* [noni] is a non-invertible mapping
* n is the depth of search
* g is a dummy argument
*)
Ltac solver_dfs pro spl noni n g :=
try rsplit pro spl g;
let t := match n with
| O => myfail
| S ?k => noni ltac:(solver_dfs pro spl noni k)
end
in t g.
(* [solver pro spl noni n g] is an iterative deepening search
solving tactic where:
* [pro] is progressing
* [spl] is splitting
* [noni] is a non-invertible mapping
* n is the depth of search
* g is a dummy argument
*)
Ltac solver pro spl noni n g :=
let t :=
match n with
| O => solver_dfs pro spl noni 0
| S ?k =>
let u g := (solver pro spl noni k g || solver_dfs pro spl noni n g) in u
end
in t g.
(* [splitsolve pro spl noni n g] is a splitting tactic trying to
solve the generated subgoals with [solver]
*)
Ltac splitsolve pro spl noni n g :=
try rsplit pro spl g; try solver pro spl noni n g.
(* [everywhere t g] generalizes the whole goal, then applies g,
then introduces previously generalized hyps and variable back.
NB: we have to take care of 'match goal' non-determinism since
we want a deterministic behaviour here: the first case must
apply only on the last hypothesis of the context
*)
Ltac everywhere t g := match goal with
| [ H : _ |- _ ] => generalize H; clear H; (everywhere t g || fail 1); intro H
| [ |- _ ] => match goal with
| [ H : _ |- _ ] => fail 1
| [ |- _ ] => t g
end
end.
(* apply [t] on some hyp [H] by generalizing [H], applying [t]
(and verifying it is progressing), then introducing [H] back.
*)
Ltac on_one_hyp t g := match goal with
| [ H : _ |- _ ] => generalize H; clear H;
(progress (t g) || on_one_hyp t g || fail 1);
intro H
end.
(* our generic rewrite database is named rew_db *)
Ltac autorew g := autorewrite with rew_db.
(* The base progress, splitting and non-invertible tactics I use.
I do not pretend they have nice theoretical properties (besides
being progressing, splitting and non-invertible) but they do the
job for me. (I call them using [splitsolve0] below.)
*)
Ltac progress0 g := match goal with
| [ |- _ ] => omega || elimtype False;omega
| [ |- _ ] => progress (autorew g)
| [ |- _ ] => on_one_hyp ltac:autorew g
| [ H : ?t = ?t |- _ ] => clear H
| [ H : ?x = ?t |- _ ] => subst x
| [ H : ?t = ?x |- _ ] => subst x
| [ H : ?a = ?b |- _ ] => discriminate H
| [ H : ?a = ?b |- _ ] => injection H;
match goal with
| [ H: _ |- a = b -> ?p ] => fail 1
| [ H: _ |- _ ] => idtac
end;
clear H;intros
| [ H : (exists x, _) |- _ ] => elim H; clear H; intros
| [ H : _ |- _ ] => inversion H;fail
| [ |- _ ] => assumption
| [ H : ?p, H2 : ?p |- _ ] => clear H || clear H2
| [ H1 : ?a -> ?b, H2 : ?a |- _ ] => assert b; [ exact (H1 H2) | clear H1 ]
| [ H : ?a /\ ?b |- _ ] =>
generalize (proj1 H) (proj2 H);clear H; intro; intro
| [ |- ?a -> ?b ] => intro
| [ H : ?a /\ ?b -> ?c |- _ ] => cut (a -> b -> c) ;
[ clear H; intro H
| intro; intro; apply H;split; assumption ]
| [ |- forall x, _ ] => intro
| [ |- ?t = ?u ] => congruence
| [ |- False ] => congruence
| [ |- ?t <> ?u ] => intro
| [ |- ?t = ?u ] => ring;fail
| [ |- _ ] => everywhere ltac:(fun g => (progress simpl)) g
| [ |- True ] => trivial
| [ H : ?a >= ?b |- _ ] => cut (a > b \/ a = b); [clear H;intro H| omega]
| [ H : ?a = ?a -> ?b |- _ ] => cut b ;
[ clear H; intro H | apply H; reflexivity]
end.
Ltac split0 g := match goal with
| [ H : ?a \/ ?b |- _ ] => elim H;clear H
| [ H : (?a +{ ?b }) |- _ ] => elim H; clear H;intro
| [ H : ({ ?a }+{ ?b }) |- _ ] => elim H; clear H;intro
| [ |- ?a /\ ?b ] => assert a ; [ idtac | split ; [ assumption | idtac ] ]
end.
Ltac noni0 t g := match goal with
| [ |- _ ] => econstructor; t g
(* | [ |- _ ] => left; t g subsummed by constructor above *)
| [ |- _ ] => constructor 2; t g
| [ x : _ |- exists y, _ ] => exists x;t g
| [ |- ?f1 ?x1 = ?f2 ?x2 ] =>
cut (f1 = f2);
[ cut (x1 = x2); [ intros;congruence
| idtac ]
| idtac ]; t g
| [ H : (forall x, _), x0 : _ |- _ ] => generalize (H x0);clear H;t g
| [ H : (?f ?u) <> (?f ?v) |- _ ] =>
cut (u <> v); [ clear H; intro H; t g | congruence ]
| [ |- _ ] =>
(apply Zorder.Zmult_le_compat_l
|| apply Zorder.Zmult_ge_compat_l
|| apply Zorder.Zplus_le_0_compat
|| apply Zorder.Zmult_le_0_compat);
t g
| [ H : _ |- _ ] => apply H; t g
| [ |- _ ] => solve [eauto]
end.
Ltac splitsolve0 n := splitsolve progress0 split0 noni0 n 0.
Ltac solver0 n := solver progress0 split0 noni0 n 0.