Agda列出了与1的列表相连的自然人的一般列表的最后一个

Question

我有一个函数：

natListLast : List ℕ → ℕ
natListLast []            = 0
natListLast nats@(x ∷ xs) = v.last (v.fromList nats)

当我做时

_ : natListLast (2 l.∷ l.[] l.++ 1 l.∷ l.[]) ≡ 1
_ = refl

我没有任何错误。

但当我试图将其推广到任意的List nat时，比如：

natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
natListConcatLast [] = refl
natListConcatLast nats@(x ∷ xs) = ?

我不知道用什么来代替?。

我试着从begin:开始

natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
natListConcatLast [] = refl
natListConcatLast nats@(x ∷ xs) =
begin
natListLast (nats l.++ 1 l.∷ l.[])
≡⟨⟩
v.last (v.fromList ((x l.∷ xs) l.++ 1 l.∷ l.[]))
≡⟨⟩
?
≡⟨⟩
1
∎

但我得到了这个错误：

1 !=
(last (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[]))
| initLast (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[])))
of type ℕ
when checking that the expression 1 ∎ has type
last (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[])) ≡ 1

我不知道如何解释这个错误。我不知道如何处理| initLast。

谢谢！

Answer 1

我建议以下解决方案：

open import Data.List
open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
natListLast : List ℕ → ℕ
natListLast [] = 0
natListLast (x ∷ []) = x
natListLast (_ ∷ y ∷ l) = natListLast (y ∷ l)
natListConcatLast : ∀ l → natListLast (l ++ [ 1 ]) ≡ 1
natListConcatLast [] = refl
natListConcatLast (_ ∷ []) = refl
natListConcatLast (_ ∷ _ ∷ l) = natListConcatLast (_ ∷ l)