如何让Agda展开定义以证明foo c c≡123等价性命题

你无法直接用refl完成证明的核心原因是：Agda标准库中Char类型的布尔相等运算符_==_是基于可判定相等（Decidable Equality）封装得到的，不会对未知具体值的变量参数自动归约为true。当你传入具体字符字面量（比如'a'）时，Agda可以直接计算出'a' == 'a' = true，因此可以直接归约foo 'a' 'a'得到123；但当参数是任意变量c时，Agda无法预判c == c的判定结果，因此无法自动完成beta归约。

首先证明辅助引理：对任意字符c，c == c恒等于true，再用rewrite将函数中的判定条件替换为true，即可直接用refl完成主命题证明，完整代码如下：

open import Data.Char
open import Data.Nat
open import Data.Bool
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true  = 123
... | false = 456

-- 辅助引理：任意字符与自身的布尔相等判定结果恒为true
c==c : ∀ (c : Char) → (c == c) ≡ true
c==c c with c ≟ c
... | yes refl = refl
... | no  neq  = ⊥-elim (neq refl)

-- 主定理证明
foo-eq⇒123 : ∀ (c : Char) → foo c c ≡ 123
foo-eq⇒123 c rewrite c==c c = refl

代码说明 #

• _≟_是Char类型原生的可判定相等接口，返回Dec (c ≡ c)类型：yes p分支携带c ≡ c的证明，no np分支携带¬ (c ≡ c)（即c与c不可能相等）的证明。
• 对c ≟ c分情况讨论时：
  • yes refl分支下，c == c会自动归约为true，直接用refl即可证明引理。
  • no neq分支是不可能存在的矛盾分支：我们将自反性证明refl传入neq即可得到假值，用⊥-elim消去该分支。
• 主定理中使用rewrite c==c c将foo c c定义中c == c的判定位置替换为true，此时foo c c直接归约为123，用refl即可完成证明。

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