coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Rewrite question
- Date: Fri, 30 May 2014 20:19:46 +0200
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.
- [Coq-Club] Rewrite question, Marcus Ramos, 05/30/2014
- Re: [Coq-Club] Rewrite question, J. Ian Johnson, 05/30/2014
- Re: [Coq-Club] Rewrite question, Jonathan, 05/30/2014
- Re: [Coq-Club] Rewrite question, plastyx, 05/31/2014
Archive powered by MHonArc 2.6.18.