The Coq mailing list

[marko AT ffri.hr]

> Can you turn your problem around so that all cases appear in the same
> goal?

No, I can't because these hypotheses are some of the most important thinks
in my system. But I try to find a way to "merge" subgoals. So, if I have
several subgoals with the same statement to prove and if every subgoal
contain hypothesis with the same name but (maybe) with the different
values, for example:

subgoal 1:

H : x=5
...other hypotheses...
----------------------
y=z

subgoal 2:

H : x=6
...other hypotheses...
----------------------
y=z

can I somehow "merge" this two subgoals in subgoal 3 and then in subgoal 3
to check is the values of parameter x is the same. So, subgoal 3 has to
look like this:

subgoal 3:

H1 : x=5
H2 : x=6
...other hypotheses...
----------------------
y=z

> As a side note, the example you give is very strange.  Do you believe that
> by assuming
>
> H: lista_predikata = predikat a1 b2 a3 c4 :: predikat d1 c2 a3 c4::nil
>
>
> you are actually asserting that predikat a1 b2 a3 c4 hold?  This is not
> the case!

This is not important for me. Hypothesis

H: lista_predikata = predikat a1 b2 a3 c4 :: predikat d1 c2 a3 c4::nil

is for me just a way to record some values and lista_predikata is growing
up through the proof tree. I just need to read from this hypothesis some
records.

Thank you very much,

Marko Malikoviæ