Agda: Para wektorów o tej samej długości

Question

W Agdzie, jak zdefiniować parę wektorów, które muszą mieć tę samą długość?

-- my first try, but need to have 'n' implicitly 
b : ∀ (n : ℕ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n) 
b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ []) 
b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ []) 
b _ = _ 

-- how can I define VecSameLength correctly? 
VecSameLength : Set 
VecSameLength = _ 

c : VecSameLength 
c = (1 ∷ 2 ∷ []) , (1 ∷ 2 ∷ []) 

d : VecSameLength 
d = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ []) 

-- another try 
VecSameLength : Set 
VecSameLength = Σ (Vec ℕ ?) (λ v → Vec ℕ (len v)) 

Answer 1

Jeśli chcesz zachować długość jako część typu, wystarczy spakować dwa wektory o tym samym indeksie rozmiaru. Niezbędnego importu pierwsze:

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

nic extra nadzwyczajnego: po prostu jak można napisać zwykły wektor wielkości n, można to zrobić:

2Vec : ∀ {a} → Set a → ℕ → Set a 
2Vec A n = Vec A n × Vec A n 

Oznacza to, 2Vec A n jest typ par wektorów A s, oba z elementami n. Zwróć uwagę, że skorzystałem z okazji, aby uogólnić ją na arbitralny poziom wszechświata - co oznacza, że ​​możesz mieć wektory Set s, na przykład.

Drugą użyteczną rzeczą, na którą warto zwrócić uwagę, jest to, że użyłem _×_, która jest zwykłą, nieuzależnioną parą. Jest zdefiniowany jako Σ jako specjalny przypadek, w którym drugi składnik nie zależy od wartości pierwszej.

I zanim przejdę do przykładu, gdzie chcemy chce zachować rozmiar ukryty, oto przykładowa wartość tego typu:

test₁ : 2Vec ℕ 3 
-- We can also infer the size index just from the term: 
-- test₁ : 2Vec ℕ _  
test₁ = 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ [] 

Można sprawdzić, że Agda słusznie narzeka podczas próby wlać dwa wektory o nierównej wielkości do tej pary.

Ukrywanie indeksów jest zadaniem dokładnie dostosowanym do pary zależnej. Jako starter, oto jak chcesz ukryć długość jednego wektora:

data SomeVec {a} (A : Set a) : Set a where 
    some : ∀ n → Vec A n → SomeVec A 

someVec : SomeVec ℕ 
someVec = some _ (0 ∷ 1 ∷ []) 

Indeks rozmiar jest utrzymywane poza podpisem typu, więc wiemy tylko, że wektor wewnątrz ma trochę Nieznany Rozmiar (efektywnie dając ci listę). Oczywiście pisanie nowego typu danych za każdym razem, gdy potrzebowalibyśmy ukryć indeks, byłoby męczące, więc standardowa biblioteka daje nam Σ.

someVec : Σ ℕ λ n → Vec ℕ n 
-- If you have newer version of standard library, you can also write: 
-- someVec : Σ[ n ∈ ℕ ] Vec ℕ n 
-- Older version used unicode colon instead of ∈ 
someVec = _ , 0 ∷ 1 ∷ [] 

Teraz łatwo możemy zastosować to do rodzaju 2Vec podanej powyżej:

∃2Vec : ∀ {a} → Set a → Set a 
∃2Vec A = Σ[ n ∈ ℕ ] 2Vec A n 

test₂ : ∃2Vec ℕ 
test₂ = _ , 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ [] 

---

copumpkin podnosi doskonały punkt: można dostać taką samą gwarancję tylko za pomocą listę par . Te dwie reprezentacje kodują dokładnie te same informacje, spójrzmy.

Tutaj użyjemy innej listy importu, aby zapobiec kolizji nazw:

open import Data.List 
open import Data.Nat 
open import Data.Product as P 
open import Data.Vec as V 
open import Function 
open import Relation.Binary.PropositionalEquality 

Idąc od dwóch wektorów do jednej listy jest sprawą skompresowanie dwóch wektorów razem:

vec⟶list : ∀ {a} {A : Set a} → ∃2Vec A → List (A × A) 
vec⟶list (zero , []  , [])  = [] 
vec⟶list (suc n , x ∷ xs , y ∷ ys) = (x , y) ∷ vec⟶list (n , xs , ys) 

-- Alternatively: 
vec⟶list = toList ∘ uncurry V.zip ∘ proj₂ 

Powrót polega na rozpakowaniu - pobranie listy par i utworzenie pary list:

list⟶vec : ∀ {a} {A : Set a} → List (A × A) → ∃2Vec A 
list⟶vec [] = 0 , [] , [] 
list⟶vec ((x , y) ∷ xys) with list⟶vec xys 
... | n , xs , ys = suc n , x ∷ xs , y ∷ ys 

-- Alternatively: 
list⟶vec = ,_ ∘ unzip ∘ fromList 

Nie w, wiemy jak dostać się z jednej reprezentacji do drugiej, ale wciąż musimy pokazać, że te dwie reprezentacje dostarczają nam tych samych informacji.

Po pierwsze, pokazujemy, że jeśli zrobimy listę, przekonwertujemy ją na wektor (przez list⟶vec), a następnie z powrotem na listę (przez vec⟶list), wtedy otrzymamy tę samą listę z powrotem.

pf₁ : ∀ {a} {A : Set a} (xs : List (A × A)) → vec⟶list (list⟶vec xs) ≡ xs 
pf₁ []  = refl 
pf₁ (x ∷ xs) = cong (_∷_ x) (pf₁ xs) 

A potem na odwrót: najpierw wektor do listy, a następnie wymienić na wektorze:

pf₂ : ∀ {a} {A : Set a} (xs : ∃2Vec A) → list⟶vec (vec⟶list xs) ≡ xs 
pf₂ (zero , []  , [])  = refl 
pf₂ (suc n , x ∷ xs , y ∷ ys) = 
    cong (P.map suc (P.map (_∷_ x) (_∷_ y))) (pf₂ (n , xs , ys)) 

W przypadku, gdy zastanawiasz się co cong robi:

cong : ∀ {a b} {A : Set a} {B : Set b} 
     (f : A → B) {x y} → x ≡ y → f x ≡ f y 
cong f refl = refl 

Mamy wykazano, że list⟶vec wraz z vec⟶list tworzą izomorfizm między List (A × A) i ∃2Vec A, co oznacza, że ​​te dwie reprezentacje to izomorficzna.