一。

Theorem plus_1_l : ∀ n:nat, 1 + n = S n. Proof. intros n. reflexivity. Qed. Theorem mult_0_l : ∀ n:nat, 0 × n = 0. Proof. intros n. reflexivity. Qed.

上述定理名称的后缀 _l 读作“在左边”。 跟进这些证明的每个步骤，观察上下文及证明目标的变化是非常值得的。 你可能要在 reflexivity 前面加上 simpl 调用，以便观察 Coq 在检查它们的相等关系前进行的化简。

注意

关键词reflexivity ，只有“在左边”的时候，才会生效。

二。

Proof. (* 将两个量词移到上下文中： *) intros n m. (* 将前提移到上下文中： *) intros H. (* 用前提改写目标： *) rewrite → H. reflexivity. Qed.

此时，是把 证明的第一行将全称量词变量 n 和 m 移到上下文中。 第二行将前提 n = m 移到上下文中，并将其命名为 H。 第三行告诉 Coq 改写当前目标（n + n = m + m），把前提等式 H 的左边替换成右边。

改写的内容，是goal或者subgoal中的内容。原则是根据H来替换。

注意

(rewrite 中的箭头与蕴含无关：它指示 Coq 从左往右地应用改写。 若要从右往左改写，可以使用 rewrite <-。在上面的证明中试一试这种改变， 看看 Coq 的反应有何不同。)