Coq定理证明中遇到‘false=true’矛盾前提时的处理方法

当前分支下的假设H : false = true属于Coq中典型的不可满足矛盾前提：true和false是布尔类型的两个不同归纳构造子，二者从定义上就不可能相等。
根据Coq的基础逻辑规则，从矛盾命题出发可以推导出任意结论（即逻辑中的爆炸原理），因此你完全不需要真的逐字证明Var 0 = Var (S n)这个目标，只需要利用系统提供的矛盾检测策略即可快速闭合分支。

• 在当前目标状态下，直接执行discriminate H即可闭合该分支
  该策略会自动识别到等式两侧是同一归纳类型的不同构造子，利用“不同构造子生成的项必然不等”的内置判定，从矛盾假设直接完成目标证明。
• 该分支闭合后，回到归纳证明的剩余分支：
  1. 当归纳变量x为S x'时，对n做destruct n拆分：
     • 若n为O：化简后前提会变为H: false = true，同样调用discriminate H闭合目标
     • 若n为S n'：化简后前提变为H: equals x' n' = true，此时直接应用之前的归纳假设IH（即对任意n，equals x' n = true → Var x' = Var n），即可得到Var x' = Var n'，再对该等式两边应用f_equal，即可推导出Var (S x') = Var (S n')，完成目标。

Proof.
  intros x n. induction x as [| x' IH].
  (* x为0的分支 *)
  - destruct n. 
    + reflexivity. (* n也为0时，equals 0 0 = true，等式直接自反成立 *)
    + simpl. intro H. discriminate H.
  (* x为S x'的分支 *)
  - destruct n.
    + (* n为0的情况，前提矛盾 *)
      simpl. intro H. discriminate H.
    + (* n为S n'的情况，应用归纳假设完成证明 *)
      simpl. intro H. apply IH in H. f_equal. exact H.
Qed.

补充说明：上述证明的核心逻辑和标准库中自然数相等判定的等价性定理完全一致——对于任意两个自然数，相等判定函数返回true当且仅当两个自然数本身相等，此时再配合Var构造子的注入性（即两个Var项相等当且仅当内部存储的自然数相等），就可以自然推导出你要证明的结论。

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