Affichage (tête. Init) = tête en Agda

Question

Je suis en train de prouver un lemme simple Agda, que je pense est vrai.

  

Si un vecteur a plus de deux éléments, en prenant son head suit en prenant le init est la même chose que prendre son head immédiatement.

J'ai formulé comme suit:

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

Ce qui me donne;

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

en tant que réponse.

Je ne comprends pas tout à fait lire le composant (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). Je suppose que mes questions sont; est-il possible, comment et qu'est-ce que ce terme moyen.

Merci.

Answer 1

  

Je ne comprends pas tout à fait comment   lire le composant (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)). je   suppose que mes questions sont; est-il   possible, comment et qu'est-ce que terme   dire.

Cela vous indique que la valeur init (x ∷ xs) dépend de la valeur de tout à droite de la |. Lorsque vous prouvez quelque chose dans une fonction en Agda votre preuve devra avoir la structure de la définition originale.

Dans ce cas, vous devez le cas sur le résultat de initLast parce que la définition de initLast fait cela avant de produire des résultats.

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

Voici donc comment nous écrivons le lemme.

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

Je pris la liberté de votre lemme généralisant Vec A depuis le lemme ne dépend pas du contenu du vecteur.

Answer 2

Ok. J'ai celle-ci par la tricherie et j'espère que quelqu'un a une meilleure solution. J'ai jeté toutes les informations supplémentaires que vous obtenez de init étant défini en termes de initLast et créé ma propre version naïve.

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

Maintenant, le lemme est trivial.

Les autres offres?