types - Agda: Forming all pairs {(x , y) | x in xs, y in ys} -

i'm wondering best way approach list-comprehensions or cartesian products in agda is.

what have 2 vectors, xs , ys. want (informal) set {(x , y) | x in xs, y in ys }.

i can form set using map , concat:

allpairs :  {a : set} -> {m n : ℕ} -> vec m -> vec n -> vec (a × a) (m * n) allpairs xs ys = data.vec.concat (data.vec.map (λ x -> data.vec.map (λ y -> (x , y) ) ys  ) xs ) 

from here, i'd getting witness pairs, like:

pairwitness : ∀ {a} -> {m n : ℕ} -> (xv : vec m) -> (yv : vec n) -> (x : a) -> (y : a) -> x ∈ xv -> y ∈ yv -> (x , y ) ∈ allpairs xv yv 

i don't know how construct such witness. far can tell, lose of original structure of vectors able use inductive cases.

i'm wondering

1. is there in standard library dealing kind of "all pairs" operation, have lemmas proved this?
2. if not, how go constructing pair witness?

i've uploaded a self-contained version of code right imports make easier play code.

what's important here see structure of final vector obtain when running allpairs: obtain m chunks of size n precise pattern.

• the first chunk listing pairs composed of head of xv each 1 of elements in yv.

• (...)

• the nth chunk listing pairs composed of nth element of xv each 1 of elements in yv.

all these chunks assembled concatenation (_++_). able either select 1 chunk (because x you're looking in it) or skip (because x further away), therefore going introduce intermediate theorems describing interaction between _++_ , _∈_.

you should able know how select chunk (in case x in one) corresponds easy intermediate lemma:

_∈xs++_ : {a : set} {x : a} {m : ℕ} {xs : vec m}           (prx : x ∈ xs) {n : ℕ} (ys : vec n) → x ∈ xs ++ ys here     ∈xs++ ys = here there pr ∈xs++ ys = there (pr ∈xs++ ys) 

but should able skip chunk (in case x further away) corresponds other lemma:

_∈_++ys : {a : set} {x : a} {n : ℕ} {ys : vec n}           (prx : x ∈ ys) {m : ℕ} (xs : vec m) → x ∈ xs ++ ys pr ∈ []     ++ys = pr pr ∈ x ∷ xs ++ys = there (pr ∈ xs ++ys) 

finally, once have selected right chunk, can notice has been created using map so: vec.map (λ y -> (x , y)) ys. well, 1 thing can prove map compatible membership proofs:

_∈map_xs : {a b : set} {x : a} {m : ℕ} {xs : vec m}            (prx : x ∈ xs) (f : → b) → f x ∈ vec.map f xs here     ∈map f xs = here there pr ∈map f xs = there (pr ∈map f xs) 

you can put of , produce witness induction on proof x ∈ xs:

pairwitness : {a : set} {m n : ℕ} (xv : vec m) (yv : vec 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