The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/14/2014 04:56 PM, Jonathan wrote:
> 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).

Or, not.  As I recall, Jason, you pointed out this "_ /\ _" trick a 
while ago:

Variables P Q R : Prop.
Axiom okp : P.
Axiom okq : Q.
Axiom okr : R.

Ltac prepare_pruning v := refine (let v := _ in _); shelve_unifiable.

Ltac prune v := try tauto; instantiate (1:=_/\_) in (Type of v); 
decompose [and] v; eauto.

Ltac split_pruned := repeat split; [exact I|..].

Goal P /\ Q /\ R /\ Q /\ P /\ Q /\ R /\ R /\ P /\ Q.
prepare_pruning pruner.
repeat split.
all: prune pruner.
Unshelve.
split_pruned.
apply okr.
apply okq.
apply okp.
Qed.

Probably requires some work to make this work for goals complete with 
their hypotheses (extra points of the order of hypotheses doesn't 
matter, and if subsuming goals can be combined) - but this is a good 
starting point.  Still requires the annoying "prepare_pruning" 
initialization, though.

-- Jonathan