The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Are you looking for something like this?

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

On Wed, Jun 25, 2014 at 4:52 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 06/25/2014 02:29 AM, Guillaume Melquiond wrote:

On 24/06/2014 23:53, Jonathan wrote:

Could someone describe in more detail what is supposed to go on at the
end of a section with regard to this dependency analysis?  I might be
seeing a bug, or I might just not understand what is involved in a
dependency according to this analysis.  Is it perhaps that some tactics
involved in the proof of the definition create "false" dependencies that
aren't really needed, but are still honored with respect to
end-of-section dependency analysis?

As long as the hypotheses appear in the constructed proof terms, they are actual dependencies. You can Print the proved theorems to see where they come from. Do you happen to use any automatic tactic (auto, omega, assumption, etc)? Such tactics don't try to find the minimal subset of hypotheses needed for proving a goal. And even if they were doing this extra work locally, that would not guarantee that the whole theorem would use a minimal subset of hypotheses.

Best regards,

Guillaume

Yes, the set of tactics used includes various automation tactics - so it is not surprising that the dependencies are formed.

The other issues with section variables being discussed make it unlikely that using Section in the way I described (turning a goal into a separate definition) would work anyway.

But, if that other bug was fixed - it might be possible to create a Section from a goal, prove the consequent in that section as a definition, and then automatically one at a time delete the variables to see which ones can be removed without altering the proof...

-- Jonathan