The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hi. This is mostly a bug-report but is also related to the thread about
OCaml tactics.

The problem: sometimes when the context is big with a lot of complicated
terms,
the Assumption tactic takes a very long time to work. This would seem to
be because
it tries to reduce each hypothesis to see if it can work. Generally in
this case,
the right answer (e.g. Exact H17) is fast, but eliminating the wrong
answers is slow.
In fact, in at least half the cases, the right answer is textually
identical to the goal.

Q1: is Assumption going to be optimized in V8? The most obvious strategy
would be to try all the
terms with a short limit on the computing time; then if none works, go
back and try again
with a longer time limit (say 2x the previous limit).  Another
optimization would be to
look first for hypotheses whose statement is textually identical to the
goal.

The same problem arises more generally with user-defined tactics using
the Match Context With
construction.  For example, this came up with a tactic that looks like

can we ask for an extension of the tactics language in 2 directions:

Q2: ask for some type of syntax permitting a sort of textual analysis
--and more generally analysis
on the structure of terms. As a general matter, in reply to Nadeem's
question
it would seem appropriate to note that it is better to write tactics in
the tactic language,
since they will then be forward-compatible with future versions; but the
tactic language
has to be strong enough to do so.
  A good criterion would seem to be: can one write all of the basic
tactics in the tactic language?
(For example I don't see how to do the Apply tactic).

Q3: for the optimization problem referred to above, it would be good to
have an invariant abstract
measure of computing time integrated into the program, and then a
tactical of the form
Timeout n t
which would succeed if the tactic t succeeds in less than or equal to n
"cycles" (refering to the
abstract time measure), and would fail (in n+1 cycles) if t does not
succeed after n cycles.
The optimized Assumption tactic might then look like:
Tactic Definition NewAssumption :=
Match Context With
[id1 : ? |- ?] -> Timeout 500 (Exact id1) |
[id1 : ? |- ?] -> Timeout 1000 (Exact id1) |
[id1 : ? |- ?] -> Timeout 2000 (Exact id1) |
[id1 : ? |- ?] -> Timeout 4000 (Exact id1) |
[id1 : ? |- ?] -> Timeout 8000 (Exact id1) |
[id1 : ? |- ?] -> Timeout 16000 (Exact id1) |
_ -> Assumption.

(of course, even better if n could be an element of ZArith.Z...).

---Carlos Simpson