The Coq mailing list

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

Now I understand. Thank you very much for the detailed explanation.

Best Regards,

Marcus.

2014-06-04 10:03 GMT+02:00 Cedric Auger <sedrikov AT gmail.com>:

2014-06-03 20:42 GMT+02:00 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.

As I tried to explain, they do *not* remain exactly the same.
Implicit arguments are arguments that the user does not wish to be printed. For instance, consider the type list:

Inductive list (A : Type) : Type :=

  | nil : list A
  | cons : A -> list A -> list A.

So, for instance, if you want to define the reverse function for lists, you should type:

Definition reverse (A : Type) (l : list A) := rev_append l (nil A).
(or alternatively: Definition reverse (A : Type) (l : list A) := rev_append l (nil _).)

and not

Definition reverse (A : Type) (l : list A) := rev_append l nil.

provided you have a function rev_append with signature: ∀ A, list A → list A.

But here, the 'A' parameter of nil can easily be inferred, and some people (me included) find it annoying to have to type it.
So there is a mechanism to tell Coq whether or not a given parameter should be implicit (and allow the second definition).
In this case you can retrieve the non implicit behaviour by inserting '@' before functions:

Definition reverse (A : Type) (l : list A) := rev_append l (@nil A).

"Set Implicit Arguments." at the begin of file automatically does it, and there is also more fine grained commands, beginning with the "Argument" keyword which allows to tell what arguments should be set implicit.
There is also the curly braces mechanism.

Now back to the main subject:

Imagine you have the following context and goal:

A : Type
B : Type
l : list A
H : @nil ((fun X Y => X) A B) = l
f : list A -> list A
----------------------------------
f (@nil ((fun X Y => Y) B A)) = f l

with default display options, it is printed as:

A : Type
B : Type
l : list A
H : nil = l
f : list A -> list A
----------------------------------
f nil = f l

and there, you have the impression that you can prove it by "rewrite H. reflexivity.".
But here, "rewrite H." will  fail as the terms are not syntactically equal.
With "simpl in *." first, the things will be changed with:

A : Type
B : Type
l : list A
H : @nil A = l
f : list A -> list A
----------------------------------
f (@nil A) = f l

with default display options, it is printed as:

A : Type
B : Type
l : list A
H : nil = l
f : list A -> list A
----------------------------------
f nil = f l

so in appearance, nothing changed, but with the correct display options, you will see the real changes, and there H can be rewritten.

 

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\...

--
.../Sedrikov\...