Say I have a hypothesis H : a = a -> Hc /\ Hd -> ... -> He.

To make use of He, I have to assert a = a, prove it, assert Hc /\ Hd, prove it, ... then specialize H.

Is there a better way to somehow `auto`

all the trivial stuff when doing forward reasoning?

More generally, for forward reasoning, are there better ways than to use pose proof and specialize over and over?

I used to advertise `especialize`

tactic from LibHyps, which allowed for `especialize H at 1,2,4`

, `especialize H at *`

or `especialize H until 3`

. But it is currently broken with the latest coq versions because of a change in the regular `specialize`

tactic.

stdpp has a few tactics for this. They were added in this MR here: https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512

if the forward reasoning is at first order or propositional level, I think best option is to use a powerful automation tactic rather than messing with hypotheses:

`itauto`

from https://gitlab.inria.fr/fbesson/itauto`sauto`

from https://github.com/lukaszcz/coqhammer

Both are available in the Coq Platform.

@Pierre Courtieu : wasn't there an update to LibHyps to fix this (we complained about this from Coq Platform side). Or is it broken again?

latest discussion is here, to my knowledge the version without `especialize`

is going to be in the next Platform: https://github.com/Matafou/LibHyps/issues/14

There is also the `forward`

tactic that is defined in Equations: https://github.com/mattam82/Coq-Equations/blob/main/theories/Init.v#L148

As the comment suggests it should be part of the standard library.

```
Ltac forward_gen H tac :=
match type of H with
| forall (_ : ?X), _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
end.
Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
```

I confirm: I could not fix `especialize`

in latest coq versions. That said I have been asking for opinions there and am a bit stuck on these subjects currently.

Thanks for the responses! `forward`

is very nice for how simple it is.

Last updated: Jun 23 2024 at 05:02 UTC