Stream: Coq users

Topic: Clearing trivial hypotheses

João Mendes (Apr 16 2023 at 22:58):

I know clear tactic allows to remove either all hypotheses or the hypothesis which has a label given as parameter. But is there any way I could use clear (or even another tactic) to remove only all literal True hypotheses without the needing to refer to their labels?

Patrick Nicodemus (Apr 16 2023 at 22:59):

João Mendes said:

I know clear tactic allows to remove either all hypotheses or the hypothesis which has a label given as parameter. But is there any way I could use clear (or even another tactic) to remove all literal True hypotheses without the needing to refer to their labels?

It may be that you're looking for something more concise than this but you can do this with

repeat (match goal with
| [H : True |- _ ] => clear H
end)

João Mendes (Apr 16 2023 at 23:09):

Thanks, this already helps!

João Mendes (Apr 16 2023 at 23:12):

Btw, one question: what is the role the [...] after the | plays in this code?

Patrick Nicodemus (Apr 16 2023 at 23:53):

Sometimes an example is easier?

match goal with
| [ H1 : ?A = _  |- ?A = _  ] => rewrite H1
end

The left and right brackets [ ] enclose a pattern to match a sequent.

The arrow => demarcates this pattern from an Ltac command on the right, which executes if the pattern is matched, and may refer to variables introduced in the pattern
Left of the turnstile symbol |- is a list of hypotheses to match, right is the goal to match.
This code will search for a hypothesis of the form ?A = _ for some A. If the goal is of the form ?A = _ (for the same ?A in the hypothesis!), it will rewrite using the equation H1.

Patrick Nicodemus (Apr 16 2023 at 23:55):

Or

match goal with
| [ H :  _ < ?B |-  _ < ?B ] => refine (lt_trans _ H)
end

Patrick Nicodemus (Apr 16 2023 at 23:56):

will search for a hypothesis of the form ?A < ?B, and if the goal is of the form ?C < ?B, we will reduce it to proving ?A < ?C.

Patrick Nicodemus (Apr 16 2023 at 23:56):

This is pseudocode i'm writing from memory, syntax errors may result

Patrick Nicodemus (Apr 17 2023 at 00:00):

The documentation is here
https://coq.github.io/doc/v8.11/refman/proof-engine/ltac.html#coq:tacn.match-goal
but in my experience most people are not great at reading the backus naur grammar of a language and suddenly going "Of course, it's immediately clear how to solve all engineering problems using this tool"

Last updated: Oct 04 2023 at 20:01 UTC