The Coq mailing list

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

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