The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

I think you want rewrite -> H3 (which is equivalently rewrite H3).
-Ian
----- Original Message -----
From: "Marcus Ramos" 
<marcus.ramos AT univasf.edu.br>
To: 
coq-club AT inria.fr
Sent: Friday, May 30, 2014 2:19:46 PM GMT -05:00 US/Canada Eastern
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.