shows（head。init）= agdaの頭

Question

私はAGDAの単純な補題を証明しようとしていますが、それは真実だと思います。

ベクトルに3つ以上の要素がある場合、 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 補題はベクトルの内容に依存していないためです。

Answer 2

Ok。私は不正行為によってこれを手に入れました、そして私は誰かがより良い解決策を持っていることを望んでいます。私はあなたが得るすべての余分な情報を捨てました init の観点から定義される initLast そして、私自身の素朴なバージョンを作成しました。

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

今、補題は些細なものです。

他にオファーはありますか？