The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/27/2014 02:24 PM, Marcus Ramos wrote:
> Hi,
>
> I have the following context/goal:
>
> 1 subgoals
> g : cfg
> n : nat
> l : list sf
> IHn : Datatypes.length (removelast l) >= 2 ->
>        (forall i : nat,
>         i <= Datatypes.length (removelast l) - 2 ->
>         exists (left : non_terminal) (right s s' : sf),
>           nth i (removelast l) [] = s ++ inl left :: s' /\
>           nth (S i) (removelast l) [] = s ++ right ++ s' /\ rules g left
> right) ->
>        sflist g (removelast l)
> H0 : Datatypes.length l = S n
> H1 : Datatypes.length l >= 2
> left : non_terminal
> right : sf
> s : sf
> s' : sf
> H6 : nth (Datatypes.length l - 2) l [] = s ++ inl left :: s'
> H7 : last l [] = s ++ right ++ s'
> H8 : rules g left right
> H3 : Datatypes.length (removelast l) = n
> H : Datatypes.length (removelast l) < 2
> H5 : nth (S (Datatypes.length l - 2)) l [] = last l []
> H9 : removelast l = [s ++ inl left :: s']
> ______________________________________(1/1)
> sflist g (removelast l ++ [last l []])
>
> and I get an error message when I try to "rewrite H7".
>
> The message is:
> Error: Found no subterm matching "last l []" in the current goal.
>
> Which is strange, since "last l []" appears as a subterm next to the end of
> the goal. A similar message appears if I try to "rewrite H9".
>
> I can´t figure out why this happens and how to get my goal written as:
>
> sflist g ([s ++ inl left :: s'] ++ [s ++ right ++ s'])
>
> Thanks in advance for any help.
>
> Best Regards,
> Marcus.

One thing to always try when this happens is Set Printing All, and then 
redisplay the goal.  Often, you'll see that the rewrite rule doesn't 
match the target anymore - due to implicit args and/or coercions.  
That's probably what is happening here.

-- Jonathan