Affichage (tête. Init) = tête en Agda
-
27-09-2019 - |
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 leinit
est la même chose que prendre sonhead
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.
La solution
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.
Autres conseils
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?