The Coq mailing list

[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?