Mostrando (testa. Init) = testa a Agda

Question

Sto cercando di dimostrare un semplice lemma in Agda, che credo sia vero.

  

Se un vettore ha più di due elementi, prendendo il suo head seguendo prendendo il init è lo stesso che immediatamente la sua head.

ho formulato come segue:

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

Il che mi dà;

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

come risposta.

Io non del tutto a capire come leggere la componente (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). Suppongo che le mie domande sono; è possibile, come e che cosa significa quel termine medio.

Molte grazie.

Answer 1

  

Io non del tutto a capire come   Leggere la componente (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). io   supponiamo che le mie domande sono; è   possibile, come e che cosa fa quel termine   significare.

Questo indica che il valore init (x ∷ xs) dipende dal valore del tutto alla destra del |. Quando si prova qualcosa a proposito di una funzione in Agda la prova dovrà avere la struttura della definizione originale.

In questo caso bisogna caso sul risultato di initLast perché la definizione di initLast fa questo prima di produrre alcun risultato.

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

Quindi, ecco come si scrive il lemma.

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

Mi sono permesso di generalizzare il tuo lemma per lemma Vec A dal momento che il non dipende dal contenuto del vettore.

Answer 2

Ok. Ho questo uno con l'inganno e spero che qualcuno ha una soluzione migliore. Ho buttato via tutte le informazioni supplementari che si ottiene da init essere definita in termini di initLast e ha creato la mia versione ingenua.

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

Ora il lemma è banale.

Tutte le altre offerte?