The Coq mailing list

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

No, I don't need this. Imagine 30 subgoals and every subgoal like chain of
10, 15 or 20 implications: A -> B -> ... It is several groups of subgoals
with different number of possible intros (it depend on one of hypothesis
which have to be introduced also). Here is small example:

Parameter B C D E F Z : Prop.
Inductive arguments : Set := x | y | z.
Parameter P : arguments -> Prop.
Parameter u : arguments.
Parameter m : nat.
Axiom A1 : (m=1 -> C -> D -> E) -> Z.
Axiom A2 : (m=2 -> B -> C) -> Z.
Axiom A3 : (m=3 -> C -> D -> E -> F) -> Z.

Goal P u -> Z.

intro Hu;
induction u;
match goal with
  | [ Hu : P x |- _ ] => apply A1
  | [ Hu : P y |- _ ] => apply A2
  | [ Hu : P z |- _ ] => apply A3
end;

And now I need to make intros. But, first I need to intro hypothesis of
value m. On value of m depend number of intros I have to do.
So, without Ltac definition it is:

intro Hm;
match goal with
  | [ Hm : m=1 |- _ ] => intros H1 H2
  | [ Hm : m=2 |- _ ] => intros H1
  | [ Hm : m=3 |- _ ] => intros H1 H2 H3
end.

But I need recursion (!!!) and I need to make Ltac definition and put all
tactics into that definition. And here are problems:

1. I need to intro Hm without any compute or similary - I can not do it
2. I must to do pattern matching on goal and to intro rest of hypothesis.
Number of hypothesis depend on value of m. But I can not do it because of
problems we are talking about

Greetings,

Marko Malikoviæ

Edsko de Vries reèe:
> On Thu, Dec 06, 2007 at 11:11:18PM +0100, Marko Malikovi? wrote:
>> 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.
>
> I'm not sure what exactly you are trying to do, but if you need to
> 'search' for the hypothesis you need in the tactic, perhaps you could do
> something like
>
> Ltac test :=
>   let H := fresh in
>   intro H;
>   (solve_using H || test).
>
> Where solve_using is some tactic that uses H (note: not tested, don't
> have access to Coq at the moment). This basically recursively tries to
> introduce a new hpothesis, tries to use that hypothesis, and if that
> fails, recursively tries the next.
>
> Edsko
>