The Coq mailing list

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

Hi,

I can´t see why "replace" does not work in the following case. The context is:

1 subgoals

g : cfg

i : nat

s : sentence

s0 : sf

l : list sf

n : non_terminal

H1 : sflist g (s0 :: [] :: l)

H2 : S i = Datatypes.length (s0 :: [] :: l)

H3 : s0 = [inl n]

H4 : last (s0 :: [] :: l) [] = map terminal_lift s

H5 : s <> []

left : non_terminal

right : sf

s' : sf

H21 : [] = right

H22 : rules g n right

______________________________________(1/1)

exists l' : list sf,

  sflist (g_emp g) l' /\

  hd [] l' = hd [] (s0 :: [] :: l) /\ last l' [] = last (s0 :: [] :: l) []

  

I execute "replace (s0 :: [] :: l) with ([s0] ++ ([] :: l)) in H1." and the new context that I get is:

2 subgoal

g : cfg

i : nat

s : sentence

s0 : sf

l : list sf

n : non_terminal

H1 : sflist g (s0 :: [] :: l)

H2 : S i = Datatypes.length (s0 :: [] :: l)

H3 : s0 = [inl n]

H4 : last (s0 :: [] :: l) [] = map terminal_lift s

H5 : s <> []

left : non_terminal

right : sf

s' : sf

H21 : [] = right

H22 : rules g n right

______________________________________(1/2)

exists l' : list sf,

  sflist (g_emp g) l' /\

  hd [] l' = hd [] (s0 :: [] :: l) /\ last l' [] = last (s0 :: [] :: l) []

______________________________________(2/2)

[s0] ++ [] :: l = s0 :: [] :: l

That is, instead of getting a new H1 (with the replacement required) and a corresponding new subogal, I get the same H1 as before and the new subgoal. "simpl in H1" before "replace" does not work as well. Any suggestions?

Thanks in advance,

Marcus.