integers between 0 and 3

Stream: general

[Kevin Buzzard]

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]

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

[Kenny Lau]

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]

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

[Kevin Buzzard]

PS thanks

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

got it

[Mario Carneiro]

We need a decidable instance for bounded integer ranges

[Kevin Buzzard]

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

[Mario Carneiro]

they are there in match, not in def patterns

[Mario Carneiro]

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]

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]

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

[Kenny Lau]

you're welcome to write 3 more instances

[Kenny Lau]

but the answer is no

[Kevin Buzzard]

You should PR all four

[Kenny Lau]

nah I'll wait till they accept my current PR

[Kenny Lau]

you can PR all four

[Kenny Lau]

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]

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

[Kevin Buzzard]

Thank you Kenny

[Kenny Lau]

Merged @Kevin Buzzard

[Tobias Grosser]

(deleted)