The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

I would like to advertise a few  tools that I developed to speedup my
work in Coq.  They are mostly tactics or commands written in ml, with
a vernacular file attached to make these tools directly available from 
Coq.

Here is a summary

* SearchPattern : a more elaborate search command, to see less
  garbage.
  in http://www.inria.fr/lemme/Yves.Bertot/fine_search.tar.gz

* OnThen : like ";" except that the second tactic is only applied to
  designated subgoals.
  (available with DebugTac).

* DebugTac : a tactic debugger for large composed tactics
  in http://www.inria.fr/lemme/Yves.Bertot/debug_tac.tar.gz


Here is a more complete explanation of these tools.

* SearchPattern,

   Like Search, but it uses a patten to decide the theorems you want to
  see.  For instance you can request to see only those equalities on
  type blahblah by entering the command:

    SearchPattern (eq blahblah ? ?).

  There are a few variants, like

    SearchPattern ? = ? outside Zcomplements Zlogaritm zarith_aux.

  If you don't want to see the theorems that were defined in a given
  collection of files (in this example we avoid the theorems used for
  the tactic Omega), and even more useful (nach meine einige
  erfahrungen) you can search for rewriting theorems using commands
  like the following one:

    SearchRewrite (minus (plus ? ?) ?).

  Patterns need not be linear: you can express that the same
  expression must occur in two places by using indexed existential
  variables:

    SearchPattern (le ?1 (S ?1)).

  will not find the the constructor le_S.

  I also have a variant for use inside CtCoq and Pcoq in the future.

* OnThen
  This is a variant of the ";" tactic composer.  It receives as extra
  arguments the list of indices of goals that will be taken care of by 
  the second tactic.

  For instance

     OnThen (Case t) (Discriminate) 1 3 5

  Will apply the tactic "Case t", then it will apply Discriminate only 
  on the first, third, and fifth generated subgoals.

* DebugTac

  This is a simple tactic debugger for large composed tactics
  constructed using ";" and ";[...| ... | ...]".  Such large composed
  tactics can be very useful for the "Abstract" tactical, but they are 
  rather painful to debug when an error creeps in (or when the context 
  changes).

  There are two variants to the debugger.  The first one is called
  DebugTac and will execute an erroneous composed tactic as much as
  possible, giving as a report the tactic that was effectively
  computed.  This tactic never fails.

  The second variant is called DebugTac2 and will fail if the observed 
  tactic fails.  When failing it will give a report consisting of:
  - the goal at the time of failure
  - the sub-tactic that should have been applied on this goal.

  Hopefully, the combination of these two tactics should make
  debugging large tactics much easier.


  Here is an example of use (done with CoqV6.3.1, but the package also 
  works with CoqV6.3, or CoqV6.2.4).

paprika$ coqtop
Welcome to Coq V6.3.1 (December 1999)
No .coqrc or .coqrc.6.3.1 found. Skipping rcfile loading.

Coq < Require Debug_tac.
[Reinterning Debug_tac...done]
[Loading ML file debug_tac.cmo ...done]

Coq < Goal (True /\ ~O=(S O)) /\ (True /\ O = O).
1 subgoal
  
  ============================
   (True/\~O=(S O))/\True/\O=O

Unnamed_thm < DebugTac2(Split;(Split;[Auto | Discriminate])).
in branch no 2 after tactic Split
Execution of this tactic raised message 

Error: goal does not satify the expected preconditions

on goal
  
  ============================
   O=O

faulty tactic is

Discriminate

1 subgoal
  
  ============================
   (True/\~O=(S O))/\True/\O=O

Unnamed_thm < DebugTac(Split;(Split;[Auto | Discriminate])).

=========    Successful tactic    =============
(OnThen (Split) (Split; [ Auto | Discriminate ])
 1)
========= End of successful tactic ============
1 subgoal
  
  ============================
   O=O

Unnamed_thm < 

  I am currently working on integrating these inside the graphical
  user-interface Pcoq (error reporting must be done in a different way).

these packages are available from my web-page.  I also have versions
of these packages adapted for older version of Coq.  Any feedback or
suggestion for improvement is welcome.

Yves