在构造基本 Agda 函数时克服定义相等问题-解网

问：

我正在尝试在 agda 中编写一个反向向量函数，但遇到了以下绊脚石

Goal: Vec Nat (suc n)
Have: Vec Nat (n +N 1)

如果我理解正确的话，这些值并不是绝对相等的。这是反向函数。

vReverse : {X : Set} {n : Nat} → Vec X n → Vec X n
vReverse [] = []
vReverse (x ,- x₁) = {!(vReverse x₁) +V (x ,- [])!}

如果可能的话，我怎样才能在不重构代码的情况下克服这个问题。如果重构是必要的，那么通常如何先验地避免这些陷阱呢？下面是代码的其余部分。

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}

_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)      -- there are other choices

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_   -- the "cons" operator associates to the right

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V xs = xs
(x ,- xs) +V [] = x ,- xs +V []
(x ,- xs) +V x₁ ,- ys = x ,- xs +V x₁ ,- ys

列出平等 AGDA

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}

_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)      -- there are other choices

infixl 5 _+N_

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)

infixr 4 _,-_   -- the "cons" operator associates to the right

但是，您的串联函数不正确，并且没有终止，因此这是更正后的版本。

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V vs = vs
(x ,- xs) +V vs = x ,- (xs +V vs)

我们不需要在这个函数中做任何替换的原因是，在定义上等于。suc n + msuc (n + m)

既然你已经定义了自己的自然和你自己的添加，我假设你想自己重新定义一切。根据这个假设，你需要定义命题相等，具体如下：

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

infix 1 _≡_

从这个定义中，我们可以定义本答案的序言中提到的替换，以及您的问题的评论中提到的替换：

subst : ∀ {a b} {A : Set a} {x y : A} (P : A → Set b) → x ≡ y → P x → P y
subst _ refl p = p

在反向函数中，问题在于定义上不等于。这就是为什么我们需要一个属性来建立这个事实，然后我们可以将其提供给我们的替换机制。这个证明需要我们定义的命题相等的一致性，如下所示：n + 1suc n

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

n+1≡sn : ∀ {n} → n +N 1 ≡ suc n
n+1≡sn {zero} = refl
n+1≡sn {suc _} = cong suc n+1≡sn

现在，我们已经具备了编写函数所需的所有元素：vReverse

vReverse : ∀ {X n} → Vec X n → Vec X n
vReverse [] = []
vReverse (x ,- x₁) = subst (Vec _) n+1≡sn ((vReverse x₁) +V (x ,- []))

更进一步，您可以使用相同的过程来构建通常的反向函数，该函数效率更高（线性复杂度）。我冒昧地为您执行此操作，因为它显示了更多使用 .subst

n+sm≡sn+m : ∀ {n m} → n +N suc m ≡ suc (n +N m)
n+sm≡sn+m {zero} = refl
n+sm≡sn+m {suc _} = cong suc n+sm≡sn+m

reverse-better-aux : ∀ {X n m} → Vec X n → Vec X m → Vec X (n +N m)
reverse-better-aux [] v₂ = v₂
reverse-better-aux (x ,- v₁) v₂ = subst (Vec _) n+sm≡sn+m (reverse-better-aux v₁ (x ,- v₂))

n+0≡n : ∀ {n} → n +N 0 ≡ n
n+0≡n {zero} = refl
n+0≡n {suc _} = cong suc n+0≡n

reverse-better : ∀ {X n} → Vec X n → Vec X n
reverse-better v = subst (Vec _) n+0≡n (reverse-better-aux v [])

上一个：任意排序对象列表的相等性 kotlin [已关闭]

下一个：R：是向量列表中的向量 [duplicate]

在构造基本 Agda 函数时克服定义相等问题

Overcoming definitional equality issues when constructing basic Agda functions

评论