Stream: Coq users

Topic: ✔ Basic tactics q


view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip Notification Bot (May 06 2022 at 23:15):

Patrick Nicodemus has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: May 20 2024 at 22:01 UTC