Stream: Coq users

Topic: ✔ Run a tactic on all hypothesis once


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 30 2022 at 15:30):

Thibaut Pérami has marked this topic as resolved.


Last updated: Jun 18 2024 at 09:02 UTC