The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/14/2014 02:14 PM, Colm Bhandal wrote:
> Hi,
>
> I am wondering if anybody had any idea how to use tactics in Coq to
> eliminate identical subgoals? More preciselsy, let's say there are two
> subgoals:
>
> [H1, H2, H3, ... |- SG] and [H1, H2, H3, ... |- SG] in the context such
> that all the hypotheses and the goals are the same in each case.
>
> It would be nice if there was a tactic "prune" or something to get rid of
> the duplicate subgoal. Anybody got any ideas how to write a tactic like
> this or does one already exist maybe?
>
> Thanks,
>
> Colm

Unforunately, I don't think there is any way to do such pruning after 
the subgoals exist.  If you see that this is about to happen, as in a 
case like:

[H1, H2, H3 |- SG /\ SG]

you can, instead of splitting the goal, rewrite the conclusion so that 
it is just a single SG.  Of course, this is a trivial case.  It can't 
handle the case when the subgoals start out being different and then 
become identical later.

In other cases, if you can solve one of those subgoals in a single 
(perhaps aggregate) tactic, then you can use abstract with a name to 
solve the first, then just apply the resulting named lemma to solve the 
second:

Require Import Omega.

Goal 5 + 3 > 6 /\ 5 + 3 > 6.
split.
abstract omega (*or some other complicated tactic*) using mylemma.
apply mylemma.
Show Proof. (* (conj mylemma mylemma) *)
Qed.

I recall that having an interactive version of the "abstract" tactic was 
once discussed - which would package up any proved subgoal as a separate 
named lemma, even one that is interactively proved.

-- Jonathan