Agda中Any? Decide-N-Even [5]的no证明与扩展lambda错误

相关代码实现 #

Any?谓词定义 #

Any? P? (x :: xs) with P? x   | Any? P? xs
...                   | yes Px      |     _         =   yes (here Px)
...                   |     _       |    yes Pxs    =   yes (there Pxs)
...                   | no ¬Px      |  no ¬AnyPxs   =   no (λ {(here Px) → ¬Px Px ; (there Pxs) → ¬AnyPxs Pxs})

自然数偶数判定及辅助证明 #

Decide-N-Even : ∀ (n : ℕ) → Dec (even n)
Decide-N-Even 0 = yes zero
Decide-N-Even (suc n) with Decide-N-Even n
...                      | no ¬EvenN = yes (suc (¬-even→odd n ¬EvenN))
...                      | yes evenN = no (λ {(suc OddN) → (even→¬odd n evenN) OddN})

¬5Even : ¬ (even 5)
¬5Even 5IsEven = (even→¬odd 5 5IsEven) (suc (suc (suc (suc (suc zero)))))

验证问题 #

直接验证失败 #

尝试直接用refl验证Any? Decide-N-Even [5]的结果时无法通过：

_ : (Any? Decide-N-Even [ 5 ]) ≡ no (λ { (here 5IsEven) → ¬5Even 5IsEven})
_ = refl

而返回yes的场景（如[5,4,3]）可正常通过refl验证。

辅助函数尝试的错误信息 #

使用辅助函数时出现以下错误：

(λ { (here 5IsEven) → ¬5Even 5IsEven ; (there ()) }) x !=
(λ { (here 5IsEven) → ¬5Even 5IsEven ; (there ()) }) x of type ⊥
Because they are distinct extended lambdas: one is defined at

   Lists10.agda:1101,91-127
and the other at
   Lists10.agda:1099,38-74,
so they have different internal representations.
when checking that the inferred type of an application
  Any? Decide-N-Even [ 5 ] ≡
  no (λ { (here 5IsEven) → ¬5Even 5IsEven ; (there ()) })
matches the expected type
  Any? Decide-N-Even [ 5 ] ≡
  no (λ { (here 5IsEven) → ¬5Even 5IsEven ; (there ()) })

解决方案 #

核心原因是Agda默认的定义相等不包含函数外延相等——即使两个lambda行为完全一致，只要不是同一处定义的，就不会被判定为相等。以下是两种可行解决方法：

方法1：引入命题外延性公理 #

通过公理声明“若两个函数对所有输入的输出都相等，则函数本身相等”，以此证明两个lambda的等价性：

open import Relation.Binary.PropositionalEquality

-- 声明命题外延性公理
postulate
  fun-ext : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

-- 完成验证
any-5-even≡no : Any? Decide-N-Even [5] ≡ no (λ {(here 5IsEven) → ¬5Even 5IsEven})
any-5-even≡no with Decide-N-Even 5 | Any? Decide-N-Even []
... | no ¬e | no ¬any = cong no (fun-ext λ { (here px) → refl ; (there ()) })
... | _ | _ = refl -- 其他分支不可能触发

方法2：复用Agda生成的证明项 #

先让Agda自动推断no后的证明项，再直接使用该结果完成验证：

-- 先让Agda补全下划线处的证明项
test : Any? Decide-N-Even [5] ≡ no _
test = refl

-- 复制Agda生成的证明项，替换下划线后即可用refl验证
final-proof : Any? Decide-N-Even [5] ≡ no (λ { (here 5IsEven) → ¬5Even 5IsEven ; (there ()) })
final-proof = refl

方法3：证明Decide-N-Even的结果等价性 #

先证明Decide-N-Even 5生成的否定证明与自定义的¬5Even相等，再结合Any?的计算逻辑完成验证：

decide-5-equiv : Decide-N-Even 5 ≡ no ¬5Even
decide-5-equiv = refl -- 若自动推导失败，可手动展开Decide-N-Even的计算步骤证明

any-5-even≡no : Any? Decide-N-Even [5] ≡ no (λ {(here 5IsEven) → ¬5Even 5IsEven})
any-5-even≡no rewrite decide-5-equiv = cong no (fun-ext λ { (here px) → refl ; (there ()) })

内容的提问来源于stack exchange，提问作者Werner Germán Busch