I am busy formalising a theorem using a library which introduces an indexed datatype. For simplicity one can think of it to have the form data idx (n : ℕ).
Now I want to create a list of elements over this datatype with the parameter fixed, whose length depends on this parameter. I have simplified the whole problem to the example below:
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) {!!}
I want to write a function func : (m n : ℕ) → List (idx (n + m)) that returns a list num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ ... num (n + m) ∷ [] when called with func 0 (n + m) or maybe func (n + m) 0 - whatever would work - (as in exampleB).
It seems to be simpler to first compute the reverse list, which I try to achieve in rev-list and rev-list'.
However, I get the errors indicated in the code above. I have been struggling with this for hours to no avail. If anybody here could help me, it would be much appreciated :)
Given that the parameter is fixed you can simply do
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ℕ)