coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Inverse of split tactic?
- Date: Mon, 19 Jan 2015 08:33:51 +0000
- Accept-language: de-DE, en-US
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
- [Coq-Club] Inverse of split tactic?, Soegtrop, Michael, 01/16/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
- RE: [Coq-Club] Inverse of split tactic?, Soegtrop, Michael, 01/19/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
Archive powered by MHonArc 2.6.18.