coq 中“|-”的含义是什么，我如何找到其他看似未记录的符号的定义？答案

【问题标题】：What is the meaning of "|-" in coq, and how do I find the definitions for the other seemingly undocumented notations?coq 中“|-”的含义是什么，我如何找到其他看似未记录的符号的定义？
【发布时间】：2021-01-28 20:43:32
【问题描述】：

coq 中的“|-”是什么意思？它似乎用于可能引用术语或模式的地方，例如：

 simpl in |- *.

或者，来自 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.

但 coq 参考手册只说它已加载到前奏中，可能会被覆盖。虽然标准库文档什么也没说。除此之外，搜索、定位、检查、打印、展开等命令似乎也无法提供任何相关信息。

“[=”和“**”更加神秘，因为我只知道存在，因为手册说它们是在前奏中加载的。

【问题讨论】：

标签： coq

【解决方案1】：

|- 令牌记录在 in the reference manual under goal_occurences 中。其含义通常是将假设与目标分开，因为|- 是⊢ 的ASCII 格式，在数学中用于相同目的。所以simpl in * |- 表示“假设中的simpl”，simpl in |- * 表示“目标中的simpl”，而simpl in H |- * 表示“H 中的simpl 也是目标”。不幸的是，simpl 的语法没有记录（我已经将此报告为错误here），但rewrite 的语法记录在here。

match goal 中的 |- 的语法记录在 here 中，用于区分假设模式和目标模式的相同目的。

一般来说，定位战术的最佳位置是the tactic index in the reference manual，但我认为这些不是您所说的正确战术。我认为您正在考虑intros ** 和intros [= H]，它们都是介绍模式。见this documentation of intros。特别是the grammar for intropattern_list 说：

[= intropattern*, ] — 如果产品超过相等类型，则应用 injection 或 discriminate。如果注入适用，intropattern 将用于injection 生成的假设。如果模式数小于生成的假设数，则使用模式? 来完成列表。示例

** — 从结果中引入一个或多个量化变量或假设，直到没有更多量化变量或含义 (->)。 intros ** 等价于 intros。示例

【讨论】：