Zeige (Kopf. Init) = Kopf in Agda

Question

Ich versuche, ein einfaches Lemma in Agda zu beweisen, was ich denke, wahr ist.

  

Wenn ein Vektor mehr als zwei Elemente hat, wobei seine head die init folgende Einnahme ist die gleiche wie unter seinem head sofort.

Ich habe es wie folgt formuliert:

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

Was mir gibt;

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

als Antwort zurück.

Ich verstehe nicht ganz, wie die (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) Komponente zu lesen. Ich nehme an, meine Fragen sind; ist es möglich, wie und was bedeutet dieser Begriff bedeuten.

Vielen Dank.

Answer 1

  

Ich verstehe nicht ganz, wie man   Lesen Sie die (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) Komponente. ich   nehme meine Fragen sind; ist es   möglich, wie und was bedeutet dieser Begriff   bedeuten.

Hier erfahren Sie, dass der Wert init (x ∷ xs) rechts von der | auf den Wert der alles abhängt. Wenn Sie etwas über in einer Funktion in Agda Ihr Beweis beweisen die Struktur der ursprünglichen Definition haben müssen.

In diesem Fall müssen Sie zu Fall auf dem Ergebnis der initLast, weil die Definition von initLast dies vor dem ergebnislos.

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

Hier ist also, wie wir das Lemma schreiben.

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

habe ich die Freiheit, Ihre Lemma zu Vec A verallgemeinern, da das Lemma nicht auf den Inhalt des Vektors abhängt.

Answer 2

Ok. Ich habe diese bekommt man durch Betrug und ich hoffe, dass jemand eine bessere Lösung hat. Ich warf alle zusätzlichen Informationen, die Sie von init erhalten in Bezug auf initLast definiert ist und meine eigene naive Version erstellt.

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

Nun das Lemma ist trivial.

Alle anderen Angebote?