Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Inverse of split tactic?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Inverse of split tactic?


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page