如何使用 `splitAt` 在 Vec 上实现 `rotate` 函数？

Question

问题

我正在尝试在 Vec 上实现一个 rotate 函数，它将每个元素 n 位置向左移动，循环。我可以使用 splitAt 来实现该功能。这是一个草图：

open import Data.Nat
open import Data.Nat.DivMod
open import Data.Fin
open import Data.Vec
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality

rotateLeft : {A : Set} -> {w : ℕ} -> {w≢0 : False (w ≟ 0)} -> ℕ -> Vec A w -> Vec A w
rotateLeft {A} {w} n vec =
  let parts = splitAt (toℕ (n mod w)) {n = ?} vec
  in  ?

问题是 splitAt 需要两个输入，m 和 n，因此向量的大小为 m + n。由于这里向量的大小是w，我需要找到一个k使得k + toℕ (n mod w) = w。我找不到任何方便的标准功能。最好的方法是什么？

一些可能性？

如果 k = n mod w 给我一个 k < w 的证明，那我可能会有所帮助，这样我就可以尝试实现一个函数 diff : ∀ {k w} -> k < w -> ∃ (λ a : Nat) -> a + k = w。另一种可能性是只接收 a 和 b 作为输入，而不是要移位的位和向量的大小，但我不确定这是最好的接口。

更新

我已经实施了以下内容：

add-diff : (a : ℕ) -> (b : Fin (suc a)) -> toℕ b + (a ℕ-ℕ b) ≡ a
add-diff zero    zero    = refl
add-diff zero    (suc ())
add-diff (suc a) zero    = refl
add-diff (suc a) (suc b) = cong suc (aaa a b)

现在我只需要证明∀ {n m} -> n mod m < m。

Answer 1

这是我的想法。

open import Data.Vec
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Fin hiding (_+_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties using (+-comm)

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

rotate-help : ∀ {A : Set} {m} (n : Fin m) → Vec A m → Vec A m
rotate-help {A} {m = m} n vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , ys , _ = subst (Vec A) (+-comm o (toℕ n)) (ys ++ xs)

rotate : ∀ {A : Set} {m} (n : ℕ) → Vec A m → Vec A m
rotate {m = zero} n v = v
rotate {m = suc m} n v = rotate-help (n mod suc m) v

Answer 2

在 IRC 上与 adamse 交谈后，我想到了这个：

open import Data.Fin hiding (_+_)
open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

diff : {a : ℕ} → {b : Fin a} → ∃ λ c → toℕ b + c ≡ a
diff {zero}  {()}
diff {suc a} {zero}  = suc a , refl
diff {suc a} {suc b} with diff {a} {b}
... | c , prf = c , cong suc prf

rotateLeft : {A : Set} → {w : ℕ} → {w≢0 : False (w ≟ 0)} → ℕ → Vec A w → Vec A w
rotateLeft {A} {w} {w≢0} n v =
  let m  = _mod_ n w {w≢0}
      d  = diff {w} {m}
      d₁ = proj₁ d
      d₂ = proj₂ d
      d₃ = subst (λ x → x ≡ w) (+-comm (toℕ (n mod w)) d₁) d₂
      v₁ = subst (λ x → Vec A x) (sym d₂) v
      sp = splitAt {A = A} (toℕ m) {n = d₁} v₁
      xs = proj₁ (proj₂ sp)
      ys = proj₁ sp
  in  subst (λ x → Vec A x) d₃ (xs ++ ys)

虽然没有他的实现那么优雅（部分原因是我仍在学习 Agda 的语法，所以我选择只使用函数），但确实有效。现在我应该 return 一个更精致的类型，我相信。（怎么感谢他都不为过！）

Answer 3

你的最后一个问题只是为了证明 k < w，因为 k = toℕ (n mod w)，你可以使用 Data.Fin.Properties 中的 bounded:

bounded : ∀ {n} (i : Fin n) → toℕ i ℕ< n

如何使用 `splitAt` 在 Vec 上实现 `rotate` 函数？

How can I implement a `rotate` function on Vec by using `splitAt`?

agda

问题

一些可能性？

更新