Agda:形成所有对 {(x , y) | x 在 xs 中,y 在 ys 中}
Agda: Forming all pairs {(x , y) | x in xs, y in ys}
我想知道在 Agda 中处理列表推导或笛卡尔积的最佳方法是什么。
我有两个向量,xs
和 ys
。我想要(非正式的)集合 {(x , y) | xs 中的 x,ys 中的 y }.
我可以使用 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
我不知道如何构建这样的见证。据我所知,我失去了太多的向量原始结构,无法使用我的归纳案例。
我在想
- 标准库中是否有处理这种 "all pairs" 操作的东西,已经有像这样证明的引理?
- 如果没有,我该如何构建配对见证?
我已经上传 a self-contained version of the code 所有正确的导入,让您更轻松地使用代码。
这里重要的是查看当 运行 allPairs
时获得的最终向量的结构:您获得具有精确模式的 m
大小 n
的块.
第一个块列出了由 xv
的头部和 yv
中的每个元素组成的对。
(...)
第 n 个块列出了由 xv
的第 n 个元素和 yv
中的每个元素组成的对。
所有这些块都是通过连接 (_++_
) 组装而成的。为了能够 select 一个块(因为你正在寻找的 x
在其中)或跳过它(因为 x
更远),你将因此介绍描述 _++_
和 _∈_
.
之间相互作用的中间定理
您应该能够知道如何 select 一个块(如果 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)
最后,一旦您 select 编辑了正确的块,您会注意到它是使用 map
创建的,如下所示:Vec.map (λ y -> (x , y)) ys
。好吧,你可以证明的一件事是 map
与成员证明兼容:
_∈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
我想知道在 Agda 中处理列表推导或笛卡尔积的最佳方法是什么。
我有两个向量,xs
和 ys
。我想要(非正式的)集合 {(x , y) | xs 中的 x,ys 中的 y }.
我可以使用 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
我不知道如何构建这样的见证。据我所知,我失去了太多的向量原始结构,无法使用我的归纳案例。
我在想
- 标准库中是否有处理这种 "all pairs" 操作的东西,已经有像这样证明的引理?
- 如果没有,我该如何构建配对见证?
我已经上传 a self-contained version of the code 所有正确的导入,让您更轻松地使用代码。
这里重要的是查看当 运行 allPairs
时获得的最终向量的结构:您获得具有精确模式的 m
大小 n
的块.
第一个块列出了由
xv
的头部和yv
中的每个元素组成的对。(...)
第 n 个块列出了由
xv
的第 n 个元素和yv
中的每个元素组成的对。
所有这些块都是通过连接 (_++_
) 组装而成的。为了能够 select 一个块(因为你正在寻找的 x
在其中)或跳过它(因为 x
更远),你将因此介绍描述 _++_
和 _∈_
.
您应该能够知道如何 select 一个块(如果 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)
最后,一旦您 select 编辑了正确的块,您会注意到它是使用 map
创建的,如下所示:Vec.map (λ y -> (x , y)) ys
。好吧,你可以证明的一件事是 map
与成员证明兼容:
_∈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