Показ (голова. Init) = голова в agda

Question

Я пытаюсь доказать простое лемму в АГДА, которую я думаю, правда.

Если вектор имеет более двух элементов, принимая его 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

В порядке. У меня есть этот, обманывая, и я надеюсь, что у кого-то лучше. Я выбросил всю дополнительную информацию, которую вы получаете от init быть определенным с точки зрения initLast и создал свою собственную наивную версию.

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

Теперь лемма тривиальна.

Любые другие предложения?