PLFA书籍List章节Any-∃练习：有效类型签名及语法疑问

首先得说你踩的这个坑很典型——题目里的∃[ x ∈ xs ] P x是数学上的直观写法，直接套进Agda里肯定会报错，因为Agda的Σ（依赖对）要求第一个参数是类型（Set），而xs是List A的一个具体值，不是类型，这就是你看到List A !=< Set错误的核心原因。

先明确目标类型的正确写法 #

题目里的∃[ x ∈ xs ] P x想要表达的是：存在某个元素x，它在列表xs里，并且P x成立。在Agda里，我们需要用列表的成员关系谓词_∈_（PLFA的List章节已经定义过，用来表示元素属于列表的证明）来构建对应的Σ类型，正确的目标类型应该是：

Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ Σ[ x ∈ A ] (x ∈ xs × P x)

如果想让它更贴合题目里的写法，你可以先给这个“列表上的存在量词”定义一个别名：

-- 模拟题目里的 ∃[x ∈ xs] P x 写法
∃∈ : {A : Set} (P : A → Set) (xs : List A) → Set
∃∈ P xs = Σ[ x ∈ A ] (x ∈ xs × P x)

-- 这样目标类型就更直观了
Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ ∃∈ P xs

证明同构的两个方向 #

同构需要实现两个方向的转换函数，并且证明它们互为逆函数：

1. 从Any P xs到∃∈ P xs（to函数）

递归处理Any的构造器：

• 如果是here px：当前元素就是列表的头x，x ∈ x ∷ xs的证明是here refl，加上px就组成了对应的依赖对(x , (here refl , px))。
• 如果是there any：递归处理any得到(y , (y∈xs , py))，然后把y∈xs转换成there y∈xs（因为y在剩余列表里，所以在整个列表里的位置是there），得到(y , (there y∈xs , py))。

代码示例：

to : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs → ∃∈ P xs
to (here px) = (_ , (here refl , px))
to (there any) with to any
... | (y , (y∈xs , py)) = (y , (there y∈xs , py))

2. 从∃∈ P xs到Any P xs（from函数）

我们需要把“元素x + x在xs里的证明 + P x的证明”转换成Any P xs。利用_∈_和Any的对应关系：如果x ∈ xs且P x成立，那么必然存在Any P xs的证明。递归处理x ∈ xs的构造器：

• 如果x ∈ xs是here refl：直接返回here px。
• 如果x ∈ xs是there y∈xs：递归处理y∈xs和px，得到there (from (x , (y∈xs , px)))。

代码示例：

from : ∀ {A : Set} {P : A → Set} {xs : List A} → ∃∈ P xs → Any P xs
from (x , (here refl , px)) = here px
from (x , (there y∈xs , px)) = there (from (x , (y∈xs , px)))

3. 证明互为逆函数

最后需要证明to ∘ from ≡ id和from ∘ to ≡ id，用归纳法就能搞定：

• 对于to ∘ from ≡ id，分x ∈ xs是here还是there的情况，分别化简即可。
• 对于from ∘ to ≡ id，分Any是here还是there的情况，递归归纳即可。

为什么这两个结构同构？ #

本质上，Any P xs就是“列表中存在满足P的元素”的证明，它的构造器here和there对应了元素在列表中的位置；而Σ[ x ∈ A ] (x ∈ xs × P x)是用依赖对打包了三个信息：元素本身、元素在列表里的位置证明、元素满足P的证明。这两个结构是一一对应的，所以它们是同构的。

内容的提问来源于stack exchange，提问作者Marko Grdinić