<commit_before>/-
Copyright (c) 2016 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import data.nat.pow
import order.min_max

/-!
# Basic operations on the integers

This file contains:
* instances on `ℤ`. The stronger one is `int.linear_ordered_comm_ring`.
* some basic lemmas about integers

## Recursors

* `int.rec`: Sign disjunction. Something is true/defined on `ℤ` if it's true/defined for nonnegative
  and for negative values.
* `int.bit_cases_on`: Parity disjunction. Something is true/defined on `ℤ` if it's true/defined for
  even and for odd values.
* `int.induction_on`: Simple growing induction on positive numbers, plus simple decreasing induction
  on negative numbers. Note that this recursor is currently only `Prop`-valued.
* `int.induction_on'`: Simple growing induction for numbers greater than `b`, plus simple decreasing
  induction on numbers less than `b`.
-/

open nat

namespace int

instance : inhabited ℤ := ⟨int.zero⟩

instance : nontrivial ℤ :=
⟨⟨0, 1, int.zero_ne_one⟩⟩

instance : comm_ring int :=
{ add            := int.add,
  add_assoc      := int.add_assoc,
  zero           := int.zero,
  zero_add       := int.zero_add,
  add_zero       := int.add_zero,
  neg            := int.neg,
  add_left_neg   := int.add_left_neg,
  add_comm       := int.add_comm,
  mul            := int.mul,
  mul_assoc      := int.mul_assoc,
  one            := int.one,
  one_mul        := int.one_mul,
  mul_one        := int.mul_one,
  sub            := int.sub,
  left_distrib   := int.distrib_left,
  right_distrib  := int.distrib_right,
  mul_comm       := int.mul_comm,
  zsmul          := (*),
  zsmul_zero'    := int.zero_mul,
  zsmul_succ'    := λ n x, by rw [succ_eq_one_add, of_nat_add, int.distrib_right, of_nat_one,
                                  int.one_mul],
  zsmul_neg'     := λ n x, neg_mul_eq_neg_mul_symm (n.succ : ℤ) x }

/-! ### Extra instances to short-circuit type class resolution

These also prevent non-computable instances like `int.normed_comm_ring` being used to construct
these instances non-computably.
-/
-- instance : has_sub int            := by apply_instance -- This is in core
instance : add_comm_monoid int    := by apply_instance
instance : add_monoid int         := by apply_instance
instance : monoid int             := by apply_instance
instance : comm_monoid int        := by apply_instance
instance : comm_semigroup int     := by apply_instance
instance : semigroup int          := by apply_instance
instance : add_comm_group int     := by apply_instance
instance : add_group int          := by apply_instance
instance : add_comm_semigroup int := by apply_instance
instance : add_semigroup int      := by apply_instance
instance : comm_semiring int      := by apply_instance
instance : semiring int           := by apply_instance
instance : ring int               := by apply_instance
instance : distrib int            := by apply_instance

instance : linear_ordered_comm_ring int :=
{ add_le_add_left := @int.add_le_add_left,
  mul_pos         := @int.mul_pos,
  zero_le_one     := le_of_lt int.zero_lt_one,
  .. int.comm_ring, .. int.linear_order, .. int.nontrivial }

instance : linear_ordered_add_comm_group int :=
by apply_instance

@[simp] lemma add_neg_one (i : ℤ) : i + -1 = i - 1 := rfl

theorem abs_eq_nat_abs : ∀ a : ℤ, |a| = nat_abs a
| (n : ℕ) := abs_of_nonneg $ coe_zero_le _
| -[1+ n] := abs_of_nonpos $ le_of_lt $ neg_succ_lt_zero _

theorem nat_abs_abs (a : ℤ) : nat_abs (|a|) = nat_abs a :=
by rw [abs_eq_nat_abs]; refl

theorem sign_mul_abs (a : ℤ) : sign a * |a| = a :=
by rw [abs_eq_nat_abs, sign_mul_nat_abs]

@[simp] lemma default_eq_zero : default ℤ = 0 := rfl

meta instance : has_to_format ℤ := ⟨λ z, to_string z⟩
meta instance : has_reflect ℤ := by tactic.mk_has_reflect_instance

attribute [simp] int.coe_nat_add int.coe_nat_mul int.coe_nat_zero int.coe_nat_one int.coe_nat_succ
attribute [simp] int.of_nat_eq_coe int.bodd

@[simp] theorem add_def {a b : ℤ} : int.add a b = a + b := rfl
@[simp] theorem mul_def {a b : ℤ} : int.mul a b = a * b := rfl

@[simp] lemma neg_succ_not_nonneg (n : ℕ) : 0 ≤ -[1+ n] ↔ false :=
by { simp only [not_le, iff_false], exact int.neg_succ_lt_zero n, }

@[simp] lemma neg_succ_not_pos (n : ℕ) : 0 < -[1+ n] ↔ false :=
by simp only [not_lt, iff_false]

@[simp] lemma neg_succ_sub_one (n : ℕ) : -[1+ n] - 1 = -[1+ (n+1)] := rfl
@[simp] theorem coe_nat_mul_neg_succ (m n : ℕ) : (m : ℤ) * -[1+ n] = -(m * succ n) := rfl
@[simp] theorem neg_succ_mul_coe_nat (m n : ℕ) : -[1+ m] * n = -(succ m * n) := rfl
@[simp] theorem neg_succ_mul_neg_succ (m n : ℕ) : -[1+ m] * -[1+ n] = succ m * succ n := rfl

@[simp, norm_cast]
theorem coe_nat_le {m n : ℕ} : (↑m : ℤ) ≤ ↑n ↔ m ≤ n := coe_nat_le_coe_nat_iff m n
@[simp, norm_cast]
theorem coe_nat_lt {m n : ℕ} : (↑m : ℤ) < ↑n ↔ m < n := coe_nat_lt_coe_nat_iff m n
@[simp, norm_cast]
theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n := int.coe_nat_eq_coe_nat_iff m n

@[simp] theorem coe_nat_pos {n : ℕ} : (0 : ℤ) < n ↔ 0 < n :=
by rw [← int.coe_nat_zero, coe_nat_lt]

@[simp] theorem coe_nat_eq_zero {n : ℕ} : (n : ℤ) = 0 ↔ n = 0 :=
by rw [← int.coe_nat_zero, coe_nat_inj']

theorem coe_nat_ne_zero {n : ℕ} : (n : ℤ) ≠ 0 ↔ n ≠ 0 :=
not_congr coe_nat_eq_zero

@[simp] lemma coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := coe_nat_le.2 (nat.zero_le _)

lemma coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
⟨λ h, nat.pos_of_ne_zero (coe_nat_ne_zero.1 h),
λ h, (ne_of_lt (coe_nat_lt.2 h)).symm⟩<commit_msg>feat(data/int/basic): coercion subtraction inequality (#10054)<commit_after>/-
Copyright (c) 2016 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import data.nat.pow
import order.min_max

/-!
# Basic operations on the integers

This file contains:
* instances on `ℤ`. The stronger one is `int.linear_ordered_comm_ring`.
* some basic lemmas about integers

## Recursors

* `int.rec`: Sign disjunction. Something is true/defined on `ℤ` if it's true/defined for nonnegative
  and for negative values.
* `int.bit_cases_on`: Parity disjunction. Something is true/defined on `ℤ` if it's true/defined for
  even and for odd values.
* `int.induction_on`: Simple growing induction on positive numbers, plus simple decreasing induction
  on negative numbers. Note that this recursor is currently only `Prop`-valued.
* `int.induction_on'`: Simple growing induction for numbers greater than `b`, plus simple decreasing
  induction on numbers less than `b`.
-/

open nat

namespace int

instance : inhabited ℤ := ⟨int.zero⟩

instance : nontrivial ℤ :=
⟨⟨0, 1, int.zero_ne_one⟩⟩

instance : comm_ring int :=
{ add            := int.add,
  add_assoc      := int.add_assoc,
  zero           := int.zero,
  zero_add       := int.zero_add,
  add_zero       := int.add_zero,
  neg            := int.neg,
  add_left_neg   := int.add_left_neg,
  add_comm       := int.add_comm,
  mul            := int.mul,
  mul_assoc      := int.mul_assoc,
  one            := int.one,
  one_mul        := int.one_mul,
  mul_one        := int.mul_one,
  sub            := int.sub,
  left_distrib   := int.distrib_left,
  right_distrib  := int.distrib_right,
  mul_comm       := int.mul_comm,
  zsmul          := (*),
  zsmul_zero'    := int.zero_mul,
  zsmul_succ'    := λ n x, by rw [succ_eq_one_add, of_nat_add, int.distrib_right, of_nat_one,
                                  int.one_mul],
  zsmul_neg'     := λ n x, neg_mul_eq_neg_mul_symm (n.succ : ℤ) x }

/-! ### Extra instances to short-circuit type class resolution

These also prevent non-computable instances like `int.normed_comm_ring` being used to construct
these instances non-computably.
-/
-- instance : has_sub int            := by apply_instance -- This is in core
instance : add_comm_monoid int    := by apply_instance
instance : add_monoid int         := by apply_instance
instance : monoid int             := by apply_instance
instance : comm_monoid int        := by apply_instance
instance : comm_semigroup int     := by apply_instance
instance : semigroup int          := by apply_instance
instance : add_comm_group int     := by apply_instance
instance : add_group int          := by apply_instance
instance : add_comm_semigroup int := by apply_instance
instance : add_semigroup int      := by apply_instance
instance : comm_semiring int      := by apply_instance
instance : semiring int           := by apply_instance
instance : ring int               := by apply_instance
instance : distrib int            := by apply_instance

instance : linear_ordered_comm_ring int :=
{ add_le_add_left := @int.add_le_add_left,
  mul_pos         := @int.mul_pos,
  zero_le_one     := le_of_lt int.zero_lt_one,
  .. int.comm_ring, .. int.linear_order, .. int.nontrivial }

instance : linear_ordered_add_comm_group int :=
by apply_instance

@[simp] lemma add_neg_one (i : ℤ) : i + -1 = i - 1 := rfl

theorem abs_eq_nat_abs : ∀ a : ℤ, |a| = nat_abs a
| (n : ℕ) := abs_of_nonneg $ coe_zero_le _
| -[1+ n] := abs_of_nonpos $ le_of_lt $ neg_succ_lt_zero _

theorem nat_abs_abs (a : ℤ) : nat_abs (|a|) = nat_abs a :=
by rw [abs_eq_nat_abs]; refl

theorem sign_mul_abs (a : ℤ) : sign a * |a| = a :=
by rw [abs_eq_nat_abs, sign_mul_nat_abs]

@[simp] lemma default_eq_zero : default ℤ = 0 := rfl

meta instance : has_to_format ℤ := ⟨λ z, to_string z⟩
meta instance : has_reflect ℤ := by tactic.mk_has_reflect_instance

attribute [simp] int.coe_nat_add int.coe_nat_mul int.coe_nat_zero int.coe_nat_one int.coe_nat_succ
attribute [simp] int.of_nat_eq_coe int.bodd

@[simp] theorem add_def {a b : ℤ} : int.add a b = a + b := rfl
@[simp] theorem mul_def {a b : ℤ} : int.mul a b = a * b := rfl

@[simp] lemma neg_succ_not_nonneg (n : ℕ) : 0 ≤ -[1+ n] ↔ false :=
by { simp only [not_le, iff_false], exact int.neg_succ_lt_zero n, }

@[simp] lemma neg_succ_not_pos (n : ℕ) : 0 < -[1+ n] ↔ false :=
by simp only [not_lt, iff_false]

@[simp] lemma neg_succ_sub_one (n : ℕ) : -[1+ n] - 1 = -[1+ (n+1)] := rfl
@[simp] theorem coe_nat_mul_neg_succ (m n : ℕ) : (m : ℤ) * -[1+ n] = -(m * succ n) := rfl
@[simp] theorem neg_succ_mul_coe_nat (m n : ℕ) : -[1+ m] * n = -(succ m * n) := rfl
@[simp] theorem neg_succ_mul_neg_succ (m n : ℕ) : -[1+ m] * -[1+ n] = succ m * succ n := rfl

@[simp, norm_cast]
theorem coe_nat_le {m n : ℕ} : (↑m : ℤ) ≤ ↑n ↔ m ≤ n := coe_nat_le_coe_nat_iff m n
@[simp, norm_cast]
theorem coe_nat_lt {m n : ℕ} : (↑m : ℤ) < ↑n ↔ m < n := coe_nat_lt_coe_nat_iff m n
@[simp, norm_cast]
theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n := int.coe_nat_eq_coe_nat_iff m n

@[simp] theorem coe_nat_pos {n : ℕ} : (0 : ℤ) < n ↔ 0 < n :=
by rw [← int.coe_nat_zero, coe_nat_lt]

@[simp] theorem coe_nat_eq_zero {n : ℕ} : (n : ℤ) = 0 ↔ n = 0 :=
by rw [← int.coe_nat_zero, coe_nat_inj']

theorem coe_nat_ne_zero {n : ℕ} : (n : ℤ) ≠ 0 ↔ n ≠ 0 :=
not_congr coe_nat_eq_zero

@[simp] lemma coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := coe_nat_le.2 (nat.zero_le _)

lemma le_coe_nat_sub (m n : ℕ) :
  (m - n : ℤ) ≤ ↑(m - n : ℕ) :=
begin
  by_cases h: m ≥ n,
  { exact le_of_eq (int.coe_nat_sub h).symm },
  { simp [le_of_not_ge h] }
end

lemma coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
⟨λ h, nat.pos_of_ne_zero (coe_nat_ne_zero.1 h),
λ h, (ne_of_lt (coe_nat_lt.2 h)).symm⟩
{'fraction_non_alphanumeric': 0.12653747455977346, 'fraction_numerical': 0.006813556322449341, 'mean_word_length': 3.1384108385206884, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '203294', 'n_tokens_mistral': 4806, 'n_tokens_neox': 4520, 'n_words': 1297}