Anzeigen (Kopf. Init) = Kopf in Agda

Question

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

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

Ich habe es wie folgt formuliert:

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

Was mich gibt;

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

als eine Antwort.

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

Vielen Dank.

Answer 1

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

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

In diesem Fall müssen Sie auf das Ergebnis von initLast Fall, weil die Definition von initLast tut dies vor der Herstellung von Ergebnissen.

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 

Also hier ist, 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 

nahm ich mir die Freiheit Ihres Lemma zu Vec A verallgemeinern, da das Lemma auf den Inhalt des Vektors hängt nicht.

Answer 2

Ok. Ich habe das durch Betrug und ich hoffe, dass jemand eine bessere Lösung hat. Ich habe alle zusätzlichen Informationen weggeworfen, die du von init bekommst, was in 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)) 

Jetzt ist das Lemma trivial.

Andere Angebote?