The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

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

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