Cartesian product... and proofs

AllPairs.agda

open import Data.Nat
open import Data.Product
open import Data.Vec as Vec

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

infixl 5 _∈xs++_ _∈_++ys _∈map_xs
_∈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)

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

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