The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/14/2014 09:45 PM, Randy Pollack wrote:
> In LEGO you can refine one goal by another goal, since all goals must
> be solved to get Qed.  Existential variables are assumed proofs of
> their types, just like ordinary variables. Every completed proof has
> to be fully checked at Qed time, but Coq already does that.
>
> --Randy

That would be interesting thing to propose as an addition to Coq, since 
Coq is getting named goals (and evars) in the next release (already 
partially there in the trunk).

Anyway, my final version of the pruner that works with hypotheses is:

Variables A B C P Q R : Prop.

Axiom okp : A -> P.

Axiom okq : B -> Q.

Axiom okr : C -> R.

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

Ltac revert_all_but v :=
  repeat match goal with H : _ |- _ => lazymatch H with v => fail | _ 
=> revert H end end.

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

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

Goal A -> B -> C -> P /\ Q /\ R /\ Q /\ P /\ Q /\ R /\ R /\ P /\ Q.
prepare_pruning pruner.
intros A B C.
repeat split.
all: prune pruner.
Unshelve.
expand_pruned.
intros; apply okr; assumption.
intros; apply okq; assumption.
intros; apply okp; assumption.
Qed.

-- Jonathan