Stream: Coq users

Topic: Automation in forward reasoning

view this post on Zulip towokit928 (Apr 30 2024 at 09:31):

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?

view this post on Zulip Pierre Courtieu (Apr 30 2024 at 09:49):

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.

view this post on Zulip Janno (Apr 30 2024 at 09:59):

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

view this post on Zulip Karl Palmskog (Apr 30 2024 at 10:36):

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:

Both are available in the Coq Platform.

view this post on Zulip Michael Soegtrop (Apr 30 2024 at 10:39):

@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?

view this post on Zulip Karl Palmskog (Apr 30 2024 at 10:39):

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

view this post on Zulip Théo Winterhalter (Apr 30 2024 at 11:41):

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.

view this post on Zulip Pierre Courtieu (Apr 30 2024 at 11:54):

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.

view this post on Zulip towokit928 (May 01 2024 at 02:22):

Thanks for the responses! forward is very nice for how simple it is.

Last updated: Oct 13 2024 at 01:02 UTC