What is the meaning of "|-" in coq, and how do I find the definitions for the other seemingly undocumented notations?

user_9767589 0
Viewed 112

What does the "|-" mean in coq? It seems to be used where one might reference a term or pattern for example:

 simpl in |- *.

or, from Coq.Init.Tauto,

Local Ltac not_dep_intros :=
  repeat match goal with
  | |- (forall (_: ?X1), ?X2) => intro
  | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
  end.

But the coq reference manual only says it's loaded in the prelude and may be over written. While the standard library documentation says nothing. On top of that commands like Search, Locate, Check, Print, Unfold, etc. don't seem to be able to give any information on that either.

"[=" and "**" are even more mysterious as I only know the exist because the manual says they are loaded in the prelude.

coq
1 Answers

The |- token is documented in the reference manual under goal_occurences. The meaning is generally to separate the hypotheses from the goals, as |- is the ASCII rendition of ⊢ which is used in mathematics for the same purpose. So simpl in * |- means "simpl in the hypotheses" and simpl in |- * means "simpl in the goal" while simpl in H |- * means "simpl in H and also the goal". Unfortunately the syntax is not documented for simpl (I've reported this as a bug here), but it is documented here for rewrite.

The syntax for |- in match goal is documented here, and serves the same purpose of dividing hypothesis patterns from goal patterns.

Generally, the best place to locate tactics is in the tactic index in the reference manual, but I think these are not proper tactics that you are talking about. I think you are thinking of intros ** and intros [= H], which are both intro patterns. See this documentation of intros. In particular the grammar for intropattern_list says:

  • [= intropattern*, ] — If the product is over an equality type, applies either injection or discriminate. If injection is applicable, the intropattern is used on the hypotheses generated by injection. If the number of patterns is smaller than the number of hypotheses generated, the pattern ? is used to complete the list. Example
  • ** — introduces one or more quantified variables or hypotheses from the result until there are no more quantified variables or implications (->). intros ** is equivalent to intros. Example
user_3770220
Related