The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/14/2014 04:34 PM, Jason Gross wrote:
> It should be possible to write a pair of tactics, [prepare_pruning] and
> [prune], such that the first one is to be run at the very beginning of the
> proof, and sets up an evar or dependent subgoal for the latter to use, and
> the latter partially instantiates the evar to solve two goals but create a
> single new one.
>
> -Jason

Yes - but that requires you to know far enough in advance you that will 
need it, and how often you will need it (as a separate evar is needed 
for each case).

Something like:

Require Import Omega.

Goal forall x y z, x=5 -> y=3 -> z=6 -> x + y > z /\ x + y > z.
intros x y z H1 H2 H3.
refine (let pruner:=_ in _);shelve_unifiable.
split.
revert x y z H1 H2 H3.
match goal with |- ?G => instantiate (1:=G) in (Type of pruner) end.
intros.
apply pruner; assumption.
apply pruner; assumption.
Unshelve.
intros.
omega. (*the one actual proof*)
Qed.

-- Jonathan

> On Fri, Nov 14, 2014 at 3:51 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>
> > 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