我写了一个 Agda 函数applyPrefix
将固定大小的向量函数应用于较长向量的初始部分,其中向量大小m
、n
和 k
可能保持隐式。以下是定义以及帮助程序函数split
:
split : ∀ {A m n} → Vec A (n + m) → (Vec A n) × (Vec A m)
split {_} {_} {zero} xs = ( [] , xs )
split {_} {_} {suc _} (x ∷ xs) with split xs
... | ( ys , zs ) = ( (x ∷ ys) , zs )
applyPrefix : ∀ {A n m k} → (Vec A n → Vec A m) → Vec A (n + k) → Vec A (m + k)
applyPrefix f xs with split xs
... | ( ys , zs ) = f ys ++ zs
我需要一个对称函数applyPostfix
它将固定大小的向量函数应用于较长向量的尾部。
applyPostfix ∀ {A n m k} → (Vec A n → Vec A m) → Vec A (k + n) → Vec A (k + m)
applyPostfix {k = k} f xs with split {_} {_} {k} xs
... | ( ys , zs ) = ys ++ (f zs)
正如applyPrefix
的定义已经显示的那样,k
-Argument 在使用applyPostfix
时不能保持隐式。例如:
change2 : {A : Set} → Vec A 2 → Vec A 2
change2 ( x ∷ y ∷ [] ) = (y ∷ x ∷ [] )
changeNpre : {A : Set}{n : ℕ} → Vec A (2 + n) → Vec A (2 + n)
changeNpre = applyPrefix change2
changeNpost : {A : Set}{n : ℕ} → Vec A (n + 2) → Vec A (n + 2)
changeNpost = applyPost change2 -- does not work; n has to be provided
有谁知道一种技术,如何实现applyPostfix
,以便在使用applyPostfix
时k
参数可以保持隐式?
我所做的是校对/编程:
lem-plus-comm : (n m : ℕ) → (n + m) ≡ (m + n)
并在定义applyPostfix
时使用该引理:
postfixApp2 : ∀ {A}{n m k : ℕ} → (Vec A n → Vec A m) → Vec A (k + n) → Vec A (k + m)
postfixApp2 {A} {n} {m} {k} f xs rewrite lem-plus-comm n k | lem-plus-comm k n | lem-plus-comm k m | lem-plus-comm m k = reverse (drop {n = n} (reverse xs)) ++ f (reverse (take {n = n} (reverse xs)))
不幸的是,这没有帮助,因为我使用 k
-Parameter 来调用引理:-(
有什么更好的想法如何避免k
明确吗?也许我应该在矢量上使用 snoc-view?
你可以做的是给postfixApp2
提供与applyPrefix
相同的类型。
问题的根源在于,只有已知自然数n
才能与p + q
统一p
。这是因为+
是通过第一个参数的归纳来定义的。
所以这个有效(我在+
上使用标准库版本的交换性):
+-comm = comm
where
open IsCommutativeSemiring isCommutativeSemiring
open IsCommutativeMonoid +-isCommutativeMonoid
postfixApp2 : {A : Set} {n m k : ℕ}
→ (Vec A n → Vec A m)
→ Vec A (n + k) → Vec A (m + k)
postfixApp2 {A} {n} {m} {k} f xs rewrite +-comm n k | +-comm m k =
applyPostfix {k = k} f xs
是的,我在这里重用原始applyPostfix
,只是通过重写两次来赋予它不同的类型。
和测试:
changeNpost : {A : Set} {n : ℕ} → Vec A (2 + n) → Vec A (2 + n)
changeNpost = postfixApp2 change2
test : changeNpost (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡ 1 ∷ 2 ∷ 4 ∷ 3 ∷ []
test = refl