The Coq mailing list

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

Intros work but even we know what name of introduced hypothesis will be we
can not use it because system can not be sure it will be this name. And it
is OK.
But pattern matching also don't work (because of the same reason I think).
And what is the possibility of using intro in Ltac definitions if you
don't know is product exist? To combine it with some another tactics like
you do?
If it is only possibility I will use it but it also seems unnaturally.
Furthermore, even this work:

Ltac test :=
try (intro H1;idtac).
Goal 2+3=5 -> 5=5.
test.

Marko

Edsko de Vries reèe:
> On Thu, Dec 06, 2007 at 07:51:40PM +0100, 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.
>
> The scope of the 'try' is only the 'intro H1', so it is not guaranteed
> that it will succeed. Therefore, H1 may or may not be in scope when the
> rest of the tactic is executed. This works:
>
> 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?
>
> 'intros' introduces all of them, but of course you won't be able to
> apply them in the tactic because you won't know their name.
>
> Edsko
>