The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.