The Coq mailing list

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

Dear all,

I need advice from somebody with experience and who have some feeling what
the best direction in this situation is:

- tfrom proof of one goal I have lot of subgoals
- some of the subgoal is possible to prove but some of them is not
- proved subgoals are not interesting for me but in unproved subgoals I
have some computed hypotheses which are important for me and with this
hypothesis I have to recursively reasoning in further steps. Furthermore,
some hypotheses are missing after first step.

I have several solutions:

- to build ltac-s and recursive reasoning (here I have problem that many
hypotheses are introduced in the middle of the proof (using intro) and
because matching patterns do not accept this hypotheses - there are not
declared before)

- to try to build-up the same context in every subgoal like it was in the
beginning

- to record somewhere important hypotheses from the subgoals and then to
try to use them

I know, my question is very general but what is your experience - in what
direction I have to go?

Thank you very much,

Marko Malikoviæ