types - Agda:形成所有对 {(x , y) | x 在 xs，y 在 ys}

Question

我想知道在 Agda 中处理列表推导式或笛卡尔积的最佳方法是什么。

我有两个向量，xs和 ys .我想要(非正式)集合 {(x , y) | x 在 xs，y 在 ys }。

我可以很容易地使用 map 和 concat 来形成这个集合:

allPairs :  {A : Set} -> {m n : ℕ} -> Vec A m -> Vec A n -> Vec (A × A) (m * n)
allPairs xs ys = Data.Vec.concat (Data.Vec.map (λ x -> Data.Vec.map (λ y -> (x , y) ) ys  ) xs )

从这里开始，我想要一些东西来获得成对的证人，例如:

pairWitness : ∀ {A} -> {m n : ℕ} -> (xv : Vec A m) -> (yv : Vec A n) -> (x : A) -> (y : A) -> x ∈ xv -> y ∈ yv -> (x , y ) ∈ allPairs xv yv

我不知道如何构建这样的见证。据我所知，我失去了太多向量的原始结构，无法使用我的归纳案例。

我很好奇

标准库中是否有处理这种“所有对”操作的东西，这已经证明了引理？

如果没有，我该如何构建配对见证？

Answer 1

我已经上传了 a self-contained version of the code 以及所有正确的导入，以便您更轻松地使用代码。

这里重要的是查看您在运行 allPairs 时获得的最终向量的结构:您以精确的模式获得大小为 m 的 n 块。

第一个块列出了由 xv 的头部和 yv 中的每个元素组成的对。

(...)

第 n 个块列出了由 xv 的第 n 个元素以及 yv 中的每个元素组成的对。

所有这些块都是通过连接 ( _++_) 组装的。为了能够选择一个块(因为您正在寻找的 x 在其中)或跳过它(因为 x 更远)，因此您将引入描述 _++_ 和 _∈_ 之间相互作用的中间定理

您应该能够知道如何选择一个块(如果 x 在这个块中)，它对应于这个简单的中间引理:

_∈xs++_ : {A : Set} {x : A} {m : ℕ} {xs : Vec A m}
          (prx : x ∈ xs) {n : ℕ} (ys : Vec A n) → x ∈ xs ++ ys
here     ∈xs++ ys = here
there pr ∈xs++ ys = there (pr ∈xs++ ys)

但是你也应该能够跳过一个块(如果 x 离得更远)，它对应于另一个引理:

_∈_++ys : {A : Set} {x : A} {n : ℕ} {ys : Vec A n}
          (prx : x ∈ ys) {m : ℕ} (xs : Vec A m) → x ∈ xs ++ ys
pr ∈ []     ++ys = pr
pr ∈ x ∷ xs ++ys = there (pr ∈ xs ++ys)

最后，一旦您选择了正确的块，您会注意到它是使用 map 创建的，如下所示: Vec.map (λ y -> (x , y)) ys 。好吧，您可以证明的一件事是 map 与成员(member)证明兼容:

_∈map_xs : {A B : Set} {x : A} {m : ℕ} {xs : Vec A m}
           (prx : x ∈ xs) (f : A → B) → f x ∈ Vec.map f xs
here     ∈map f xs = here
there pr ∈map f xs = there (pr ∈map f xs)

您现在可以将所有这些放在一起，并通过归纳证明 x ∈ xs 来产生证人:

pairWitness : {A : Set} {m n : ℕ} (xv : Vec A m) (yv : Vec A n)
              {x y : A} -> x ∈ xv -> y ∈ yv -> (x , y) ∈ allPairs xv yv
pairWitness (x ∷ xv) yv here  pry = pry ∈map (λ y → x , y) xs ∈xs++ allPairs xv yv
pairWitness (x ∷ xv) yv (there prx) pry = pairWitness _ _ prx pry ∈ Vec.map (λ y → x , y) yv ++ys