The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I think that if you have to prove a same goal many times, it is worth to prove it separately.

If you do not want to prove a new lemma, you can still go to the parent node of all of your common subgoals, and then use "assert" (forward proof) or "cut" (backward proof) at this point to get a "local lemma" inside of your proof and use it later in each of your common subgoals.

It is generally more efficient than replaying the whole tactic at each common subgoal.

2014-11-14 20:14 GMT+01:00 Colm Bhandal <bhandalc AT tcd.ie>:

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

--

.../Sedrikov\...