Zulip Chat Archive

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

Johan Commelin (Mar 22 2019 at 15:02):

/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: Dec 20 2023 at 11:08 UTC