Agda中自定义数据类型可判定相等性（Decidable equality）证明求助

可行性判断 #

该需求可以实现，你的代码整体思路已经正确，只差最后一步矛盾推导。

解决思路 #

你的Test类型只有一个单参数构造子test，包装的String类型本身已实现可判定相等，你已经调用了String._≟_做了分支判断，只需要在否定分支完成反证即可：

• 我们要证明的目标是¬ test x ≡ test x₁，即假设存在test x ≡ test x₁的等式时能推出矛盾
• 单构造子的等式可以直接推出参数相等：通过命题相等的同余性cong，对test x ≡ test x₁做构造子消除就能得到x ≡ x₁
• 这一结论和当前分支的前提¬a : ¬ x ≡ x₁直接矛盾，即可完成证明。

孔洞填充代码 #

你可以直接在孔洞位置填入下面的代码：

λ eq → ¬a (cong (λ (test s) → s) eq)

如果你开启了--pattern-lambda扩展，也可以用更简洁的模式匹配lambda写法：

λ where refl → ¬a refl

注：你贴出的孔洞上下文里将x、x₁标注为ℕ类型属于上下文显示误差，实际代码中两者是String类型，上述证明逻辑对两种场景都通用。

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