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

Question

I'm wondering what the best way to approach list-comprehensions or cartesian products in Agda is.

What I have is two vectors, xs and ys. I want the (informal) set {(x , y) | x in xs, y in ys }.

I can fairly easily form this set using map and 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 )

From here, I'd like something for getting a witness for pairs, something like:

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

I don't know how to construct such a witness. As far as I can tell, I lose too much of the original structure of the vectors to be able to use my inductive cases.

I'm wondering

Is there something in the standard library dealing with this kind of "all pairs" operation, that would already have lemmas proved like this?
If not, how do I go about constructing pair witness?

gallais gallais · Accepted Answer · 2015-07-14T01:28:31

I've uploaded a self-contained version of the code with all the right imports to make it easier for you to play with the code.

What's important here is to see the structure of the final vector you obtain when running allPairs: you obtain m chunks of size n with a precise pattern.

The first chunk is listing the pairs composed of the head of xv together with each one of the elements in yv.
(...)
The nth chunk is listing the pairs composed of the nth element of xv together with each one of the elements in yv.

All these chunks are assembled by concatenation (_++_). To be able to either select one chunk (because the x you're looking for is in it) or skip it (because the x is further away), you are therefore going to introduce intermediate theorems describing the interaction between _++_ and _∈_.

You should be able to know how to select a chunk (in case x is in this one) which corresponds to this easy intermediate lemma:

_∈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)

But you should also be able to skip a chunk (in case x is further away) which corresponds to this other lemma:

_∈_++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)

Finally, once you have selected the right chunk, you can notice that it has been created using map like so: Vec.map (λ y -> (x , y)) ys. Well, one thing you can prove is that map is compatible with membership proofs:

_∈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)

You can now put all of this together and produce the witness by induction on the proof that 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: Forming all pairs {(x , y) | x in xs, y in ys}

1 Answers