Various uses of turnstile symbol in the following code · Coq users

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):

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

Stream: Coq users

Topic: Various uses of turnstile symbol in the following code

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

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

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

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