The Coq mailing list

["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.