The Coq mailing list

[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

IHn : ge (@Datatypes.length sf (@removelast sf l)) (S (S O)) ->

      (forall i : nat,

       le i (minus (@Datatypes.length sf (@removelast sf l)) (S (S O))) ->

       @ex non_terminal

         (fun left : non_terminal =>

          @ex sf

            (fun right : sf =>

             @ex sf

               (fun s : sf =>

                @ex sf

                  (fun s' : sf =>

                   and

                     (@eq sf

                        (@nth sf i (@removelast sf l)

                           (@nil (sum non_terminal terminal)))

                        (@app (sum non_terminal terminal) s

                           (@cons (sum non_terminal terminal)

                              (@inl non_terminal terminal left) s')))

                     (and

                        (@eq sf

                           (@nth sf (S i) (@removelast sf l)

                              (@nil (sum non_terminal terminal)))

                           (@app (sum non_terminal terminal) s

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

                        (rules g left right))))))) ->

      sflist g (@removelast sf l)

H0 : @eq nat (@Datatypes.length sf l) (S n)

H1 : ge (@Datatypes.length sf l) (S (S O)) 

left : non_terminal

right : sf

s : sf

s' : sf

H6 : @eq sf

       (@nth sf (minus (@Datatypes.length sf l) (S (S O))) l

          (@nil (sum non_terminal terminal)))

       (@app (sum non_terminal terminal) s

          (@cons (sum non_terminal terminal)

             (@inl non_terminal terminal left) s'))

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

       (@app (sum non_terminal terminal) s

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

H8 : rules g left right

H3 : @eq nat (@Datatypes.length sf (@removelast sf l)) n

H : lt (@Datatypes.length sf (@removelast sf l)) (S (S O))

H5 : @eq sf

       (@nth sf (S (minus (@Datatypes.length sf l) (S (S O)))) l

          (@nil (sum non_terminal terminal)))

       (@last sf l (@nil (sum non_terminal terminal)))

H9 : @eq (list sf) (@removelast sf l)

       (@cons (list (sum non_terminal terminal))

          (@app (sum non_terminal terminal) s

             (@cons (sum non_terminal terminal)

                (@inl non_terminal terminal left) s'))

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

______________________________________(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. 

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.

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?