Как создать список элементов индексированного типа данных, длина которого зависит от индекса
Я занят формализацией теоремы с помощью библиотеки, которая представляет индексированный тип данных. Для простоты можно представить, что это имеет форму data idx (n : ℕ).
Теперь я хочу создать список элементов этого типа данных с фиксированным параметром, длина которого зависит от этого параметра. Я упростил всю проблему до примера ниже:
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) -- some random list
exampleA = num 12312 ∷ num 4792384 ∷ []
exampleB : List (idx 4) -- list of the form that I want
exampleB = num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ []
rev-list : (m n : ℕ) → List (idx (n + m))
rev-list zero n = []
-- I want to put "m" in the first hole and "suc n" in the second hole,
-- but I get the following errors:
-- 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 = []
-- I want to put "n" in the hole, but I get the following error:
-- n + suc m !=< suc (n + m) of type ℕ
rev-list' m (suc n) = num (suc n) ∷ rev-list' (suc m) {!!}
Я хочу написать функцию func : (m n : ℕ) → List (idx (n + m)), которая возвращает список num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ ... num (n + m) ∷ [] при вызове с помощью func 0 (n + m) или, может быть, func (n + m) 0 - что угодно - (как в exampleB).
Кажется, проще сначала вычислить обратный список, чего я пытаюсь достичь в rev-list и rev-list'.
Однако я получаю ошибки, указанные в приведенном выше коде. Я боролся с этим часами, но безрезультатно. Если бы кто-нибудь здесь мог мне помочь, я был бы очень признателен :)
Ответы 2
Учитывая, что параметр фиксирован, вы можете просто сделать
open import Data.List.Base using (tabulate)
open import Data.Fin.Base using (toℕ)
open import Function using (_∘_)
func : (m n : ℕ) → List (idx (n + m))
func m n = tabulate {n = n + m} (num ∘ suc ∘ toℕ)
Похоже, вы можете обобщить свою функцию до произвольного индекса k, чтобы рекурсия больше не была проблемой:
rev-list2 : (m n k : ℕ) → List (idx k)
rev-list2 m zero k = []
rev-list2 m (suc n) k = num (suc m) ∷ rev-list2 (suc m) n k
Затем вы можете определить свой особый случай:
rev-list : (m n : ℕ) → List (idx (n + m))
rev-list m n = rev-list2 m n (n + m)
Спасибо за ваш ответ. Это решает описанную проблему. Однако, к сожалению, это не решает мою исходную проблему, в которой (то, что я не упомянул) num также есть параметр, который зависит от фиксированного k. Мне нравится ваш подход, потому что он прост и понятен, но я приму ответ @effectfully, поскольку он более общий и также решает мою исходную проблему. (Возможно, мне следовало выбрать лучший пример для иллюстрации проблемы).
@user11718766 user11718766 Конечно! Я действительно подозревал, что ваша реальная задача немного другая и не может быть решена таким образом.
Большое спасибо за ваш ответ. Это полностью решает мою проблему. Мне потребовалось некоторое время, чтобы адаптировать его к моей первоначальной, несколько более сложной задаче, но
tabulateв конце концов сделал свое дело :)