Integers of norm at most one

Stream: Is there code for X?

[Oliver Nash]

I'm embarrassed to ask this but is the following really missing:

import data.int.basic
import tactic

lemma int.abs_le_one_iff {n : ℤ} : |n| ≤ 1 ↔ n = 0 ∨ n = 1 ∨ n = -1 :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { obtain ⟨h₁, h₂⟩ := abs_le.mp h,
    rcases lt_trichotomy n 0 with hn | rfl | hn,
    { right, right, linarith, },
    { left, refl, },
    { right, left, linarith, }, },
  { rcases h with rfl | rfl | rfl; simp, },
end

[Oliver Nash]

(presumably the proof can be golfed ofc)

[Johan Commelin]

It seems to be missing, indeed. Here's a golf:

lemma int.abs_le_one_iff {n : ℤ} : |n| ≤ 1 ↔ n = 0 ∨ n = 1 ∨ n = -1 :=
begin
  rw abs_le, split; intro h,
  { cases h, interval_cases n; tauto },
  { rcases h with rfl | rfl | rfl; simp, },
end

[Ruben Van de Velde]

How slow is that interval_cases?

[Oliver Nash]

A very rough analysis suggests about 800ms.

[Oliver Nash]

More precisely, the difference between the elaboration times reported for the two proofs below is c.800ms:

import data.int.basic
import tactic

set_option profiler true
lemma int.abs_le_one_iff {n : ℤ} : |n| ≤ 1 ↔ n = 0 ∨ n = 1 ∨ n = -1 :=
begin
  rw abs_le,
  refine ⟨λ h, _, λ h, _⟩,
  { cases h, interval_cases n; sorry }, -- `tauto` closes but I want to estimate time for `interval_cases` without `tauto`
  { rcases h with rfl | rfl | rfl; simp, },
end

lemma int.abs_le_one_iff' {n : ℤ} : |n| ≤ 1 ↔ n = 0 ∨ n = 1 ∨ n = -1 :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { obtain ⟨h₁, h₂⟩ := abs_le.mp h,
    rcases lt_trichotomy n 0 with hn | rfl | hn,
    { right, right, linarith, },
    { left, refl, },
    { right, left, linarith, }, },
  { rcases h with rfl | rfl | rfl; simp, },
end

[Damiano Testa]

The version with < exists: let me find it.

[Damiano Testa]

docs#int.eq_zero_iff_abs_lt_one

[Oliver Nash]

Indeed I found this myself but I want ≤ :-)

[Damiano Testa]

Though it may not shorten your proofs much anyway.

[Yakov Pechersky]

A short proof might be via int.induction_on

[Oliver Nash]

I'll make a PR and people can compete there to golf it the most!

[Ruben Van de Velde]

Good idea

lemma int.abs_le_one_iff {n : ℤ} : |n| ≤ 1 ↔ n = 0 ∨ n = 1 ∨ n = -1 :=
by rw [le_iff_lt_or_eq, int.eq_zero_iff_abs_lt_one, abs_eq (@zero_le_one ℤ _)]

[Ruben Van de Velde]

Also, we might want to change the name to match the direction of the iff here

@[simp] lemma eq_zero_iff_abs_lt_one {a : ℤ} : |a| < 1 ↔ a = 0 :=

[Oliver Nash]

Another advantage of @Ruben Van de Velde 's proof is that it works in data/int/basic.lean where the heavier tactics the other proofs used are not available.

[Yaël Dillies]

That was my idea too, using the fact that integers are a succ_order to reduce |a| ≤ n + 1 to |a| ≤ n ∨ |a| = n + 1.

[Yaël Dillies]

docs#order.le_succ_iff_eq_or_le

[Oliver Nash]

#13513