confusing behavior of 'tauto'

Stream: new members

[Daniil Homza]

Hi all,

I've discovered 'tauto' function proving a false statement. I try some others configuration and it looks like lean understand that something is wrong, however in this case it returns that "goal accomplished". Some help? Thanks in advance Lean_conf.PNG

[Vincent Beffara]

This statement is true (k=0 fits). It's just that - on natural numbers does not mean what you might expect (it is truncating at 0).

[Adam Topaz]

It's a true statement because the naturals use truncated subtraction.

[Daniil Homza]

k=0 is not fits because 0<n-1000 for lots of natural

[Vincent Beffara]

For Lean, 1 - 2 (within natural numbers) is equal to 0.

[Daniil Homza]

oh, I see what you mean, Thank you!

[Riccardo Brasca]

Here for more information about this convention, and why it is not so absurd. In any case the slogan is "don't use subtraction of natural numbers unless you really know what you're doing (use integers instead). And similarly for division".

[Yaël Dillies]

Basically - on nat is an well-behaved operation from the point of view of order theory, not from the point of view of algebra. Same for division, real.sqrt, etc...

[Adam Topaz]

IIRC, division actually works quite well if you always remember that it gives the quotient in the sense of the division algorithm as opposed to the rational number one might expect. Think division in python 2 vs python 3 (I don't know if you find that helpful).