The Coq mailing list

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

Replace worked, thanks. However, I still don´t understand why rewrite <- did not work in this case.

Best Regards,

Marcus.

2014-05-31 16:23 GMT+02:00 plastyx <plastyx AT free.fr>:

Let's try

replace (s' ++ map (g_clo_sf_lift g) s'') with (s2 ++ inl (Start_clo g) :: s3).

 

Sometime things no longer remains the same when "display" options are changed ;)

----- Original Message -----

From: Marcus Ramos

To: coq-club AT inria.fr

Sent: Friday, May 30, 2014 8:19 PM

Subject: [Coq-Club] Rewrite question

Hi,

I must be missing something quite obvious, but right now I can´t see why rewrite doesn´t work in the current subgoal (see below). As I can see, the right hand side of H3 matches exactly a subterm in the goal. Any help will be appreciated.

CONTEXT+SUBGOALS:

================

2 subgoal

g : cfg

s2 : sf (g_clo g)

s3 : sf (g_clo g)

s' : sf (g_clo g)

s'' : sf g

H1 : derives (g_clo g) [inl (Start_clo g)] s'

H2 : derives g [inl (start_symbol g)] s''

H : derives (g_clo g) [inl (Start_clo g)] (s2 ++ inl (Start_clo g) :: s3)

H3 : s2 ++ inl (Start_clo g) :: s3 = s' ++ map (g_clo_sf_lift g) s''

H0 : g_clo_rules g (Start_clo g)

       [inl (Start_clo g); inl (Transf_clo g (start_symbol g))]

______________________________________(1/2)

In (inl (Start_clo g)) (s' ++ map (g_clo_sf_lift g) s'')

______________________________________(2/2)

derives (g_clo g) [inl (Start_clo g)] [] \/

(exists (s'0 : sf (g_clo g)) (s''0 : sf g),

   derives (g_clo g) [inl (Start_clo g)] s'0 /\

   derives g [inl (start_symbol g)] s''0 /\

   s2 ++ inl (Start_clo g) :: inl (Transf_clo g (start_symbol g)) :: s3 =

   s'0 ++ map (g_clo_sf_lift g) s''0)

SCRIPT:

======

...

rewrite <- H3.

...

SYSTEM MESSAGE:

==============

Error:

Found no subterm matching "s' ++ map (g_clo_sf_lift g) s''" in the current goal.

Thanks in advance,

Marcus.