rotateVecに関数を実装しようとしています。この関数は、すべての要素の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 ?
問題は、あるsplitAt2つの入力を必要とし、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。
これが私が思いついたものです。
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
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加