The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

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.