The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Friday 04 April 2008 08:30:22 
marko AT ffri.hr
 wrote:
> Greetings,
>
> I send this problem on this mailing list already but question was little
> different:
>
> How to compare hypotheses over subgoals?
>
> But now I am asking: "Is it possible to compare hypotheses over subgoals?"
> So is it possible in environment:
>
> Subgoal 1:
>
> H : x=value_1
>
> Subgoal 2:
>
> H : x=value_2
>
> ...
>
> Subgoal n:
>
> H : x=value_n
>
> find out are all x's have the same or different values and then to apply
> different tactics according of this knowledge?
>
> I spend five (5) days to find solution but every idea failed (pattern
> matching, rewriting, abstracting lemma from one subgoal and applying to
> other subgoals, etc...)
>
> Yves Bertot already answers me that he doesn’t believe I can and I'm
> gratefully for the answer.
>
> But, I need to know is it impossible for sure? Are all tactics forbid it?
> Or is it maybe possible but nobody did something like that?

If you need more power than Ltac will give you, you can always write a tactic 
in OCaml that will do what you want. However, I would advise you to consider 
the reason you need such a tactic (i.e. what is the actual high-level problem 
you're trying to solve?) and ask you to consider alternative solutions that 
do not require tactic use with the behaviour you specify.

Regards,

Sean