Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Rewrite question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewrite question


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page