Zulip Chat Archive

Stream: maths

Topic: int.one_nonneg


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Mar 22 2019 at 14:50):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 14:58):

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

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 14:59):

curiouser and curiouser

view this post on Zulip Johan Commelin (Mar 22 2019 at 14:59):

Both sides are true by definition?

view this post on Zulip 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)
-/

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 15:02):

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

view this post on Zulip Johan Commelin (Mar 22 2019 at 15:02):

/me :confused:

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 15:02):

maybe you can just prove everything using int.zero_lt_one

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 15:03):

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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Mar 22 2019 at 15:04):

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

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 15:04):

I see, rfl is different

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Mar 22 2019 at 15:06):

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

view this post on Zulip Kevin Buzzard (Mar 22 2019 at 15:08):

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

I see.

view this post on Zulip 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?

view this post on Zulip 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