The Coq mailing list

[marko AT ffri.hr]

But, I can do it with little "wild" way. I can apply this kind of pattern
matching on all subgoals:

match goal with
| [H:lista_predikata = predikat a1 ?x ?y ?z :: ?Y |- _ ] =>
     match goal with
     | [H:lista_predikata = predikat ?x a2 ?y ?z :: ?Y |- _ ] =>

         ...etc

| [ |- _ ] => match goal with
              | [H:lista_predikata = predikat b1 ?x ?y ?z :: ?Y |- _ ] =>

         ...etc

So, I can do matching for EVERY combinations of parameters in lists. But
this way is "wild". If you understand me and if you have some idea to make
it more beauty please let me know.

Thank you very much,

Marko Malikoviæ




>Â marko AT ffri.hr
>  wrote:
>> The question is: "How can I compare hypotheses H in different subgoals
>> and
>> if in each subgoals the hypotheses H are the same then apply some
>> tactic?"
>>
>> Any idea?
>>
>>
> I don't believe you can.  The idea behind tactics is rather that you
> address each goal independently
> from the others...
>
> Can you turn your problem around so that all cases appear in the same
> goal?
>
> 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!
>
> Nobody prevents you from defining a list of propositions, even if no
> element in the proposition
> hold, as in the following script:
>
> Require Import List.
>
> Definition l := False::nil.
>
> Definition counter_example : l = False::nil := refl_equal l.
>
> In this three line script, we never provide a proof of False.
>
> Yves
>