The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Sean, so you also combine intro with another tactic when using try.
But it can be little uncouthly if you have 20-30 subgoals, you don't know
if intro is possible and if after all intros you use different tactics in
different subgoals depending on other hypotheses in subgoals.

Greetings,

Marko

Sean Wilson reèe:
> On Thursday 06 December 2007 18:51:40 Marko Malikoviæ wrote:
>> Greetings,
>>
>> can somebody give me a reason why first example work, but second not:
>>
>> Ltac test :=
>> intro H1;
>> compute in H1;
>> assumption.
>> Goal 2+3=5 -> 5=5.
>> test.
>>
>>
>> Ltac test :=
>> try intro H1;
>> compute in H1;
>> assumption.
>> Goal 2+3=5 -> 5=5.
>> test.
>>
>> I need to build Ltac but I don't know how many intros are possible to do
>> in particular subgoal. Is it some solution?
>
> This is a hack, but you can do something like this:
>
> (intros x y z H; compute in H ||
>  intros x y   H; compute in H ||
>  intros x     H; compute in H ||
>  intros       H; compute in H ||
>  fail "Too many variables?")
>
> The first intros will fail if there aren't enough variables, so the second
> intros is attempted with one less variable and so on until hopefully one
> of
> the intros works. It will break if you have a subgoal with too many
> variables
> though. Make sure to put in a recognisable error message so you know to
> add
> more intros patterns later if this tactic fails.
>
> I'd like to know if there is a cleaner way to do this, but I find that I
> need
> to use hacks like this in Ltac quite often as it lacks certain fine
> control.
> This is another Ltac hack I use frequently when working with functions
> when I
> don't know the number of parameters needed:
>
> Ltac fun_name t :=
>  match t with
>            ?f ?a => f
>          | ?f ?a ?b => f
>          | ?f ?a ?b ?c => f
>          | ?f ?a ?b ?c ?d => f
>          | ?f ?a ?b ?c ?d ?e => f
>          | _ => fail "fun_name: function has too many parameters!"
>      end.
>
> Good luck,
>
> Sean
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>