The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 05/30/2014 02:19 PM, Marcus Ramos wrote:
> 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'')

Does it work to use the "pattern" tactic to factor out that term in the 
consequent?

-- Jonathan