Mostrando (cabeça. Init) = cabeça em AGDA

Question

Estou tentando provar um lema simples em AGDA, o que eu acho verdadeiro.

Se um vetor tem mais de dois elementos, levando seu head Depois de tomar o init é o mesmo que levar o seu head imediatamente.

Eu o formulei da seguinte maneira:

lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l)))
                    -> head (init xs) ≡ head xs
lem-headInit (x ∷ xs) = ?

O que me dá;

.l : ℕ
x  : ℕ
xs : Vec ℕ (suc .l)
------------------------------
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x

como uma resposta.

Eu não entendo totalmente como ler o (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) componente. Suponho que minhas perguntas sejam; É possível, como e o que esse termo significa.

Muito Obrigado.

Answer 1

Eu não entendo totalmente como ler o (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) componente. Suponho que minhas perguntas sejam; É possível, como e o que esse termo significa.

Isso diz que o valor init (x ∷ xs) depende do valor de tudo à direita do |. Quando você prova algo em uma função na AGDA, sua prova terá que ter a estrutura da definição original.

Nesse caso, você deve se casar com o resultado de initLast Porque a definição de initLast Faz isso antes de produzir quaisquer resultados.

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

Então, aqui está como escrevemos o lema.

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

Eu tomei a liberdade de generalizar seu lema para Vec A Como o lema não depende do conteúdo do vetor.

Answer 2

OK. Eu tenho esse trapaceando e espero que alguém tenha uma solução melhor. Eu joguei fora todas as informações extras que você obtém de init sendo definido em termos de initLast e criou minha própria versão ingênua.

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

Agora o lema é trivial.

Alguma outra oferta?