9

私は Agda で単純な補題を証明しようとしていますが、これは正しいと思います。

ベクトルに 2 つ以上の要素がある場合、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))コンポーネントの読み方がよくわかりません。私の質問は次のとおりだと思います。それは可能ですか、その用語はどのように、そして何を意味しますか。

どうもありがとう。

4

2 に答える 2

9

(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補題はベクトルの内容に依存しないため、補題を自由に一般化しました。

于 2010-11-07T22:26:29.673 に答える
3

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

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

これで補題は自明です。

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

于 2010-08-11T16:20:42.353 に答える