The Coq mailing list

[Ben Moseley <ben_moseley AT mac.com>]

The problem seems to be that the two different usages of '+' in your 'assert' 
are getting mapped to different 'plus' implementations.

This can be seen if you use:

Unset Printing Notations.

 assert (H: S (S n') + m = S (S (n' + m))).

...

   eq (plus (S (S n')) m) (S (S (Peano.plus n' m)))


Also, if you try these two:

 assert (H1:   (m + n') =   (n' + m)).
 assert (H2: S (m + n') = S (n' + m)).

You can see that the former is understood as: 

   eq (plus m n') (plus n' m)

...but the latter as: 

   eq (S (Peano.plus m n')) (S (Peano.plus n' m))

I don't know enough about Coq's Scope/Notation mechanism to explain why this 
is the case (from "About S." it seems likely it's because the argument of 'S' 
is declared to be in 'nat_scope'...), but hopefully the above is useful.

--Ben

On 26 Dec 2010, at 03:06, Eric Tanter wrote:

> On Dec 25, 2010, at 11:59 PM, Eric Tanter wrote:
> 
>> Note that I've just realized that the HTML page for Basics.v in SF:
>> http://www.cis.upenn.edu/~bcpierce/sf/Basics.html
>> 
>> defines plus within a Playground2 module in order to not mess up with the 
>> actual definition. 
>> 
>> But the file Basics.v that is distributed does not include these module 
>> declarations, so the definition of plus given there does interfere. 
> 
> I now realize this has been fixed already online. I was using an older 
> version of the files :/
> 
>> At this point, I guess I'm interested in understanding why the definition 
>> of plus used in the code below does not work.
> 
> This is still the case!
> 
> Thanks,
> 
> -- Éric