显示(head.init)=在Agda开头

Question

我试图在Agda中证明一个简单的引理,我认为这是真的.

如果一个向量有两个以上的元素,那么采取head以下方法就init可以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))组件.我想我的问题是; 是否有可能,该术语的含义和含义是什么.

非常感谢.

Answer 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因为引理不依赖于向量的内容.