The Coq mailing list

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

​​Hi Jonathan, Auger and Enrico,

Thanks a lot, you gave me the solution for my problem. First of all, yes, "sf" is globally defined:

Definition sf: Type:= list (non_terminal + terminal).

Second, I used an "unfold" before each rewrite as you suggested and now both rewrites work fine:

unfold sf in H7.

rewrite H7.

unfold sf in H9.

rewrite H9.

As a result, I have the goal as I wanted and I was able to finish my proof:

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 ([s ++ inl left :: s'] ++ [s ++ right ++ s'])

I still don´t understand why Coq didn´t make the conversion in the first place, but I will try to study the other information you sent to me and get to the point. 

Anyway, my script will look strange with apparently useless unfolds before these two rewrites. I guess I´ll have to add comments so that I and others can understand it in the future, but this doesn´t seem very natural. Unless, of course, display options are changed. But should it be like this? 

I´ll keep ssreflect in mind, thanks Enrico.

With My Best Regards,

Marcus.

2014-07-28 22:08 GMT-03:00 Jonathan <jonikelee AT gmail.com>:

On 07/28/2014 08:22 PM, Marcus Ramos wrote:

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

Marcus,

I don't see the definition of sf in the above goal - I guess it is defined globally.  One possibility is that Coq didn't immediately notice the equivalence between sf and (list (sum non_terminal terminal)) on the attempted rewrite - although it certainly understands that they are equivalent in other places.  In that case, what happens if you unfold sf in H7 and then retry the rewrite?  I have seen cases where Coq gets confused in the presence of type aliases such as sf.  In general, I have opted to use Notations instead of Definitions to make shorthand aliases for types, as Coq has no problems with notational aliases.

-- Jonathan