Mostrando (cabeza. Init) = cabeza en Agda

Question

Estoy intentando probar un lema simple en Agda, que creo que es cierto.

  

Si un vector tiene más de dos elementos, teniendo su head siguiendo tomar el init es lo mismo que tomar su head inmediatamente.

I han formulado como sigue:

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

Lo que me da;

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

como una respuesta.

No entiendo del todo cómo leer el componente (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). Supongo que mis preguntas son; es posible, cómo y qué significa eso plazo.

Muchas gracias.

Answer 1

  

No entiendo del todo cómo   leer el componente (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). yo   supongamos que mis preguntas son; Lo es   posible, cómo y lo que ese término   significar.

Esto le indica que el valor init (x ∷ xs) depende del valor de todo a la derecha de la |. Al probar algo acerca de una función en Agda su prueba tendrá que tener la estructura de la definición original.

En este caso hay que caso sobre el resultado de initLast porque la definición de initLast hace esto antes de producir ningún resultado.

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

Así que aquí es cómo se escribe el 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

Me tomé la libertad de generalizar su lema a Vec A ya que el lema no depende de los contenidos del vector.

Answer 2

Ok. Tengo éste por el engaño y estoy esperando que alguien tiene una mejor solución. Tiré toda la información adicional que se obtiene de init se define en términos de initLast y creado mi propia versión ingenua.

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

Ahora el lema es trivial.

Las demás ofertas?