如何在Agda中实现符合指定类型的两个Fin函数的求和？

要实现这个类型的sum函数，核心是利用Fin类型在自然数加法下的不交并特性：Fin (a + c)的元素必然属于两类——要么是从Fin a嵌入的元素，要么是从Fin c嵌入的元素。我们只需要对这两类元素分别应用对应的函数，再将结果嵌入到目标类型即可。

首先补充必要的导入（包含Fin的嵌入和拆分函数）：

open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Fin using (inject₁; inject₂; split)

然后实现sum函数：

sum : (a b c d : ℕ) → (x : Fin a → Fin b) → (y : Fin c → Fin d) → (Fin (a + c) → Fin (b + d))
sum a b c d x y z with split z
... | inj₁ i = inject₁ (x i)
... | inj₂ j = inject₂ (y j)

代码说明 #

• split z：将Fin (a + c)类型的元素z拆分为两种情况：inj₁ i（i是Fin a的元素）或inj₂ j（j是Fin c的元素）
• 对于inj₁ i：用函数x处理i得到Fin b的结果，再通过inject₁嵌入到Fin (b + d)中
• 对于inj₂ j：用函数y处理j得到Fin d的结果，再通过inject₂嵌入到Fin (b + d)中

内容的提问来源于stack exchange，提问作者Ruben