如何创建长度依赖于索引的索引数据类型元素列表？

问题背景 #

需要实现函数func : (m n : ℕ) → List (idx (n + m))，当调用func 0 k或func k 0时，返回形如num 1 ∷ num 2 ∷ ... ∷ num k ∷ []的列表（示例中的exampleB形式）。尝试生成逆序列表时遇到类型不匹配错误。

错误代码示例 #

open import Data.Nat using (ℕ ; _+_ ; suc ; zero) public
open import Data.List.Base using (_∷_ ; [] ; List) public

data idx (n : ℕ) : Set where
  num : ℕ → idx n

exampleA : List (idx 4) -- 随机列表
exampleA = num 12312 ∷ num 4792384 ∷ []

exampleB : List (idx 4) -- 目标格式列表
exampleB = num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ []

rev-list : (m n : ℕ) → List (idx (n + m))
rev-list zero n = []
-- 尝试填入m和suc n时出现类型错误：
-- first hole:  m !=< suc m of type ℕ
-- second hole: suc (n + ?0) !=< n + suc m of type ℕ
rev-list (suc m) n = num (suc m) ∷ rev-list {!!} {!!} 

rev-list' : (m n : ℕ) → List (idx (n + m))
rev-list' m zero = []
-- 尝试填入n时出现类型错误：
-- n + suc m !=< suc (n + m) of type ℕ
rev-list' m (suc n) =  num (suc n) ∷ rev-list' (suc m) {!!}

错误原因 #

Agda的类型系统对自然数加法的结构严格匹配，不会自动推导加法的交换律、结合律或后继性质。例如suc (n + m)和n + suc m在类型层面被视为不同的表达式，导致递归调用的类型无法与函数返回类型匹配。

解决方法 #

需要显式使用自然数加法的性质引理（如+-suc、交换律comm），通过类型转换（subst）调整递归调用的类型，或者调整递归结构让类型自然匹配。

方案1：修正逆序列表实现，利用类型转换 #

首先导入必要的等式和加法性质：

open import Data.Nat using (ℕ ; _+_ ; suc ; zero ; +-suc) public
open import Data.List.Base using (_∷_ ; [] ; List ; reverse) public
open import Relation.Binary.PropositionalEquality using (_≡_ ; subst ; sym)

修正rev-list函数，用subst转换递归调用的类型：

data idx (n : ℕ) : Set where
  num : ℕ → idx n

rev-list : (m n : ℕ) → List (idx (n + m))
rev-list zero n = []
rev-list (suc m) n = 
  num (suc m) ∷ 
  subst (λ x → List (idx x)) (sym (+-suc n m)) (rev-list m (suc n))

• +-suc n m提供引理n + suc m ≡ suc (n + m)，sym反转得到suc (n + m) ≡ n + suc m
• subst将rev-list m (suc n)的类型List (idx (suc n + m))（即List (idx (suc (n + m)))）转换为List (idx (n + suc m))，与rev-list (suc m) n的返回类型匹配

基于逆序列表实现func：

func : (m n : ℕ) → List (idx (n + m))
func m n = reverse (rev-list (n + m) 0)

调用func 0 4会返回num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ []，符合需求。

方案2：直接生成正向列表，利用加法交换律 #

先实现生成1到k的正向列表，再通过加法交换律转换类型适配func的签名：

open import Data.Nat using (ℕ ; _+_ ; suc ; zero ; comm) public
open import Data.List.Base using (_∷_ ; [] ; List ; map) public
open import Relation.Binary.PropositionalEquality using (_≡_ ; subst)

data idx (n : ℕ) : Set where
  num : ℕ → idx n

-- 生成从1到k的列表，类型为List (idx k)
build-upto : ℕ → List (idx ℕ)
build-upto zero = []
build-upto (suc k) = num 1 ∷ map (λ (num x) → num (suc x)) (build-upto k)

func : (m n : ℕ) → List (idx (n + m))
func m n = subst (λ x → List (idx x)) (comm n m) (build-upto (m + n))

• comm n m提供加法交换律引理n + m ≡ m + n
• subst将build-upto (m + n)的类型List (idx (m + n))转换为List (idx (n + m))，匹配func的返回类型

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