## Stream: general

### Topic: integers between 0 and 3

#### Kevin Buzzard (Oct 20 2018 at 09:30):

example : ∀ (r : ℤ), r ≥ 0 → r < 3 → r = 0 ∨ r = 1 ∨ r = 2 := dec_trivial doesn't work for me. Is there any easy way of getting from $0\leq r<3$ (with r : int) to the three cases?

#### Kevin Buzzard (Oct 20 2018 at 09:31):

(with nat it works fine so there's a slightly painful way)

#### Kenny Lau (Oct 20 2018 at 09:44):

example : ∀ (r : ℤ), r ≥ 0 → r < 3 → r = 0 ∨ r = 1 ∨ r = 2
| (int.of_nat 0) _ _ := dec_trivial
| (int.of_nat 1) _ _ := dec_trivial
| (int.of_nat 2) _ _ := dec_trivial


#### Kevin Buzzard (Oct 20 2018 at 09:55):

So what is the equation compiler doing that dec_trivial can't do? It knows things which aren't decidable?

PS thanks

#### Kevin Buzzard (Oct 20 2018 at 09:58):

eew how do I sent this into the middle of a tactic proof?

#### Kevin Buzzard (Oct 20 2018 at 10:01):

example (r : ℤ) (H0 : r ≥ 0) (H3 : r < 3) : r = 0 ∨ r = 1 ∨ r = 2 :=
begin
exact match r, H0, H3 with
| (int.of_nat 0), _, _ := dec_trivial
| (int.of_nat 1), _, _ := dec_trivial
| (int.of_nat 2), _, _ := dec_trivial
end,
end


got it

#### Mario Carneiro (Oct 20 2018 at 10:04):

We need a decidable instance for bounded integer ranges

#### Kevin Buzzard (Oct 20 2018 at 10:05):

that too. I was just tripped over by commas by the way. They're sometimes there and sometimes not.

#### Mario Carneiro (Oct 20 2018 at 10:06):

they are there in match, not in def patterns

#### Mario Carneiro (Oct 20 2018 at 10:07):

I agree that this is an annoying inconsistency, but it also makes sense locally, if you change it then it doesn't fit something else

#### Kenny Lau (Oct 20 2018 at 10:12):

import data.finset

def int.range (m n : ℤ) : finset ℤ :=
(finset.range (int.to_nat (n-m))).map
⟨λ r, m+r, λ r s H, int.coe_nat_inj $add_left_cancel H⟩ theorem int.mem_range_iff {m n r : ℤ} : r ∈ int.range m n ↔ m ≤ r ∧ r < n := ⟨λ H, let ⟨s, h1, h2⟩ := finset.mem_map.1 H in h2 ▸ ⟨le_add_of_nonneg_right trivial, add_lt_of_lt_sub_left$ match n-m, h1 with
| (k:ℕ), h1 := by rwa [finset.mem_range, int.to_nat_coe_nat, ← int.coe_nat_lt] at h1
end⟩,
λ ⟨h1, h2⟩, finset.mem_map.2 ⟨int.to_nat (r-m),
finset.mem_range.2 $by rw [← int.coe_nat_lt, int.to_nat_of_nonneg (sub_nonneg_of_le h1), int.to_nat_of_nonneg (sub_nonneg_of_le (le_of_lt (lt_of_le_of_lt h1 h2)))]; exact sub_lt_sub_right h2 _, show m + _ = _, by rw [int.to_nat_of_nonneg (sub_nonneg_of_le h1), add_sub_cancel'_right]⟩⟩ instance int.decidable_bounded (P : int → Prop) [decidable_pred P] (m n : ℤ) : decidable (∀ r, m ≤ r → r < n → P r) := decidable_of_iff (∀ r ∈ int.range m n, P r)$ by simp only [int.mem_range_iff, and_imp]


#### Kevin Buzzard (Oct 20 2018 at 10:57):

Will this trigger if I have 1<= r <= 5?

#### Kenny Lau (Oct 20 2018 at 12:44):

you're welcome to write 3 more instances

#### Kevin Buzzard (Oct 20 2018 at 12:53):

You should PR all four

#### Kenny Lau (Oct 20 2018 at 12:53):

nah I'll wait till they accept my current PR

#### Kenny Lau (Oct 20 2018 at 12:53):

you can PR all four

#### Kenny Lau (Oct 20 2018 at 13:11):

import data.finset

def int.range (m n : ℤ) : finset ℤ :=
(finset.range (int.to_nat (n-m))).map
⟨λ r, m+r, λ r s H, int.coe_nat_inj $add_left_cancel H⟩ theorem int.mem_range_iff {m n r : ℤ} : r ∈ int.range m n ↔ m ≤ r ∧ r < n := ⟨λ H, let ⟨s, h1, h2⟩ := finset.mem_map.1 H in h2 ▸ ⟨le_add_of_nonneg_right trivial, add_lt_of_lt_sub_left$ match n-m, h1 with
| (k:ℕ), h1 := by rwa [finset.mem_range, int.to_nat_coe_nat, ← int.coe_nat_lt] at h1
end⟩,
λ ⟨h1, h2⟩, finset.mem_map.2 ⟨int.to_nat (r-m),
finset.mem_range.2 $by rw [← int.coe_nat_lt, int.to_nat_of_nonneg (sub_nonneg_of_le h1), int.to_nat_of_nonneg (sub_nonneg_of_le (le_of_lt (lt_of_le_of_lt h1 h2)))]; exact sub_lt_sub_right h2 _, show m + _ = _, by rw [int.to_nat_of_nonneg (sub_nonneg_of_le h1), add_sub_cancel'_right]⟩⟩ instance int.decidable_le_lt (P : int → Prop) [decidable_pred P] (m n : ℤ) : decidable (∀ r, m ≤ r → r < n → P r) := decidable_of_iff (∀ r ∈ int.range m n, P r)$ by simp only [int.mem_range_iff, and_imp]

instance int.decidable_le_le (P : int → Prop) [decidable_pred P] (m n : ℤ) : decidable (∀ r, m ≤ r → r ≤ n → P r) :=
decidable_of_iff (∀ r ∈ int.range m (n+1), P r) \$ by simp only [int.mem_range_iff, and_imp, int.lt_add_one_iff]

instance int.decidable_lt_lt (P : int → Prop) [decidable_pred P] (m n : ℤ) : decidable (∀ r, m < r → r < n → P r) :=
int.decidable_le_lt P _ _

instance int.decidable_lt_le (P : int → Prop) [decidable_pred P] (m n : ℤ) : decidable (∀ r, m < r → r ≤ n → P r) :=
int.decidable_le_le P _ _


#### Kenny Lau (Oct 28 2018 at 14:56):

https://github.com/leanprover/mathlib/pull/445 @Kevin Buzzard

Thank you Kenny

#### Kenny Lau (Oct 30 2018 at 18:14):

Merged @Kevin Buzzard

#### Tobias Grosser (Oct 30 2018 at 19:34):

(deleted)

Last updated: May 14 2021 at 22:15 UTC