The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

Yeah, I really don't understand why you would want to do something like that.  Why does the solution of one subgoal depend on the solution to another subgoal?  Subgoals are independent.

2008/4/4 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

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club