How to compare Vectors of Nats in Agda

2
votes

I'm trying to use Decidable Equality to compare two Vectors of Nats in Agda. I've tried opening the Vector Equality module, passing the Nat DecSetoid as an argument, as follows:

open import Data.Nat
open import Data.Vec

open import Relation.Binary.PropositionalEquality
import Data.Vec.Equality

myFunction : {n : ℕ} -> Vec ℕ n -> Vec ℕ n -> ℕ 
myFunction v1 v2 
  with v1 Data.Vec.Equality.DecidableEquality.≟ v2
... | _  =  {!!}
  where 
    open Data.Vec.Equality.DecidableEquality  (Relation.Binary.PropositionalEquality.decSetoid Data.Nat._≟_)

However, I get the following error:

Vec ℕ .n !=< .Relation.Binary.DecSetoid (_d₁_6 v1 v2) (_d₂_7 v1 v2)
of type Set
when checking that the expression v1 has type
.Relation.Binary.DecSetoid (_d₁_6 v1 v2) (_d₂_7 v1 v2)

I'm not sure what I'm doing wrong. Am I using the module system wrong, or do I need to use ≟ differently?

2
typesfunctional-programmingagdadependent-type

2 Answers

5
votes

The problem here is that the where clause does not bring the identifiers in scope for the expressions in the with. So when you use Data.Vec.Equality.DecidableEquality.≟, you're not refering to the one specialised to vectors of natural numbers but to the general one define in Data.Vec.Equality. That's why Agda expects a DecSetoid as the first argument and complains.

A possible fix is to name the module you are interested in first and then used a qualified name to refer to its _≟_. I've taken the liberty of using shorter names by defining aliases via as:

open import Relation.Binary.PropositionalEquality as PropEq
import Data.Vec.Equality as VecEq

module VecNatEq = VecEq.DecidableEquality (PropEq.decSetoid Data.Nat._≟_)

myFunction : {n : ℕ} -> Vec ℕ n -> Vec ℕ n -> ℕ 
myFunction v1 v2 
  with v1 VecNatEq.≟ v2
... | _  =  {!!}
4
votes

You can also define, import and open modules locally:

open import Data.Nat
open import Data.Vec

open import Relation.Binary.PropositionalEquality as P
import Data.Vec.Equality as VE

myFunction : {n : ℕ} -> Vec ℕ n -> Vec ℕ n -> ℕ 
myFunction v1 v2 with let module DVE = VE.DecidableEquality (decSetoid _≟_) in v1 DVE.≟ v2
... | _ = {!!}

However you don't really need with in your case — pattern matching lambda is enough:

open import Function
open import Relation.Nullary

myFunction : {n : ℕ} -> Vec ℕ n -> Vec ℕ n -> ℕ 
myFunction v1 v2 = case v1 DVE.≟ v2 of λ
    { (no  p) -> {!!}
    ; (yes p) -> {!!}
    }
  where module DVE = VE.DecidableEquality (decSetoid _≟_)