The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

I'm trying to write some Ltac tactics and I'm running into trouble because 
I'm 
not sure how to control the order in which my tactic tackles goals. For 
example, if I have a single proof goal X and I execute "assert (1=1)", "1=1" 
will be added as the new current goal and X will become subgoal 2. If I want 
my tactic to use assert but I want the asserted goal to become goal 2 instead 
(so I can deal with it later), what options do I have to do this?

When in proof mode, I could use the command "Focus 2" to focus on the goal 
I'm 
interested in, but this command does not seem available to use in Ltac. Is 
there anyway I can use this?

Also, are there any ways in which Ltac tactics can return results (like lists 
or numbers) for other tactics to use? For instance, can I write a tactic that 
returns a list of all assumptions in the hypothesis with type nat which can 
be passed as input to another tactic which calls "clear" for each assumption 
found?

Specifically, I'm experimenting trying to write a simple counter-example 
generator. Given a goal with some universally quantified variables, I'm 
replacing each variable (using "replace") in the current goal with example 
values and then seeing if I can find a contradiction. As "replace" will 
insert unprovable goals like "x=1", I need my tactic to ignore these goals. 
When I have multiple goals, the "replace" goals are getting mixed up with 
goals I want my tactic to work on. I'm wondering if it would be better to 
write this in OCaml, but it would be nice to use Ltac.

Regards,

Sean