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.
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
The question mark is used to mark the symbol as an Ltac variable and not as a Coq variable/identifier/term
Last updated: Oct 04 2023 at 23:01 UTC