I am following Adam Chlipala's Formal Reasoning about Programs and saw the following code:

```
Theorem commuter_constantFold : forall e, commuter (constantFold e) = constantFold (commuter e).
Proof.
induct e; simplify;
repeat match goal with
| [ |- context[match ?E with _ => _ end] ] => cases E; simplify
| [ H : ?f _ = ?f _ |- _ ] => invert H
| [ |- ?f _ = ?f _ ] => f_equal
...
```

The only thing I know about it is from Chlipala's repository, which says that it "separates hypotheses and conclusion in a goal". I notice that more stuff appears at the top of the goal window as a result of `[ |- context[match ?E with _ => _ end] ]`

, and so I am guessing that the turnstile is responsible for that. While the `|-`

appears at the very front for the first and third case, it appears at the very back for the second case, and it is also followed by blank.

I am not sure where to look in the documentation to see what it means and how it is used. Any guidance would be greatly appreciated.

https://coq.github.io/doc/master/refman/proof-engine/ltac.html#coq:tacn.match-goal

I had trouble understanding this documentation as a beginner so I will try and explain in my own words to see if it is helpful.

In the expression `[ |- context[match ?E with _ => _ end] `

, this represents a pattern which the match statement tries to match/align with the goal. This is a kind of control flow structure where the expression `[ ... |- ...]`

describes the "if" condition (if the goal is of this form, with hypotheses left of the turnstile and conclusion right of the turnstile) and the expression after the `=>`

is the 'then' expression (do this). One difference between this and the `if _ then _`

of Python, C, Java etc. is that the if-condition is also binding the variable `E`

which is then visible to the tactic to be executed. The way I would read this first branch in English is: If the goal contains a subterm of the form "match E with _ => _ end", where E is arbitrary, then execute the ltac tactic "cases E; simplify" (where E has been set to the value in the match statement)

The second branch reads: if there is a hypothesis of the form `f _ = f _`

for some arbitrary term `f`

, then execute the tactic `invert H`

, where `H`

is the name of that hypothesis

The third branch reads: if the goal is of the form `f _ = f _`

then execute the tactic `f_equal`

.

The question mark is used to mark the symbol as an Ltac variable and not as a Coq variable/identifier/term

yes

Last updated: Jun 18 2024 at 00:02 UTC