GenericTactics

GenericTactics

Rationale

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).

Coq code

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.