module Data.Vec.Equality where
open import Data.Vec
open import Data.Nat using (suc)
open import Function
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
module Equality {s₁ s₂} (S : Setoid s₁ s₂) where
private
open module SS = Setoid S
using () renaming (_≈_ to _≊_; Carrier to A)
infix 4 _≈_
data _≈_ : ∀ {n¹} → Vec A n¹ →
∀ {n²} → Vec A n² → Set (s₁ ⊔ s₂) where
[]-cong : [] ≈ []
_∷-cong_ : ∀ {x¹ n¹} {xs¹ : Vec A n¹}
{x² n²} {xs² : Vec A n²}
(x¹≈x² : x¹ ≊ x²) (xs¹≈xs² : xs¹ ≈ xs²) →
x¹ ∷ xs¹ ≈ x² ∷ xs²
length-equal : ∀ {n¹} {xs¹ : Vec A n¹}
{n²} {xs² : Vec A n²} →
xs¹ ≈ xs² → n¹ ≡ n²
length-equal []-cong = P.refl
length-equal (_ ∷-cong eq₂) = P.cong suc $ length-equal eq₂
refl : ∀ {n} (xs : Vec A n) → xs ≈ xs
refl [] = []-cong
refl (x ∷ xs) = SS.refl ∷-cong refl xs
sym : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
xs ≈ ys → ys ≈ xs
sym []-cong = []-cong
sym (x¹≡x² ∷-cong xs¹≈xs²) = SS.sym x¹≡x² ∷-cong sym xs¹≈xs²
trans : ∀ {n m l} {xs : Vec A n} {ys : Vec A m} {zs : Vec A l} →
xs ≈ ys → ys ≈ zs → xs ≈ zs
trans []-cong []-cong = []-cong
trans (x≈y ∷-cong xs≈ys) (y≈z ∷-cong ys≈zs) =
SS.trans x≈y y≈z ∷-cong trans xs≈ys ys≈zs
_++-cong_ : ∀ {n₁¹ n₂¹} {xs₁¹ : Vec A n₁¹} {xs₂¹ : Vec A n₂¹}
{n₁² n₂²} {xs₁² : Vec A n₁²} {xs₂² : Vec A n₂²} →
xs₁¹ ≈ xs₁² → xs₂¹ ≈ xs₂² →
xs₁¹ ++ xs₂¹ ≈ xs₁² ++ xs₂²
[]-cong ++-cong eq₃ = eq₃
(eq₁ ∷-cong eq₂) ++-cong eq₃ = eq₁ ∷-cong (eq₂ ++-cong eq₃)
module DecidableEquality {d₁ d₂} (D : DecSetoid d₁ d₂) where
private module DS = DecSetoid D
open DS using () renaming (_≟_ to _≟′_ ; Carrier to A)
open Equality DS.setoid
open import Relation.Nullary
_≟_ : ∀ {n m} (xs : Vec A n) (ys : Vec A m) → Dec (xs ≈ ys)
_≟_ [] [] = yes []-cong
_≟_ [] (y ∷ ys) = no (λ())
_≟_ (x ∷ xs) [] = no (λ())
_≟_ (x ∷ xs) (y ∷ ys) with xs ≟ ys | x ≟′ y
... | yes xs≈ys | yes x≊y = yes (x≊y ∷-cong xs≈ys)
... | no ¬xs≈ys | _ = no helper
where
helper : ¬ (x ∷ xs ≈ y ∷ ys)
helper (_ ∷-cong xs≈ys) = ¬xs≈ys xs≈ys
... | _ | no ¬x≊y = no helper
where
helper : ¬ (x ∷ xs ≈ y ∷ ys)
helper (x≊y ∷-cong _) = ¬x≊y x≊y
module PropositionalEquality {a} {A : Set a} where
open Equality (P.setoid A)
to-≡ : ∀ {n} {xs ys : Vec A n} → xs ≈ ys → xs ≡ ys
to-≡ []-cong = P.refl
to-≡ (P.refl ∷-cong xs¹≈xs²) = P.cong (_∷_ _) $ to-≡ xs¹≈xs²
from-≡ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≈ ys
from-≡ P.refl = refl _