Agda: Forming all pairs {(x, y) | x in xs, y in ys}
I am wondering what is the best way to come close to understanding lists or cartesian products in Agde.
I have two vectors, xs
and ys
. I want an (informal) set {(x, y) | x in xs, y in ys}.
I can shape this set quite easily 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 would like something to get a witness for couples, 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 build such a witness. As far as I can tell, I am losing too much of the original vector structure to be able to use my inductive cases.
I'm curious
- Is there something in the standard library dealing with this type of all-pairs operation that already has such lemmas?
- If not, how do I start creating a pair of witnesses?
source to share
I have downloaded a standalone version of the code with all the correct imports to make it easier for you to play with the code.
What's important to see the structure of the final vector that you get when you start allPairs
: you end up with exactly m
sized chunks n
.
-
The first snippet lists the chapter pairs,
xv
along with each of the elements inyv
. -
(...)
-
The n-th block lists the pairs consisting of the n-th item
xv
along with each of the items inyv
.
All these pieces are assembled by concatenation ( _++_
). To be able to select one fragment (because it contains the x
one you are looking for) or skip it (because it x
is further away), you must introduce intermediate theorems describing the interaction between _++_
and _∈_
.
You should be able to know how to pick a piece (in the case x
in this), which corresponds to this simple 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 the chunk (in case it x
is further), 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 chosen the right piece, you can see that it was created with the help of map
the following: Vec.map (λ y -> (x , y)) ys
. So, you can prove to be map
compatible with proof of membership:
_∈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)
Now you can put it all together and inductively induce a witness to prove 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
source to share