Agda证明¬Any≃All¬时λ表达式间的解析错误问题

目标定理与已定义函数 #

要证明的等价性定理：

¬Any≃All¬ : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs

已实现的to/from转换函数：

to [] t = []
to (x :: xs) v = (v ∘ here) ∷ to xs (v ∘ there)

from [] [] ()
from (x :: xs´) (¬Px ∷ ¬Pxs´) = λ { (here Px) → ¬Px Px ; (there Pxs´) → (from xs´ ¬Pxs´) Pxs´}

待完成的往返相等证明目标：

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v 

解析错误的核心原因与修复方案 #

在使用≡⟨⟩连接λ表达式时出错，本质是Agda的语法解析规则约束，常见问题及解决方式：

1. λ表达式的括号缺失
   Agda对λ项的边界识别严格，若直接将无括号的λ作为等式两侧的项，会触发解析歧义。必须给λ表达式包裹括号，例如将：

λ { (here Px) → ... ; (there p) → ... } ≡⟨⟩ λ { (here Px) → ... ; (there p) → ... }

改为：

(λ { (here Px) → ... ; (there p) → ... }) ≡⟨⟩ (λ { (here Px) → ... ; (there p) → ... })

2. λ模式分支的格式问题
   花括号模式的λ要求所有分支缩进一致，分号后需保证正确的空格对齐。若分支缩进混乱，Agda会无法识别模式结构，需统一分支的缩进层级。

3. 归纳证明的上下文错误
   在处理x :: xs的归纳情况时，递归调用FromTo xs (v ∘ there)需通过cong来关联函数部分的等式，否则会导致λ项与递归步骤的语法冲突。

修正后的示例代码 #

以xs = x :: xs的归纳步骤为例，正确的证明结构如下：

open import Relation.Binary.PropositionalEquality using (_≡_; cong; refl; begin_; _≡⟨⟩_; _∎)

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v 
FromTo [] v = refl
FromTo (x :: xs) v =
  begin
    from (x :: xs) (to (x :: xs) v)
  ≡⟨⟩
    from (x :: xs) ((v ∘ here) ∷ to xs (v ∘ there))
  ≡⟨⟩
    (λ { (here Px) → (v ∘ here) Px ; (there p) → from xs (to xs (v ∘ there)) p })
  ≡⟨ cong (λ f → λ { (here Px) → (v ∘ here) Px ; (there p) → f p }) (FromTo xs (v ∘ there)) ⟩
    (λ { (here Px) → v (here Px) ; (there p) → (v ∘ there) p })
  ≡⟨⟩
    v
  ∎

额外检查项 #

• 确认已正确导入Relation.Binary.PropositionalEquality中的相关符号，以及Data.List、Data.Any、Data.All等依赖模块。
• 验证≃的定义是否正确导入（通常来自Relation.Binary），避免因类型不匹配导致的隐性错误。

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