Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Rewrite does not work

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewrite does not work


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Rewrite does not work
  • Date: Sun, 27 Jul 2014 14:52:04 -0400

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




Archive powered by MHonArc 2.6.18.

Top of Page