coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Inverse of split tactic?
- Date: Fri, 16 Jan 2015 14:27:49 -0500
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
Ltac revert_all := repeat lazymatch goal with H:_ |- _ => revert H end. (*a distinct tuple type for collecting goals*) Inductive goals (A B:Type) : Type := Split : A -> B -> goals A B. Arguments Split {A} {B} a b. Notation "x â¡ y" := (goals x y) (at level 100, right associativity, y at level 200) : type_scope. Notation "x â® y" := (Split x y) (at level 100, right associativity, y at level 200). Ltac collect_goals := try (is_evar ?__Collect_Goals; fail 1 "collect_goals: The evar name ?__Collect_Goals is being used"); revert_all; try (let C:=fresh in refine (let C:=?[__Collect_Goals]: _ in _); [ | |clear C]); [ > (*__Collect_Goals type evar subgoal*) | (*__Collect_Goals evar subgoal*) | (*non-last original subgoals*) let C:=fresh in pose (C:=?__Collect_Goals); lazymatch goal with |- ?G => instantiate (1:=goals G _) in (Type of C) end; decompose [goals] C; assumption .. | (*last original subgoal*) let C:=fresh in pose (C:=?__Collect_Goals); lazymatch goal with |- ?G => instantiate (1:=G) in (Type of C) end; decompose [goals] C; assumption]; refine (_) (*rename remaining goal away from __Collect_Goals*). Goal forall n, n>=0. (*demo*) intro n. destruct n. (*give the two subgoals some other hyps to show how these are preserved*) 1:pose (first_subgoal := true). 2:pose (second_subgoal := false). all:collect_goals. (*collect all focused goals into one*) (*repeat split would maybe split too much - so do this instead to undo the collect:*) repeat apply Split; intros. Show Existentials. Abort.
- [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.