The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

thanks, the approach is very interesting! Unfortunately I am still on 8.4pl5 
and want to stay there for a while in order to avoid issues with other 
libraries I need. But I will experiment a bit around your ideas!

Thanks & best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jonathan Leivent
Sent: Friday, January 16, 2015 8:28 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Inverse of split tactic?


On 01/16/2015 12:43 PM, Jonathan Leivent wrote:
>
> On 01/16/2015 12:03 PM, Soegtrop, Michael wrote:
>> Dear Coq users,
>>
>> Is there an inverse of the split tactic, that is a tactic that 
>> combines the top two goals into one conjunction goal? This might be 
>> handy for automatically constructing certain terms using Ltac.
>>
>> Best regards,
>>
>> Michael
>>
>>
>
> There is no standard tactic to do this.  However, I am working on a 
> toolbox of tactics compatible with 8.5  - and one of them combines all 
> focused goals into a single goal - like an inverse of "repeat split".
> These tactics feature a bunch of "hacks" involving the behavior of 
> evars and tactics-in-terms (the "$(...)$" syntax) in 8.5 that I've 
> been exploring.
>
>

I separated out the collect_goals tactic from the rest I'm working on - 
If you're using 8.5 (or any fairly recent trunk version of Coq), then 
the attached file should work.  The particular "hacks" that 
collect_goals makes use of are: how a hardcoded evar name 
(?__Collect_Goals) can be used to establish a single evar that is shared 
across all goals under focus, and how that one evar can be used to 
collect info of various kinds (in this case, conclusion types) from all 
of those subgoals.

I'd be interesting in what you mean by "automatically constructing 
certain terms using Ltac" - as I have other tactics that might be 
helpful with that.

-- Jonathan