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: 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.



Archive powered by MHonArc 2.6.18.

Top of Page