I am trying to create new hypothesis using Ltac. I have the following MWE to illustrate my case
Set Default Timeout 1. (* recommended *) Ltac plip' := let H := fresh "H" in assert True as H ; [apply I|]. Ltac plop := repeat match goal with | [ |- False ] => plip' end. Ltac plop' := repeat match goal with | [ H: True |- _ ] => plip' end. Goal False. plip'. (* creates new hypothesis *) Fail plop. (* time out *) Fail plop'. (* time out *) Abort.
plip' always create a new hypothesis. But
plop timeouts. I was expecting to use a match to create the new hypothesis from either current goal or current set of hypothesis.
Any idea what is causing this? I am using Coq 8.16.
Is there a recommended practice to achieve something similar, i.e., create new hypothesis from a given context?
I have a longer code snippet that would benefit from such pattern.
Of course, it is always when you click that you realize that this "repeat" might create a fork bomb ...
Is it safe to assume that
repeat rescans the list of goals every time a match occurs?
Yes, you can replace
do n to see what is happening.
Ltac plop := do 3 match goal with | [ |- False ] => plip' end. Ltac plop' := do 3 match goal with | [ H: True |- _ ] => plip' end.
Jerome Hugues has marked this topic as resolved.
Last updated: Oct 04 2023 at 20:01 UTC