显示 (head . unit ) = Agda 中的头部

Posted 2023-05-08

【中文标题】显示 (head . unit ) = Agda 中的头部

【英文标题】：Showing (head . init ) = head in Agda

【发布时间】：2011-03-27 22:24:11

【问题描述】：

我试图在 Agda 中证明一个简单的引理，我认为这是正确的。

如果一个向量有两个以上的元素，则在获取init 之后获取其head 与立即获取其head 相同。

我将其表述如下：

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)) 组件。我想我的问题是；有没有可能，这个词的含义是什么？

非常感谢。

【参考方案1】：

我不完全明白如何 阅读(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) 组件。一世 假设我的问题是；是吗 可能，该术语如何以及是什么 意思。

这告诉您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，因为引理不依赖于向量的内容。

【参考方案2】：

好的。我通过作弊得到了这个，我希望有人有更好的解决方案。我抛弃了你从init 获得的所有额外信息，这些信息是根据initLast 定义的，并创建了我自己的幼稚版本。

initLazy : ∀A l → Vec A (suc l) → Vec A l
initLazy (x ∷ []) = []
initLazy (x ∷ (y ∷ ys)) = x ∷ (initLazy (y ∷ ys))

现在引理是微不足道的。

还有其他优惠吗？