The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

You first need to write your three "tactics" into three single tactics
(the period ends a tactic, so "intros. rewrite mult_n_O. trivial." is
actually three tactics) because tacticals take unique tactics as
arguments.

Most of the time this is easy using the ";" tactical. sometimes you
may also need the [ | ] tactical to apply different tactics to
different subgoals. For example: tactic3 should probably be written
"induction n; [intros; simpl; trivial | simpl; trivial].

Once you rewrote the three "tactics" into three single ones you may
combine them in several ways. Eric suggested one, you can also try

solve [tactic1 | tactic2 | tactit3]

or:

try now tactic1 ; try now tactic2 ; try now tactic3

etc.

Hope this helps,
Pierre



2014-10-27 21:34 GMT+01:00 Eric Mullen 
<emullen AT cs.washington.edu>:
> Is what you want similar to:
>
> try solve [tactic1]; try solve [tactic2]....
>
> On Oct 27, 2014 1:26 PM, "Gransden, Thomas" 
> <tg75 AT student.le.ac.uk>
>  wrote:
>>
>> Hi all,
>>
>>
>> I was just wondering if there was a way of encoding the following scenario
>> in Ltac:
>>
>>
>> Say that we have a few sequences of tactics that we use often in a corpus
>> of proofs - for example lets say the following:
>>
>>
>> t1 - intros. rewrite mult_n_O. trivial.
>>
>> t2 - intros. destruct_all bool. reflexivity.
>>
>> t3 - induction n. intros. simpl; trivial. simpl; trivial.
>>
>>
>> Can I create an Ltac tactic that applies t1 OR t2 OR t3?
>>
>>
>> I have had a play around with Ltac but cannot seem to get something like
>> this working, so any help or hints would be much appreciated.
>>
>>
>> Thanks
>>
>>
>> Tom