Display (head. Init) = head in Agda

Question

I am trying to prove a simple lemma in Agda, which, in my opinion, is true.

If a vector has more than two elements, taking its head after accepting init is the same as its head .

I formulated it as follows:

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

What gives me;

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

as an answer.

I don’t quite understand how to read the component (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) . I guess my questions; is it possible, how and what does this term mean.

Thank you very much.

Answer 1

I don’t quite understand how to read the component (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) . I suppose my questions; it is possible how and what this term does mean.

This suggests that the value of init (x ∷ xs) depends on the value of everything that is to the right of | . When you prove something in a function in Agda, your proof will have to have the structure of the original definition.

In this case, you must specify the result of initLast , because the definition of initLast does this before any results are obtained.

 init : ∀ {an} {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 

So this is how we write the 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 

I made a commitment to generalize your lemma to Vec A , since the lemma is independent of the contents of the vector.

Answer 2

Ok I have this while cheating, and I hope someone has a better solution. I threw away all the additional information you received from init , defined from the point of view of initLast , and created my own naive version.

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

Now the lemma is trivial.

Any other suggestions?