Mostrar (head. Init) = cabeza en Agda

Question

Estoy tratando de demostrar un lema simple en Agda, que creo que es cierto.

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

he formulado de la siguiente manera:

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

que me da;

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

como respuesta.

No entiendo completamente 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 ese término.

Muchas gracias.

Answer 1

No entiendo completamente cómo leer el componente (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). I supongamos que mis preguntas son; ¿es posible, cómo y qué significa ese término ?

Esto le indica que el valor init (x ∷ xs) depende del valor de todo a la derecha de la |. Cuando demuestres algo sobre una función en Agda, tu prueba tendrá que tener la estructura de la definición original.

En este caso, debe tener en cuenta 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í es cómo escribimos 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 

he tomado la libertad de generalizar su lema a Vec A ya que el lema no depende de los contenidos del vector.

Answer 2

Ok. Tengo este haciendo trampas y espero que alguien tenga una mejor solución. Descarté toda la información adicional que obtienes del init que se define en términos de initLast y creé 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.

¿Alguna otra oferta?