theorem-proving - 显示(head。unit)= Agda 的head

Question

我正在尝试证明在Agda中的简单引理，我认为这是对的。

If a vector has more than two elements, taking its head following taking the init is the same as taking its head immediately.

我将其表述如下:

lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l)))
                    -> head (init xs) ≡ head xs
lem-headInit (x ∷ xs) = ?

这给了我；

.l : ℕ
x  : ℕ
xs : Vec ℕ (suc .l)
------------------------------
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x

作为回应。

我不完全了解如何阅读 (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))组件。我想我的问题是；该术语是否可能，如何以及是什么意思。

非常感谢。

Answer 1

I do not entirely understand how to read the (init (x ∷ xs) | (initLast (x
∷ xs) | initLast xs)) component. I suppose my questions are; is it possible, how and what does that term mean.

这告诉您 init (x ∷ xs)的值取决于 |右侧的所有值。当您在Agda的函数中证明某些内容时，您的证明将必须具有原始定义的结构。

在这种情况下，您必须考虑 initLast的结果，因为 initLast的定义会在产生任何结果之前执行此操作。

init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
init xs         with initLast xs
                --  ⇧  The first thing this definition does is case on this value
init .(ys ∷ʳ y) | (ys , y , refl) = ys

这就是我们写引理的方式。

module inithead where

open import Data.Nat
open import Data.Product
open import Data.Vec
open import Relation.Binary.PropositionalEquality

lem-headInit : {A : Set} {n : ℕ} (xs : Vec A (2 + n))
             → head (init xs) ≡ head xs

lem-headInit (x ∷ xs) with initLast xs
lem-headInit (x ∷ .(ys ∷ʳ y)) | ys , y , refl = refl

我自由地将您的引理归纳为 Vec A，因为引理不依赖于向量的内容。