Fail to rewrite list with app_removelast_last

Question

I have an environment which looks like this:

P: list nat -> Prop
Hnil: P []
...
xs, xp: list nat
Hex: xp = a :: xs
Hnilcons: xp <> []
===================
P xp

I'd like to rewrite the goal to

P ((removelast xp)++[last xp 0])

As I have in the context a proof that xp in not nil, I try to use app_removelast_last:

Lemma app_removelast_last :
    forall l d, l <> [] -> l = removelast l ++ [last l d].

But when I try

rewrite (app_removelast_last xp 0 Hnilcons).

I get an obscure error message :

The term "Hnilcons" has type
 "not (@eq (list nat) xp (@nil nat))"
while it is expected to have type
 "not
    (@eq (list (list nat)) ?l
       (@nil (list nat)))"
(cannot unify "list (list nat)" and
"list nat").

Obviously, I don't understand how to use the proof that the list is not [].

Can someone help me clarify how to do this rewrite ?

Thank you !!

Answer 1

The arguments you provided aren't the ones app_removelast_last expects. You can find this with About:

About app_removelast_last.
(*
app_removelast_last :
forall [A : Type] [l : list A] (d : A),
l <> [] -> l = removelast l ++ [last l d]

app_removelast_last is not universe polymorphic
Arguments app_removelast_last [A]%type_scope [l]%list_scope d _
*)

Arguments that appear inside square brackets (or curly braces, although here there are none) are implicit. This means that Coq can infer them from the explicit arguments. So even though app_removelast_last needs four arguments to reach the equality (namely, A, l, d, and a proof of l <> []), it only expects two of them (d and a proof of l <> []), because A and l can be inferred from those. Or in other words, once you provide d and a proof of l <> [], there is only one possible choice for A and l.

Note that d is supposed to be a default value fed to last in case the list is empty. Here we know that the list is non-empty, so it is completely irrelevant which default value we pick, but we still must pick one. When you write app_removelast_last xp Hnilcons, you're saying that you want xp to be the default value (remember, l is implicit!). Then Coq infers that, since your default value has type list nat, the relevant l must have type list (list nat), which is why you get that error message in particular.

The solution is to rewrite with, for example, app_removelast_last 0 Hnilcons, since 0 is an adequate default value.

---

Edit: You may also avoid implicit arguments with @ as follows:

@app_removelast_last nat xp 0 Hnilcons

However, according to your comment you are not using the stdlib's version of this lemma, but Constant AlphaCode1_forward_c.app_removelast_last, which apparently is specific to lists of natural numbers and has no implicit arguments, so this is probably not what's causing the issue.