Stream: Coq users

Topic: ✔ Basic tactics q

Patrick Nicodemus (May 06 2022 at 22:57):

How can I use Ltac to do something along the lines of "for each hypothesis matching this pattern, do this".

Patrick Nicodemus (May 06 2022 at 22:59):

I know I have to use match goal but I think that match goal only finds the first hypothesis matching the pattern and then moves on. I want to do this to all hypotheses matching the pattern.

Notification Bot (May 06 2022 at 23:15):

Patrick Nicodemus has marked this topic as resolved.

Patrick Nicodemus (May 06 2022 at 23:16):

nvm I think I found the answer in the coq docs, I can do this with

match goal with
| [ H : pattern |- _ ] => // do what I want ; fail
| _ => idtac
end

but lmk if there's a better way or if this is not like, idiomatic

Paolo Giarrusso (May 07 2022 at 06:01):

fail will undo what you did in the branch. I'd add repeat around match goal, but then you need to avoid infinite loops

Patrick Nicodemus (May 07 2022 at 06:06):

Paolo Giarrusso said:

fail will undo what you did in the branch. I'd add repeat around match goal, but then you need to avoid infinite loops

Ah, ok, I see. Yeah I am running into what I think is an ltac bug in this specific context ( https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Match.20on.20type.20of.20t.20-.20bug.3F )

which makes the problem of avoiding the loop harder. I was hoping there was some native command to just go through everything once.

Last updated: Sep 26 2023 at 13:01 UTC