Rocq知识点

命令	详细功能说明	举例与输出
`Check`	查看类型。只进行类型推导，不执行计算。	`Check S O.` 输出：`S O : nat`
`Compute`	计算/约化。将表达式计算到无法再简化的“范式”。	`Compute S O + S O.` 输出：`2 : nat`
`Print`	查看定义内容。打印出该名称背后的完整源码。	`Print negb.` 输出：显示该函数的 `match` 分支实现。
`Locate`	定位符号。查找某个记法（如 `+`）属于哪个库。	`Locate "_ + _".` 输出：`Init.Nat.add`
`Search`	搜索定理。在已加载的库中寻找涉及某个谓词的定理。	`Search plus.` 输出：列出所有关于加法的定理。

定义与声明：
- Definition：全局定义。赋予一个名字具体的逻辑/数值。
  - 例：Definition double (n:nat) := n + n.
- Parameter / Axiom：全局声明。只给类型不给值（假设某种公理成立）。
  - 例：Axiom p_is_true : P.
- Variable / Hypothesis：局部声明。通常在 Section（块）中使用。
  - 考试陷阱：Section 结束时，局部变量会消失，但如果在块内定义的函数用到了它，该变量会变成函数的隐藏参数。
构造与递归：
- Inductive：定义归纳类型（如枚举、自然数）。
  - 例：Inductive bool : Set := true | false.
- Fixpoint：定义递归函数。
  - 关键点：必须有一个参数是递减的，以保证递归能够终止。
- match ... with：模式匹配，处理 Inductive 定义的多个分支。
大类 (Sorts)：
- Prop：逻辑命题的类型（Proof-irrelevant，我们只关心它是否可证）。
- Set：规范说明/数据类型的类型（如 nat, bool）。
- Type：顶层的大类。

目标含 A -> B 或 forall x $\rightarrow$ 使用 intros。
- 例：目标 forall n, P n $\xrightarrow{intros\ n}$ 假设区多了一个 n : nat，目标变为 P n。
目标与假设区某项 H 的结论一致 $\rightarrow$ 使用 apply H。
- 例：假设 H : A -> B，目标是 B $\xrightarrow{apply\ H}$ 目标变为 A。
目标已在假设区完全出现 $\rightarrow$ 使用 assumption。
直接提供证明项 $\rightarrow$ 使用 exact H。

目标是 t = t $\rightarrow$ 使用 reflexivity。
- 注：它会自动执行一些简单的计算（如 1+1 变成 2）。
目标需要展开定义或化简 $\rightarrow$ 使用 simpl 或 unfold。
- simpl：根据定义化简计算。
- unfold：手动展开某个名字。例：unfold double 会把 double x 换成 x + x。
假设区有等式 H: a = b $\rightarrow$ 使用 rewrite H。
- 默认是左换右，rewrite <- H 是右换左。

目标是 A /\ B (且) $\rightarrow$ 使用 split。生成两个子目标 A 和 B。
目标是 A \/ B (或) $\rightarrow$ 使用 left 或 right。选择你更有把握证出的那一边。
目标是 exists x, P x (存在) $\rightarrow$ 使用 exists <具体值>。
- 例：目标 exists n, n > 0 $\xrightarrow{exists\ 1}$ 目标变为 1 > 0。
假设区有一个归纳类型项（如 n : nat 或 b : bool） $\rightarrow$ 使用 destruct。
- 作用：分类讨论。如果是 nat，会拆成 n = O 和 n = S n' 两部分证。

自然数 (nat) 的内部表示：
- O 是零，S 是后继（Successor）。
- 2 在 Rocq 内部就是 S (S O)。
- 陷阱：Check 3. 输出是 3 : nat。虽然内部是 S 构造，但界面会显示阿拉伯数字。
Curry-Howard 同构：
- 一个命题（Proposition）的证明（Proof）其实就是一个 Lambda 项。
- 寻找证明的过程就是在寻找一个具有特定类型的项。
证明完成标识：
- Admitted：跳过证明，假设成立。IDE 进度条变黄色。
- Qed：完成证明并检查类型。IDE 进度条变蓝色。

第一步：看目标（Goal）。
- 有 ->？选 intros。
- 有 = ?？看左右是否一样，一样选 reflexivity，不一样看假设区有没有等式选 rewrite。
- 有 /\？选 split。
第二步：看命令类型。
- 如果是询问执行结果，看是 Check（类型）还是 Compute（数值）。