Как сравнить Векторы натов в Агде

Я пытаюсь использовать Decidable Equality для сравнения двух векторов Nats в Agda. Я попытался открыть модуль Vector Equality, передав в качестве аргумента Nat DecSetoid следующим образом:

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._≟_)

Однако я получаю следующую ошибку:

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)

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


types functional-programming dependent-type agda
person jmite    schedule 14.07.2015    source источник

Ответы (2)


arrow_upward
5
arrow_downward

Проблема здесь в том, что предложение where не включает идентификаторы в область действия для выражений в with. Поэтому, когда вы используете Data.Vec.Equality.DecidableEquality.≟, вы имеете в виду не тот, который специализируется на векторах натуральных чисел, а общий, определенный в Data.Vec.Equality. Вот почему Агда ожидает DecSetoid в качестве первого аргумента и жалуется.

Возможное исправление состоит в том, чтобы сначала назвать интересующий вас модуль, а затем использовать полное имя для ссылки на его _≟_. Я позволил себе использовать более короткие имена, определив псевдонимы через 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
... | _  =  {!!}
person gallais    schedule 14.07.2015

arrow_upward
4
arrow_downward

Вы также можете определять, импортировать и открывать модули локально:

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
... | _ = {!!}

Однако в вашем случае вам не нужен with — достаточно лямбда сопоставления с образцом:

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 _≟_)
person user3237465    schedule 15.07.2015