## Stream: Coq users

### Topic: Various uses of turnstile symbol in the following code

#### Animated Silicon (mcht) (Apr 30 2023 at 10:32):

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.

#### Gaëtan Gilbert (Apr 30 2023 at 10:35):

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

#### Patrick Nicodemus (Apr 30 2023 at 20:08):

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

#### Gaëtan Gilbert (Apr 30 2023 at 20:11):

yes

Last updated: Jun 18 2024 at 00:02 UTC