The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-29 2:22 GMT+02:00 Marcus Ramos <marcus.ramos AT univasf.edu.br>:

​​

​​

Hi Auger and Jonathan,

Thank you for the replies. When I change the settings, this is what I get:

1 subgoals

g : cfg

n : nat

l : list sf

<cut>

right : sf

s : sf

s' : sf

<cut>

H7 : @eq sf (@last sf l (@nil (sum non_terminal terminal)))

       (@app (sum non_terminal terminal) s

          (@app (sum non_terminal terminal) right s'))

<cut>

______________________________________(1/1)

sflist g

  (@app (list (sum non_terminal terminal))

     (@removelast (list (sum non_terminal terminal)) l)

     (@cons (list (sum non_terminal terminal))

        (@last (list (sum non_terminal terminal)) l

           (@nil (sum non_terminal terminal)))

        (@nil (list (sum non_terminal terminal)))))

It seems that Coq, for some reason, changed "sf" in H7 for "(list (sum non_terminal terminal))" in the goal, and perhaps this is why rewrite does not work. 

I am pretty sure it is the case. That is what I explained in my previous post.
This often occurs with type inference:

When you write «last l [] = s ++ right ++ s'», it is seen by Coq as:
«@eq α (@last β l (@nil γ)) (@app δ s (@app ε right s'))»

From there, it must infer all the implicit types (greek letters).
As «right», «s» and «s'» have type «sf», Coq decides that «list δ=list ε=sf». «sf» has not the expected form, so Coq tries to unfold «sf», and gets «sf=list (sum non_terminal terminal)».
Thus «δ=ε=sum non_terminal terminal».
As «l» is of type «list sf», Coq decides that «β=sf», and «@nil γ» must then be of type «sf=list γ». Thus «γ=sum non_terminal terminal».
Left branch has thus type «sf», while right branch has type «list (sum non_terminal terminal)». Coq has then the choice for α between these two types (which are equal when normalized), the inference algorithm tells Coq to choose «sf» in this condition.

In your goal «sflist g (@app α' (@removelast β' l)(@cons γ' (@last δ' l (@nil ε')) (@nil ζ')))» Coq inference decides that «@last δ' l (@nil ε')» must be of type «sum non_terminal terminal», and thus decides that «δ'=list (sum … …)».

This is a possible and simple scenario. There are also other scenarios in which the type was the same, but at some point in your proof one of your tactic either unfolded a «sf» into a «list (sum … …)» or folded a «list (sum … …)» into a «sf» (this can also be a way to fix your problem, see below).

 

However, this is exactly the definition of "sf". Why things look different when the settings are changed? Why did this happen and how do I fix it? This is all very confusing for me.

This looks different because some people do not like to have to insert «extraneous» information in their terms. If there were no notations, nor implicit arguments, you would have to write things like:
«cons bool True (cons bool False (cons bool True (nil bool)))» for what you could write if only notations were missing:
«cons True (cons False (cons True nil))».
Of course this problem could be made almost as readable without using implicit arguments with a:
«let nil := nil bool in let cons := cons bool in
 cons True (cons False (cons True nil))»
(or put bnil := nil bool and bcons := cons bool at top level). But the first line would be annoying to type each time you want to specialize a type.
Thus people allowed Coq to perform type inference, leading to terms like:
«cons _ True (cons _ False (cons _ True (nil _)))». Which are more readable, but when a function has many types which can be inferred, this ends in terms like:
«foo _ _ _ bar baz _ O _ (S O)» where you have to count how many holes you have to insert at each place.
Thus a need of implicit arguments arose.
If you want to work in Coq without what can appear to be "black magic" and much more predictable, you should deactivate printing of implicit arguments, deactivate use of notations, always prefix your functions with "@", and never use "_". It is interesting to do it from time to time on not too hard problems, and provides better understanding of the system. But for practical cases, I do not encourage this use.
Notations deserve a similar purpose. In fact you could almost encode implicit arguments with Notations.

Now for the how to fix it, there are multiple solutions:
- the local one: change the terms to be syntactically the same.
  Useful tactics: change, fold, unfold (and probably others); these tactics often allow to target a specific location («at» keyword) of a specific hypothesis («in» keyword)
  Examples: «unfold sf in H7; rewrite H7.», «fold sf; rewrite H7.», «change (list (sum non_terminal terminal)) with sf; rewrite H7.»
- avoid use of type aliases (like sf). This is generally a bad idea, as you will have to be quite verbose, and the terms will be big (this is likely to degrade performances).
- monomorphize your code (ie. use specialized functions). Thus a "Definition sf_last : list sf -> sf := fun (l:list sf) => @last sf l []." and then use "sf_last l" in your lemma would probably have solved your problem.

In practice, I most often use the 1st proposed solution. It is the more practical. 2nd solution is a bad one from my point of view, and 3rd solution can be used for some functions, when you think that the use of your first solution arise way too often.

 

Thanks again,

Marcus.

2014-07-27 17:33 GMT-03:00 AUGER Cédric <sedrikov AT gmail.com>:

Le Sun, 27 Jul 2014 15:24:48 -0300,
Marcus Ramos <marcus.ramos AT univasf.edu.br> a écrit :

> Hi,
>
> I have the following context/goal:
>
> 1 subgoals
> g : cfg
> n : nat
> l : list sf
> IHn : Datatypes.length (removelast l) >= 2 ->
>       (forall i : nat,
>        i <= Datatypes.length (removelast l) - 2 ->
>        exists (left : non_terminal) (right s s' : sf),
>          nth i (removelast l) [] = s ++ inl left :: s' /\
>          nth (S i) (removelast l) [] = s ++ right ++ s' /\ rules g
> left right) ->
>       sflist g (removelast l)
> H0 : Datatypes.length l = S n
> H1 : Datatypes.length l >= 2
> left : non_terminal
> right : sf
> s : sf
> s' : sf
> H6 : nth (Datatypes.length l - 2) l [] = s ++ inl left :: s'
> H7 : last l [] = s ++ right ++ s'
> H8 : rules g left right
> H3 : Datatypes.length (removelast l) = n
> H : Datatypes.length (removelast l) < 2
> H5 : nth (S (Datatypes.length l - 2)) l [] = last l []
> H9 : removelast l = [s ++ inl left :: s']
> ______________________________________(1/1)
> sflist g (removelast l ++ [last l []])
>
> and I get an error message when I try to "rewrite H7".
>
> The message is:
> Error: Found no subterm matching "last l []" in the current goal.
>
> Which is strange, since "last l []" appears as a subterm next to the
> end of the goal. A similar message appears if I try to "rewrite H9".
>
> I can´t figure out why this happens and how to get my goal written as:
>
> sflist g ([s ++ inl left :: s'] ++ [s ++ right ++ s'])
>
> Thanks in advance for any help.
>
> Best Regards,
> Marcus.

I lack some information, but I bet it is due to implicit arguments.

In the following, the error is also raised, but it is more expected:

Definition natnat := prod nat nat.
Lemma foo : forall l, @Nil natnat = l -> @Nil (prod nat nat) = l.
Proof.
  intros l Hl.
  rewrite Hl.

Still, the context will look like:

l : list natnat
H : Nil = l
==================
Nil = l


What would be nice with Coq reporting error is the following behavior:
if there is a subterm which is printed exactly like the one reported in
the error, then reprint the hypothesis and the error with display of
implicit arguments.

For rewrite it may be not completely obvious on how to do it, but for
the error "xxx has type yyy while it is expected to have type yyy",
there temporarily automatically set display of implicit arguments could
be helpful (and probably reduce the number of questions of this type
on the Coq list).

To make it brief, Marcus, what displays when you deactivate printing on
notations and activate display of implicit arguments?

2014-07-27 17:33 GMT-03:00 AUGER Cédric <sedrikov AT gmail.com>:

Le Sun, 27 Jul 2014 15:24:48 -0300,
Marcus Ramos <marcus.ramos AT univasf.edu.br> a écrit :

> Hi,
>
> I have the following context/goal:
>
> 1 subgoals
> g : cfg
> n : nat
> l : list sf
> IHn : Datatypes.length (removelast l) >= 2 ->
>       (forall i : nat,
>        i <= Datatypes.length (removelast l) - 2 ->
>        exists (left : non_terminal) (right s s' : sf),
>          nth i (removelast l) [] = s ++ inl left :: s' /\
>          nth (S i) (removelast l) [] = s ++ right ++ s' /\ rules g
> left right) ->
>       sflist g (removelast l)
> H0 : Datatypes.length l = S n
> H1 : Datatypes.length l >= 2
> left : non_terminal
> right : sf
> s : sf
> s' : sf
> H6 : nth (Datatypes.length l - 2) l [] = s ++ inl left :: s'
> H7 : last l [] = s ++ right ++ s'
> H8 : rules g left right
> H3 : Datatypes.length (removelast l) = n
> H : Datatypes.length (removelast l) < 2
> H5 : nth (S (Datatypes.length l - 2)) l [] = last l []
> H9 : removelast l = [s ++ inl left :: s']
> ______________________________________(1/1)
> sflist g (removelast l ++ [last l []])
>
> and I get an error message when I try to "rewrite H7".
>
> The message is:
> Error: Found no subterm matching "last l []" in the current goal.
>
> Which is strange, since "last l []" appears as a subterm next to the
> end of the goal. A similar message appears if I try to "rewrite H9".
>
> I can´t figure out why this happens and how to get my goal written as:
>
> sflist g ([s ++ inl left :: s'] ++ [s ++ right ++ s'])
>
> Thanks in advance for any help.
>
> Best Regards,
> Marcus.

I lack some information, but I bet it is due to implicit arguments.

In the following, the error is also raised, but it is more expected:

Definition natnat := prod nat nat.
Lemma foo : forall l, @Nil natnat = l -> @Nil (prod nat nat) = l.
Proof.
  intros l Hl.
  rewrite Hl.

Still, the context will look like:

l : list natnat
H : Nil = l
==================
Nil = l


What would be nice with Coq reporting error is the following behavior:
if there is a subterm which is printed exactly like the one reported in
the error, then reprint the hypothesis and the error with display of
implicit arguments.

For rewrite it may be not completely obvious on how to do it, but for
the error "xxx has type yyy while it is expected to have type yyy",
there temporarily automatically set display of implicit arguments could
be helpful (and probably reduce the number of questions of this type
on the Coq list).

To make it brief, Marcus, what displays when you deactivate printing on
notations and activate display of implicit arguments?

--
.../Sedrikov\...