The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 25 Jun 2014 20:24:43 -0400,
Jonathan 
<jonikelee AT gmail.com>
 a écrit :

> 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

Often, when I want to use abstract, I first do the proof interactively,
then turn it into a one liner.

For that, I first 'one line' the deepest branch.
That is if "t." solves the goal, I keep it,
and if "t." does not solve the goal but creates n goals, and t1…tn
solve each of these goals, then I turn "t. t1.…tn." into "t;
[t1|…|tn].".

(I also prefer to use "t1; t2." rather than "t1; [t2]" when no extra
goal is created.)

This implies that these proofs are done in two steps. The hard step is
doing the proof, the easy (but not interersting) is to one-line it.

Of course, having interactive abstract would be way better.

> 
> >
> > 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] *)
> >
> >
>