Coq中二叉搜索树证明难题：如何用e0:(val=?n)=true证val=n

你碰到的这个子目标其实是Coq里自然数布尔相等判断的核心正确性问题，标准库已经为我们准备好了现成的引理来搞定它。

关键引理：Nat.eqb_eq #

Coq的Arith模块中包含了Nat.eqb_eq引理，它的类型是：

forall x y : nat, (x =? y) = true <-> x = y

这个引理直接说明了自然数的布尔相等判断返回true当且仅当两个数实际相等，完美匹配你的需求——从假设(val =? n) = true推导出val = n。

具体证明步骤 #

首先确保你已经导入了Arith模块（如果还没导入，先在代码开头加Require Import Arith.），然后在当前的第一个子目标下，执行以下命令：

apply Nat.eqb_eq in e0.
exact e0.

或者更简洁的一步到位：

exact (Nat.eqb_eq val n e0).

解释 #

• apply Nat.eqb_eq in e0会把你的假设e0 : (val =? n) = true转换成e0 : val = n，因为引理的方向是从布尔真推导出等式成立。
• 之后exact e0直接用转换后的假设完成目标证明。

解决完这个子目标后，你就可以继续处理剩下的两个子目标了，它们可以通过调用归纳假设IHa1/IHa2结合is_found_node_lt/is_found_node_gt构造器来完成。

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