Агда: формирование всех пар {(x, y) | х в хс, у в ys}

Я загрузил автономную версию кода со всеми нужными импортами, чтобы упростить для вас, чтобы играть с кодом.

Здесь важно увидеть структуру конечного вектора, который вы получите при запуске allPairs: вы получите m фрагментов размера n с точным шаблоном.

• В первом фрагменте перечислены пары, состоящие из головы xv вместе с каждым из элементов yv.

• (...)

• N-й блок содержит пары, состоящие из n-го элемента xv вместе с каждым из элементов yv.

Все эти фрагменты собираются конкатенацией (_++_). Чтобы иметь возможность либо выбрать один фрагмент (поскольку x, который вы ищете, находится в нем), либо пропустить его (поскольку x находится дальше), вы собираетесь ввести промежуточные теоремы, описывающие взаимодействие между _++_ и _∈_.

Вы должны знать, как выбрать фрагмент (в случае, если 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)

Наконец, как только вы выбрали правильный фрагмент, вы можете заметить, что он был создан с использованием 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