The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi Cedric,

Thank you for your message. I am not using any display options, just running plain CoqIDE in Windows. However, I used "simpl in *" before the rewrite as you suggested, and now it works. Since the context and the goal remain exactly the same before and after the "simpl in *", I still don´t know what happened.

Best Regards,

Marcus.

2014-06-02 12:43 GMT+02:00 Cedric Auger <sedrikov AT gmail.com>:

As hinted, did you try to change the display options.

I do not know if it is the case here, but implicit parameters can be tricky from time to time.

For instance, imagine you have:

A predicate "foo" which first argument is implicit,
"@foo (f x) y = z" in your hypothesis and
"P (@foo w y) -> P z" as your goal, and furthermore, "f x" reduces to w.

Then you cannot rewrite your hypothesis in your goal as they are not syntactically equal.

If you have the default displaying options, still, it will look like:
"foo y = z" in your hypothesis and
"P (foo y) -> P z" as your goal

which might be a situation similar to the one you had.

Often a "simpl in *." before the rewrite can reduce terms so that they become syntactically equal.

2014-06-01 19:05 GMT+02:00 Marcus Ramos <marcus.ramos AT univasf.edu.br>:

Replace worked, thanks. However, I still don´t understand why rewrite <- did not work in this case.

Best Regards,

Marcus.

2014-05-31 16:23 GMT+02:00 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.

--
.../Sedrikov\...