The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/25/2014 07:21 PM, Jason Gross wrote:
> Are you looking for something like this?

Jason,

I am in looking for a solution that isn't like "abstract tac" - it 
should instead allow for separate interactive solution of the goal being 
abstracted.  The techniques you show here look quite interesting, but I 
don't see how they could apply if the goal is to be interactively solved 
instead of solved via a single tactic.

-- Jonathan

> Tactic Notation "test" tactic3(tac) :=
>   try (first [ tac | fail 2 tac "does not succeed" ]; fail tac "succeeds";
> [](* test for [t] solved all goals *)).
>
> (** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and
> is equivalent to [idtac] if [tac] fails *)
> Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac
> "succeeds").
>
> (** [revert_last] and [reverse] are taken from [Coq.Program.Program] *)
> Ltac revert_last :=
>    match goal with
>      | [ H : _ |- _ ] => revert H
>    end.
> Ltac reverse := repeat revert_last.
>
> Ltac goal_has_evars :=
>    let G := match goal with |- ?G => constr:(G) end in
>    has_evar G.
>
> (** Clear any hypotheses that aren't needed to solve the goal by [intros;
> tac], and then revert all remaining hypotheses *)
> Ltac prepare_for_solving_by tac :=
>    first [ test solve [ intros; tac ]
>          | fail "The goal cannot be solved by intros;" tac ];
>    first [ not goal_has_evars
>          | fail "prepare_for_solving_by does not handle evars" ];
>    intros;
>    repeat match goal with
>             | [ H : _ |- _ ] => clear H; test solve [ intros; tac ]
>           end;
>    reverse.
>
> (** Like [intros; abstract tac], but the resulting opaque proof term won't
> depend on any hypotheses it doesn't need.  Note that the time this takes is
> something like O((number of clearable hypotheses + 1) * (number of
> unclearable hypotheses + 1) * time of running [tac]) *)
> Ltac clear_abstract tac :=
>    prepare_for_solving_by tac;
>    intros; abstract tac.
>
> Require Import Omega.
> Goal forall (n m q : nat), n + m = m + n.
>    intros.
>    prepare_for_solving_by omega.
>    (* [forall n m : nat, n + m = m + n] *)