list - 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)