Zulip Chat Archive

Stream: general

Topic: integers between 0 and 3


view this post on Zulip 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 0r<30\leq r<3 (with r : int) to the three cases?

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 09:31):

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

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

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

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 09:55):

PS thanks

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 09:58):

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

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

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 10:04):

got it

view this post on Zulip Mario Carneiro (Oct 20 2018 at 10:04):

We need a decidable instance for bounded integer ranges

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

view this post on Zulip Mario Carneiro (Oct 20 2018 at 10:06):

they are there in match, not in def patterns

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

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

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 10:57):

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

view this post on Zulip Kenny Lau (Oct 20 2018 at 12:44):

you're welcome to write 3 more instances

view this post on Zulip Kenny Lau (Oct 20 2018 at 12:44):

but the answer is no

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 12:53):

You should PR all four

view this post on Zulip Kenny Lau (Oct 20 2018 at 12:53):

nah I'll wait till they accept my current PR

view this post on Zulip Kenny Lau (Oct 20 2018 at 12:53):

you can PR all four

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

view this post on Zulip Kenny Lau (Oct 28 2018 at 14:56):

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

view this post on Zulip Kevin Buzzard (Oct 28 2018 at 15:03):

Thank you Kenny

view this post on Zulip Kenny Lau (Oct 30 2018 at 18:14):

Merged @Kevin Buzzard

view this post on Zulip Tobias Grosser (Oct 30 2018 at 19:34):

(deleted)


Last updated: May 14 2021 at 22:15 UTC