## Stream: maths

### Topic: int.one_nonneg

#### Sebastien Gouezel (Mar 22 2019 at 14:48):

example : (0:ℤ) ≤ (2:ℤ) := int.one_nonneg


is puzzling me (as you expect, int.one_nonneg does not mention 2). I guess the kernel computes by itself, but still this is funny. This was found by library_search.

#### Johan Commelin (Mar 22 2019 at 14:49):

What you wrote is by definition 1 < 2 which is by definition 0 < 1. Is that right?

#### Sebastien Gouezel (Mar 22 2019 at 14:50):

It also works with 17, or whatever you like. Even 0 (but not -1 :)

#### Kevin Buzzard (Mar 22 2019 at 14:57):

The proof of int.one_nonneg mentions zero_lt_one:

example : (0 : ℤ) < (17 : ℤ) := int.zero_lt_one -- works fine


#### Kevin Buzzard (Mar 22 2019 at 14:58):

example : (0 : ℤ) < (17 : ℤ) = ((0 : ℤ) < (1 : ℤ)) := rfl


#### Kevin Buzzard (Mar 22 2019 at 14:59):

curiouser and curiouser

#### Johan Commelin (Mar 22 2019 at 14:59):

Both sides are true by definition?

#### Kevin Buzzard (Mar 22 2019 at 15:01):

example : ((2 : ℕ) + 2 = 4) = ((3 : ℕ) + 3 = 6) := rfl
/-
type mismatch, term
rfl
has type
?m_2 = ?m_2
but is expected to have type
2 + 2 = 4 = (3 + 3 = 6)
-/


#### Kevin Buzzard (Mar 22 2019 at 15:02):

example : (3 : ℤ) < (17 : ℤ) := int.zero_lt_one -- works


/me :confused:

#### Kevin Buzzard (Mar 22 2019 at 15:02):

maybe you can just prove everything using int.zero_lt_one

#### Sebastien Gouezel (Mar 22 2019 at 15:02):

2 + 2 = 4 is not true by definition. For the inequalities, the kernels can reduce them to true. So, when you give a proof which also reduces to true, it is happy.

#### Kevin Buzzard (Mar 22 2019 at 15:03):

I thought 2 + 2 = 4 was true by definition.

#### Kevin Buzzard (Mar 22 2019 at 15:04):

example : ∀ n x y z : ℕ, n ≥ 3 → x ^ n + y ^ n = z ^ n → x * y * z = 0 := int.zero_lt_one -- fails


#### Sebastien Gouezel (Mar 22 2019 at 15:04):

example : (3 : ℤ) < (17 : ℤ) := trivial -- works
example : ((2 : ℕ) + 2 = 4) := trivial -- fails


#### Kevin Buzzard (Mar 22 2019 at 15:04):

I see, rfl is different

#### Kevin Buzzard (Mar 22 2019 at 15:05):

So I can go through the library replacing all calls to int.zero_lt_one by trivial?

#### Sebastien Gouezel (Mar 22 2019 at 15:06):

rfl is for equalities only, I would say. And yes, it should work.

#### Kevin Buzzard (Mar 22 2019 at 15:08):

example : (3 : ℤ) < (17 : ℤ) = true := rfl


I see.

#### Scott Morrison (Mar 25 2019 at 02:29):

So should I consider this example example : (0:ℤ) ≤ (2:ℤ) := int.one_nonneg as a bug report against library_search?

#### Sebastien Gouezel (Mar 25 2019 at 06:54):

Not at all, this a perfectly valid and efficient proof. Rather as a remark that library_search is so efficient that it can uncover beautiful unexpected proofs.

Last updated: May 12 2021 at 08:14 UTC