为何Coq中S n' =? S n'会简化为n' =? n'？

这个行为不是由公理定义的，而是源于Coq归纳类型的核心特性以及simpl策略的内置逻辑：

• 自然数类型nat是Coq的基础归纳类型，定义如下：

  Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.
  

  其中S是构造子，Coq对归纳类型的构造子有一个内置的单射性规则：如果同一构造子构造的两个项相等，那么它们的参数必然相等。换句话说，若S a = S b，则a = b，这是归纳类型自带的性质，属于Coq核心推理系统的一部分，无需额外公理。
• simpl策略的核心功能是对项进行归约简化，当它遇到等式两边都是S n'形式的项时，会直接应用构造子的单射性规则，将等式简化为对应参数的等式，这是策略内置的简化逻辑，没有依赖额外公理。

简单来说，这是归纳类型构造子的固有特性，simpl只是把这个特性应用到了等式简化中。

内容的提问来源于stack exchange，提问作者wrongbyte