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)

Agda 列出与 1 的列表串联的通用自然列表的最后一个

Agda list last of a generic list of naturals concatenated with a list of 1

list

agda

vec