我试图证明 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))
成分。我想我的问题是;是否可能,如何以及该术语的含义是什么。
非常感谢。
我不完全明白如何
阅读(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
因为引理不依赖于向量的内容。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)