为什么下面的 Agda 代码不会进行类型检查？

Question

我是 Agda 的新手，对此感到困惑。

open import Data.Vec
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Fin hiding (_+_ ; splitAt)
open import Data.Product
open import Relation.Binary.PropositionalEquality

difference : ∀ m (n : Fin m) → ∃ λ o → m ≡ toℕ n + o
difference zero ()
difference (suc m) zero = suc m , refl
difference (suc m) (suc n) with difference m n
difference (suc m) (suc n) | o , p1 = o , cong suc p1

takeFin : ∀ {A : Set} {m : ℕ} (n : Fin m) → Vec A m → Vec A (toℕ n)
takeFin {A} {m = m} n vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , _ , _ = xs

takeFin函数报错信息： m != lhs 类型 ℕ 检查类型时 {m : ℕ} (n : Fin m) (o : ℕ) (p : m ≡ to ℕ n + o) (lhs : ℕ) → lhs ≡ toℕ n + o → {A : Set} (vec : Vec A lhs) → Vec A (toℕ n) 生成的 with 函数格式正确

但以下函数可以编译

takeFin' : ∀ {A : Set} {m : ℕ} (n : Fin m) → Vec A m → Vec A m
takeFin' {A} {m = m} n a vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , ys , _ = xs ++ ys

takeFin'' : ∀ {A : Set} {m : ℕ} (n : Fin m) → A → Vec A m → Vec A (toℕ n)
takeFin'' {A} {m = m} n a vec = replicate a

谁能帮帮我？

Answer 1

正如新的 Agda 用户倾向于做的那样，您确实使事情变得比您需要的复杂得多。您打算证明的内容实际上可以通过更简单的方式完成，如下所示：

open import Data.Vec
open import Data.Fin

takeFin : ∀ {a} {A : Set a} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {n = zero} (x ∷ v) = []
takeFin {n = suc _} (x ∷ v) = x ∷ takeFin v

您应该始终尝试编写简单的归纳证明，而不是使用不必要的中间引理。

至于为什么你的版本没有类型检查（不是编译，是类型检查）原因在于你的重写调用是在 m ≡ toℕ n + o 的元素上进行的，而你的目标是类型 Vec A (toℕ n) 并且不包含任何出现的 m。您要做的是在您的上下文中转换 vec 的类型，而 rewrite 仅对目标起作用。以下是我如何让它发挥作用：

takeFin : ∀ {A : Set} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {m = m} {n} vec with difference m n
... | _ , p = proj₁ (splitAt (toℕ n) (subst (Vec _) p vec))

它可以工作，但如您所见，它远没有那么优雅（并且它还需要您定义的 difference 函数），更重要的是，它使用 subst，这通常是不鼓励的。

作为旁注，主要是为了好玩，可以使函数更简洁和优雅（但不太容易理解），如下所示：

open import Function

takeFin : ∀ {A : Set} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {n = n} = proj₁ ∘ (splitAt (toℕ n)) ∘ (subst (Vec _) (proj₂ (difference _ n)))

这个版本虽然读起来复杂得多，但显示了 Agda 在推断参数值方面的强大功能，因为只明确给出了 n。

为什么下面的 Agda 代码不会进行类型检查？

Why won't the following Agda code typecheck?

agda