coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sean Wilson <sean.wilson AT ed.ac.uk>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Goal ordering in Ltac
- Date: Tue, 8 May 2007 19:45:59 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: School of Informatics, The University of Edinburgh
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
- [Coq-Club] Goal ordering in Ltac, Sean Wilson
- Re: [Coq-Club] Goal ordering in Ltac, Brian E. Aydemir
Archive powered by MhonArc 2.6.16.