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.

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`

.

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, so`revert`

might fail, where with a normal match, since it goes in last to first order, I'm sure that revert will always succeed

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.

Thibaut Pérami has marked this topic as resolved.

Last updated: Jun 18 2024 at 09:02 UTC