Agda: std-lib: List: all but last element with snoc

I defined allButLast this way:

allButLast : ∀ {a} {A : Set a} → List A → List A
allButLast l.[] = l.[]
allButLast list = l.reverse (tail' (l.reverse list))

and would like to prove the following statement:

allButLast-∷ʳ :
  ∀ {a} {A : Set a} →
    (list : List A) →
      (y : A) →
        allButLast (list ∷ʳ y) ≡ list
allButLast-∷ʳ []       y = refl
allButLast-∷ʳ (x ∷ []) y = refl
allButLast-∷ʳ (x ∷ xs) y =
  begin
    allButLast ((x ∷ xs) ++ [ y ])
  ≡⟨⟩
    reverse (tail' (reverse ((x ∷ xs) ∷ʳ y)))
  ≡⟨ ? ⟩
    reverse (tail' (y ∷ reverse (x ∷ xs)))
  ≡⟨⟩
    reverse (reverse (x ∷ xs))
  ≡⟨ reverse-involutive (x ∷ xs) ⟩
    (x ∷ xs)
  ∎

where I need to find what to replace ? with.

I defined:

reverse-∷ʳ :
  ∀ {a} {A : Set a} →
    (list : List A) →
      (n : A) →
        reverse (list ∷ʳ n) ≡ n ∷ reverse list

which I was able to prove.

I wanted to use it as reverse-∷ʳ (x ∷ xs) y to replace ? however, I get the following error:

x ∷ [] != [] of type List A
when checking that the expression reverse-∷ʳ (x ∷ xs) y has type
reverse (tail' (reverse ((x ∷ xs) ∷ʳ y))) ≡
reverse (tail' (y ∷ reverse (x ∷ xs)))

I'm not sure how to interpret it. Is this because I'm not covering the case x ∷ [] when I apply reverse-∷ʳ (x ∷ xs) y?

Solution

I suggest the following solution:

allButLast : ∀ {a} {A : Set a} → List A → List A
allButLast [] = []
allButLast (_ ∷ []) = []
allButLast (x ∷ x₁ ∷ l) = x ∷ (allButLast (x₁ ∷ l))

allButLast-∷ʳ : ∀ {a} {A : Set a} {l : List A} {x} → allButLast (l ∷ʳ x) ≡ l
allButLast-∷ʳ {l = []} = refl
allButLast-∷ʳ {l = _ ∷ []} = refl
allButLast-∷ʳ {l = x ∷ x₁ ∷ l} = cong (x ∷_) (allButLast-∷ʳ {l = x₁ ∷ l})

For a while now, you've been asking quite a lot of questions in #Agda and this is completely fine. However, and don't take this the wrong way, you should definitely try and understand what you're doing instead of asking similar questions again and again. It seems to me that you do not quite understand how to write definitions nor proofs in Agda, simply because you don't take enough time to try and understand how all of this work. For instance, your precedent question shows that you don't quite understand yet the difference between functions and constructors, as well as pattern matching. In addition, you always try and use chained equalities to prove your goals even though in most cases a simple case split on the data you are working on (mostly lists and vects) is sufficient to solve your issue. You tend to overcomplicate matters, and believe me, this is not what you want to do when developing in Agda or other proof assistants, because proofs tend to quickly become very complicated by themselves. I can see that you're eager to learn and to improve your Agda skills, so here are a few suggestions, which will be more useful, in the long run, than defining and proving random notions and properties in an incorrect manner :

take a step back from your definitions and proofs
take some time to figure out by head what the proof might be, if it's simple enough to be understood.
try to understand Agda's basic mechanisms, like case-splitting, instead of more advanced ones, like equality reasoning.
make sure you cannot prove your lemmas by a simple recursion over its input instead of more complex / time consuming ways.
follow some tutorials which you can find online, most of them are regrouped in the following wiki page https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html
try and understand (and possibly reproduce by yourself) the proofs that were given as answers to the questions you've asked here, because a lot of your new questions can actually be answered / solved in a similar manner.
when defining quantities, try and define them as simply as possible, for instance look at my allButLast definition as opposed to yours which uses other complex function instead of just being defined recursively over its input.
make sure your definition actually do what you intend, either by writing some simple test cases, and evaluating them using CTRL-C CTRL-N or by proving some very simple properties over them, with examples for instance. Your previous definition of allButLast, which can be found in your previous question, was actually the identity function over lists, because you always give back exactly the input, which can easily be seen with some tests and a little step back.

All in all, take your time and try to actually understand what you're doing, because there is no way you'll be able to develop anything significant in Agda if you don't. I hope these suggestions will help you, and that you will not take them the wrong way. There are probably many more, but that's a brief overview of those I could think of directly.