Stream: Coq users

Topic: ✔ Run a tactic on all hypothesis once

Thibaut Pérami (Aug 25 2022 at 10:46):

I was wondering if there was a standard or decent way to run a tactic on all hypotheses. Let's say I have a tactic tac that takes a hypothesis as a parameter. What I currently do is:

repeat (match goal with
    |  [H : _ |- _ ] => progress (tac H)
    end).

Unfortunately this can be quadratic in the number of hypothesis. Some tactics like rewrite and autorewrite support the in * syntax, but there is no way to make that available to a generic Coq tactic without writing a plugin as far as I know.

Guillaume Melquiond (Aug 25 2022 at 11:53):

The usual trick is, once a hypothesis has been handled, to revert it into the goal; and at the end, just introduce them all back. Note that you might want to use match reverse goal instead of match goal.

Thibaut Pérami (Aug 25 2022 at 18:08):

Thanks, my solution is this:

Ltac forall_hyps tac :=
  lazymatch goal with
  | H : _ |- _ => try(tac H); revert H; try (forall_hyps tac); intro H
  end.

I don't want match reverse because hypotheses can depend on previous ones, sorevert might fail, where with a normal match, since it goes in last to first order, I'm sure that revert will always succeed

Guillaume Melquiond (Aug 25 2022 at 18:25):

Actually, that is the reason I suggested you to use match reverse goal. But indeed, I stand corrected, match goal is already reversed (and match reverse goal is thus normal order). One learns something new every day.

Notification Bot (Aug 30 2022 at 15:30):

Thibaut Pérami has marked this topic as resolved.

Last updated: Apr 18 2024 at 14:02 UTC