From c03d3517442a73f2f2a6935d7999be7ff44dc0ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Apr 2018 13:29:06 -0700 Subject: [PATCH] chore(library/init/data/int): keep only definitions --- library/init/data/int/basic.lean | 407 +++---------------------- library/init/data/int/comp_lemmas.lean | 120 -------- library/init/data/int/default.lean | 2 +- library/init/data/int/order.lean | 307 ------------------- 4 files changed, 50 insertions(+), 786 deletions(-) delete mode 100644 library/init/data/int/comp_lemmas.lean delete mode 100644 library/init/data/int/order.lean diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index adb45481e7..fbf58f8f8d 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad The integers, with addition, multiplication, and subtraction. -/ prelude -import init.data.nat.lemmas init.data.nat.gcd init.meta.transfer init.data.list +import init.data.nat.gcd init.meta.transfer init.data.list open nat /- the type, coercions, and notation -/ @@ -34,204 +34,71 @@ instance : has_to_string int := namespace int -protected lemma coe_nat_eq (n : ℕ) : ↑n = int.of_nat n := rfl +protected def zero : int := of_nat 0 +protected def one : int := of_nat 1 -protected def zero : ℤ := of_nat 0 -protected def one : ℤ := of_nat 1 - -instance : has_zero ℤ := ⟨int.zero⟩ -instance : has_one ℤ := ⟨int.one⟩ - -lemma of_nat_zero : of_nat (0 : nat) = (0 : int) := rfl - -lemma of_nat_one : of_nat (1 : nat) = (1 : int) := rfl +instance : has_zero int := ⟨int.zero⟩ +instance : has_one int := ⟨int.one⟩ /- definitions of basic functions -/ -def neg_of_nat : ℕ → ℤ +def neg_of_nat : ℕ → int | 0 := 0 | (succ m) := -[1+ m] -def sub_nat_nat (m n : ℕ) : ℤ := +def sub_nat_nat (m n : ℕ) : int := match (n - m : nat) with | 0 := of_nat (m - n) -- m ≥ n | (succ k) := -[1+ k] -- m < n, and n - m = succ k end -protected def neg : ℤ → ℤ +protected def neg : int → int | (of_nat n) := neg_of_nat n | -[1+ n] := succ n -protected def add : ℤ → ℤ → ℤ +protected def add : int → int → int | (of_nat m) (of_nat n) := of_nat (m + n) | (of_nat m) -[1+ n] := sub_nat_nat m (succ n) | -[1+ m] (of_nat n) := sub_nat_nat n (succ m) | -[1+ m] -[1+ n] := -[1+ succ (m + n)] -protected def mul : ℤ → ℤ → ℤ +protected def mul : int → int → int | (of_nat m) (of_nat n) := of_nat (m * n) | (of_nat m) -[1+ n] := neg_of_nat (m * succ n) | -[1+ m] (of_nat n) := neg_of_nat (succ m * n) | -[1+ m] -[1+ n] := of_nat (succ m * succ n) -instance : has_neg ℤ := ⟨int.neg⟩ -instance : has_add ℤ := ⟨int.add⟩ -instance : has_mul ℤ := ⟨int.mul⟩ +instance : has_neg int := ⟨int.neg⟩ +instance : has_add int := ⟨int.add⟩ +instance : has_mul int := ⟨int.mul⟩ -lemma of_nat_add (n m : ℕ) : of_nat (n + m) = of_nat n + of_nat m := rfl -lemma of_nat_mul (n m : ℕ) : of_nat (n * m) = of_nat n * of_nat m := rfl -lemma of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := rfl +protected def sub (m n : int) : int := +m + -n -lemma neg_of_nat_zero : -(of_nat 0) = 0 := rfl -lemma neg_of_nat_of_succ (n : ℕ) : -(of_nat (succ n)) = -[1+ n] := rfl -lemma neg_neg_of_nat_succ (n : ℕ) : -(-[1+ n]) = of_nat (succ n) := rfl +instance : has_sub int := ⟨int.sub⟩ -lemma of_nat_eq_coe (n : ℕ) : of_nat n = ↑n := rfl -lemma neg_succ_of_nat_coe (n : ℕ) : -[1+ n] = -↑(n + 1) := rfl - -protected lemma coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n := rfl -protected lemma coe_nat_mul (m n : ℕ) : (↑(m * n) : ℤ) = ↑m * ↑n := rfl -protected lemma coe_nat_zero : ↑(0 : ℕ) = (0 : ℤ) := rfl -protected lemma coe_nat_one : ↑(1 : ℕ) = (1 : ℤ) := rfl -protected lemma coe_nat_succ (n : ℕ) : (↑(succ n) : ℤ) = ↑n + 1 := rfl - -protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl -protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl -protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl - -/- injectivity of the constructor functions -/ - -protected lemma of_nat_inj {m n : ℕ} (h : of_nat m = of_nat n) : m = n := -int.no_confusion h id - -protected lemma coe_nat_inj {m n : ℕ} (h : (↑m : ℤ) = ↑n) : m = n := -int.of_nat_inj h - -lemma of_nat_eq_of_nat_iff (m n : ℕ) : of_nat m = of_nat n ↔ m = n := -iff.intro int.of_nat_inj (congr_arg _) - -protected lemma coe_nat_eq_coe_nat_iff (m n : ℕ) : (↑m : ℤ) = ↑n ↔ m = n := -of_nat_eq_of_nat_iff m n - -lemma neg_succ_of_nat_inj {m n : ℕ} (h : neg_succ_of_nat m = neg_succ_of_nat n) : m = n := -int.no_confusion h id - -lemma neg_succ_of_nat_inj_iff {m n : ℕ} : neg_succ_of_nat m = neg_succ_of_nat n ↔ m = n := -⟨neg_succ_of_nat_inj, assume H, by simp [H]⟩ - -lemma neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl - -/- basic properties of sub_nat_nat -/ - -lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop) - (hp : ∀i n, P (n + i) n (of_nat i)) - (hn : ∀i m, P m (m + i + 1) (-[1+ i])) : - P m n (sub_nat_nat m n) := -begin - have H : ∀k, n - m = k → P m n (nat.cases_on k (of_nat (m - n)) (λa, -[1+ a])), - { intro k, cases k, - { intro e, - cases (nat.le.dest (nat.le_of_sub_eq_zero e)) with k h, - rw [h.symm, nat.add_sub_cancel_left], - apply hp }, - { intro heq, - have h : m ≤ n, - { exact nat.le_of_lt (nat.lt_of_sub_eq_succ heq) }, - rw [nat.sub_eq_iff_eq_add h] at heq, - rw [heq, add_comm], - apply hn } }, - delta sub_nat_nat, - exact H _ rfl -end - -private lemma sub_nat_nat_add_left {m n : ℕ} : - sub_nat_nat (m + n) m = of_nat n := -begin - dunfold sub_nat_nat, - rw [nat.sub_eq_zero_of_le], - dunfold sub_nat_nat._match_1, - rw [nat.add_sub_cancel_left], - apply nat.le_add_right -end - -private lemma sub_nat_nat_add_right {m n : ℕ} : - sub_nat_nat m (m + n + 1) = neg_succ_of_nat n := -calc sub_nat_nat._match_1 m (m + n + 1) (m + n + 1 - m) = - sub_nat_nat._match_1 m (m + n + 1) (m + (n + 1) - m) : by simp - ... = sub_nat_nat._match_1 m (m + n + 1) (n + 1) : by rw [nat.add_sub_cancel_left] - ... = neg_succ_of_nat n : rfl - -private lemma sub_nat_nat_add_add (m n k : ℕ) : sub_nat_nat (m + k) (n + k) = sub_nat_nat m n := -sub_nat_nat_elim m n (λm n i, sub_nat_nat (m + k) (n + k) = i) - (assume i n, have n + i + k = (n + k) + i, by simp, - begin rw [this], exact sub_nat_nat_add_left end) - (assume i m, have m + i + 1 + k = (m + k) + i + 1, by simp, - begin rw [this], exact sub_nat_nat_add_right end) - -/- nat_abs -/ - -@[simp] def nat_abs : ℤ → ℕ +@[simp] def nat_abs : int → ℕ | (of_nat m) := m | -[1+ m] := succ m -lemma nat_abs_of_nat (n : ℕ) : nat_abs ↑n = n := rfl - -lemma eq_zero_of_nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0 -| (of_nat m) H := congr_arg of_nat H -| -[1+ m'] H := absurd H (succ_ne_zero _) - -lemma nat_abs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) : nat_abs a > 0 := -(eq_zero_or_pos _).resolve_left $ mt eq_zero_of_nat_abs_eq_zero h - -lemma nat_abs_zero : nat_abs (0 : int) = (0 : nat) := rfl - -lemma nat_abs_one : nat_abs (1 : int) = (1 : nat) := rfl - -lemma nat_abs_mul_self : Π {a : ℤ}, ↑(nat_abs a * nat_abs a) = a * a -| (of_nat m) := rfl -| -[1+ m'] := rfl - -@[simp] lemma nat_abs_neg (a : ℤ) : nat_abs (-a) = nat_abs a := -by {cases a with n n, cases n; refl, refl} - -lemma nat_abs_eq : Π (a : ℤ), a = nat_abs a ∨ a = -(nat_abs a) -| (of_nat m) := or.inl rfl -| -[1+ m'] := or.inr rfl - -lemma eq_coe_or_neg (a : ℤ) : ∃n : ℕ, a = n ∨ a = -n := ⟨_, nat_abs_eq a⟩ - -/- sign -/ - -def sign : ℤ → ℤ +def sign : int → int | (n+1:ℕ) := 1 | 0 := 0 | -[1+ n] := -1 -@[simp] theorem sign_zero : sign 0 = 0 := rfl -@[simp] theorem sign_one : sign 1 = 1 := rfl -@[simp] theorem sign_neg_one : sign (-1) = -1 := rfl - -/- Quotient and remainder -/ - --- There are three main conventions for integer division, --- referred here as the E, F, T rounding conventions. --- All three pairs satisfy the identity x % y + (x / y) * y = x --- unconditionally. - --- E-rounding: This pair satisfies 0 ≤ mod x y < nat_abs y for y ≠ 0 -protected def div : ℤ → ℤ → ℤ +protected def div : int → int → int | (m : ℕ) (n : ℕ) := of_nat (m / n) | (m : ℕ) -[1+ n] := -of_nat (m / succ n) | -[1+ m] 0 := 0 | -[1+ m] (n+1:ℕ) := -[1+ m / succ n] | -[1+ m] -[1+ n] := of_nat (succ (m / succ n)) -protected def mod : ℤ → ℤ → ℤ +protected def mod : int → int → int | (m : ℕ) n := (m % nat_abs n : ℕ) | -[1+ m] n := sub_nat_nat (nat_abs n) (succ (m % nat_abs n)) -- F-rounding: This pair satisfies fdiv x y = floor (x / y) -def fdiv : ℤ → ℤ → ℤ +def fdiv : int → int → int | 0 _ := 0 | (m : ℕ) (n : ℕ) := of_nat (m / n) | (m+1:ℕ) -[1+ n] := -[1+ m / succ n] @@ -239,7 +106,7 @@ def fdiv : ℤ → ℤ → ℤ | -[1+ m] (n+1:ℕ) := -[1+ m / succ n] | -[1+ m] -[1+ n] := of_nat (succ m / succ n) -def fmod : ℤ → ℤ → ℤ +def fmod : int → int → int | 0 _ := 0 | (m : ℕ) (n : ℕ) := of_nat (m % n) | (m+1:ℕ) -[1+ n] := sub_nat_nat (m % succ n) n @@ -247,225 +114,49 @@ def fmod : ℤ → ℤ → ℤ | -[1+ m] -[1+ n] := -of_nat (succ m % succ n) -- T-rounding: This pair satisfies quot x y = round_to_zero (x / y) -def quot : ℤ → ℤ → ℤ +def quot : int → int → int | (of_nat m) (of_nat n) := of_nat (m / n) | (of_nat m) -[1+ n] := -of_nat (m / succ n) | -[1+ m] (of_nat n) := -of_nat (succ m / n) | -[1+ m] -[1+ n] := of_nat (succ m / succ n) -def rem : ℤ → ℤ → ℤ +def rem : int → int → int | (of_nat m) (of_nat n) := of_nat (m % n) | (of_nat m) -[1+ n] := of_nat (m % succ n) | -[1+ m] (of_nat n) := -of_nat (succ m % n) | -[1+ m] -[1+ n] := -of_nat (succ m % succ n) -instance : has_div ℤ := ⟨int.div⟩ -instance : has_mod ℤ := ⟨int.mod⟩ +instance : has_div int := ⟨int.div⟩ +instance : has_mod int := ⟨int.mod⟩ -/- gcd -/ +def gcd (m n : int) : ℕ := gcd (nat_abs m) (nat_abs n) -def gcd (m n : ℤ) : ℕ := gcd (nat_abs m) (nat_abs n) - -/-- Relator between integers and pairs of natural numbers -/ - -inductive rel_int_nat_nat : ℤ → ℕ × ℕ → Prop -| pos : ∀{m p}, rel_int_nat_nat (of_nat p) (m + p, m) -| neg : ∀{m n}, rel_int_nat_nat (neg_succ_of_nat n) (m, m + n + 1) - -protected lemma rel_sub_nat_nat {a b : ℕ} : rel_int_nat_nat (sub_nat_nat a b) (a, b) := -sub_nat_nat_elim a b (λa b i, rel_int_nat_nat i (a, b)) - (assume i n, rel_int_nat_nat.pos) (assume i n, rel_int_nat_nat.neg) - -instance right_total_rel_int_nat_nat : relator.right_total rel_int_nat_nat -| (n, m) := ⟨_, int.rel_sub_nat_nat⟩ - -instance left_total_rel_int_nat_nat : relator.left_total rel_int_nat_nat -| (of_nat n) := ⟨(0 + n, 0), rel_int_nat_nat.pos⟩ -| (neg_succ_of_nat n) := ⟨(0, 0 + n + 1), rel_int_nat_nat.neg⟩ - -instance bi_total_rel_int_nat_nat : relator.bi_total rel_int_nat_nat := -⟨int.left_total_rel_int_nat_nat, int.right_total_rel_int_nat_nat⟩ - -protected lemma rel_neg_of_nat {m} : ∀{n}, rel_int_nat_nat (neg_of_nat n) (m, m + n) -| 0 := rel_int_nat_nat.pos -| (nat.succ n) := rel_int_nat_nat.neg - -protected lemma rel_eq : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ iff)) - eq (λa b, a.1 + b.2 = b.1 + a.2) -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := - calc of_nat p = of_nat p' - ↔ (m + m') + p = (m + m') + p' : by rw [of_nat_eq_of_nat_iff, add_left_cancel_iff] - ... ↔ (m + p) + m' = (m' + p') + m : by simp -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') := - calc of_nat p = -[1+ n'] ↔ (m' + m) + (n' + p + 1) = (m' + m) + 0 : - begin rw [add_left_cancel_iff], apply iff.intro; intro; contradiction end - ... ↔ (m + p) + (m' + n' + 1) = m' + m : by simp -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := - calc -[1+ n] = of_nat p' ↔ (m + m') + 0 = (m + m') + (n + p' + 1) : - begin rw [add_left_cancel_iff], apply iff.intro; intro; contradiction end - ... ↔ m + m' = m' + p' + (m + n + 1) : by simp -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := - calc -[1+ n] = -[1+ n'] ↔ (m + m' + 1) + n' = (m + m' + 1) + n : - by rw [neg_succ_of_nat_inj_iff, add_left_cancel_iff, eq_comm] - ... ↔ m + (m' + n' + 1) = m' + (m + n + 1) : by simp - -/- should this be more general, i.e. ∀{n}, rel_int_nat_nat 0 (n, n) ? -/ -protected lemma rel_zero : rel_int_nat_nat 0 (0, 0) := -rel_int_nat_nat.pos - -protected lemma rel_one : rel_int_nat_nat 1 (1, 0) := -rel_int_nat_nat.pos - -protected lemma rel_neg : (rel_int_nat_nat ⇒ rel_int_nat_nat) has_neg.neg (λa, (a.2, a.1)) -| ._ ._ (@rel_int_nat_nat.pos m p) := int.rel_neg_of_nat -| ._ ._ (@rel_int_nat_nat.neg m n) := rel_int_nat_nat.pos - -protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat)) - has_add.add (λa b, (a.1 + b.1, a.2 + b.2)) -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := - have eq : m + p + (m' + p') = m + m' + (p + p'), - by simp, - show rel_int_nat_nat (of_nat (p + p')) (m + p + (m' + p'), m + m'), - begin rw [eq], apply rel_int_nat_nat.pos end -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') := - have eq1 : m + p + m' = p + (m + m'), - by simp, - have eq2 : m + (m' + n' + 1) = (n' + 1) + (m + m'), - by simp, - show rel_int_nat_nat (sub_nat_nat p (n' + 1)) (m + p + m', m + (m' + n' + 1)), - begin - rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm], - apply int.rel_sub_nat_nat - end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := - have eq1 : m + (m' + p') = p' + (m + m'), - by simp, - have eq2 : (m + n + 1) + m' = (n + 1) + (m + m'), - by simp, - show rel_int_nat_nat (sub_nat_nat p' (n + 1)) (m + (m' + p'), (m + n + 1) + m'), - begin - rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm], - apply int.rel_sub_nat_nat - end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := - have eq : (m + n + 1) + (m' + n' + 1) = (m + m') + (n + n' + 1) + 1, - by simp, - show rel_int_nat_nat -[1+ (n + n' + 1)] (m + m', (m + n + 1) + (m' + n' + 1)), - begin rw [eq], apply rel_int_nat_nat.neg end - -protected lemma rel_mul : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat)) - has_mul.mul (λa b, (a.1 * b.1 + a.2 * b.2, a.1 * b.2 + a.2 * b.1)) -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := - have e : (m + p) * (m' + p') + m * m' = (m + p) * m' + m * (m' + p') + p * p', - by simp [mul_add, add_mul], - show rel_int_nat_nat (of_nat (p * p')) - ((m + p) * (m' + p') + m * m', (m + p) * m' + m * (m' + p')), - begin rw [e], exact rel_int_nat_nat.pos end -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') := - have e : (m + p) * (m' + n' + 1) + m * m' = (m + p) * m' + m * (m' + n' + 1) + (p * (n' + 1)), - by simp [mul_add, add_mul], - show rel_int_nat_nat (of_nat p * -[1+ n']) - ((m + p) * m' + m * (m' + n' + 1), (m + p) * (m' + n' + 1) + m * m'), - begin rw [e], exact int.rel_neg_of_nat end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := - have e : m * m' + (m + n + 1) * (m' + p') = m * (m' + p') + (m + n + 1) * m' + ((n + 1) * p'), - by simp [mul_add, add_mul], - show rel_int_nat_nat (-[1+ n] * of_nat p') - (m * (m' + p') + (m + n + 1) * m', m * m' + (m + n + 1) * (m' + p')), - begin rw [e], exact int.rel_neg_of_nat end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := - have e : m * m' + (m + n + 1) * (m' + n' + 1) = - m * (m' + n' + 1) + (m + n + 1) * m' + ((n + 1) * (n' + 1)), - by simp [mul_add, add_mul], - show rel_int_nat_nat (-[1+ n] * -[1+ n']) - (m * m' + (m + n + 1) * (m' + n' + 1), m * (m' + n' + 1) + (m + n + 1) * m'), - begin rw [e], exact rel_int_nat_nat.pos end - -/- - int is a ring --/ - -protected meta def transfer_core : tactic unit := do - transfer.transfer [`relator.rel_forall_of_total, `relator.rel_not, - `int.rel_eq, `int.rel_zero, `int.rel_one, - `int.rel_add, `int.rel_neg, `int.rel_mul] - -protected meta def transfer (distrib := tt) : tactic unit := -if distrib then `[int.transfer_core, simp [add_mul, mul_add]] -else `[int.transfer_core, simp] - -local attribute [simp] mul_assoc mul_comm mul_left_comm - -instance : comm_ring int := -{ add := int.add, - add_assoc := by int.transfer, - zero := int.zero, - zero_add := by int.transfer, - add_zero := by int.transfer, - neg := int.neg, - add_left_neg := by int.transfer, - add_comm := by int.transfer, - mul := int.mul, - mul_assoc := by int.transfer tt, - one := int.one, - one_mul := by int.transfer, - mul_one := by int.transfer, - left_distrib := by int.transfer tt, - right_distrib := by int.transfer tt, - mul_comm := by int.transfer} - -/- Extra instances to short-circuit type class resolution -/ -instance : has_sub int := by apply_instance -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_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 : zero_ne_one_class ℤ := -{ zero := 0, one := 1, zero_ne_one := by int.transfer } - -lemma of_nat_sub {n m : ℕ} (h : m ≤ n) : of_nat (n - m) = of_nat n - of_nat m := -show of_nat (n - m) = of_nat n + neg_of_nat m, from match m, h with -| 0, h := rfl -| succ m, h := show of_nat (n - succ m) = sub_nat_nat n (succ m), - by delta sub_nat_nat; rw sub_eq_zero_of_le h; refl -end - -lemma neg_succ_of_nat_coe' (n : ℕ) : -[1+ n] = -↑n - 1 := -by rw [sub_eq_add_neg, ← neg_add]; refl - -protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := of_nat_sub - -protected lemma sub_nat_nat_eq_coe {m n : ℕ} : sub_nat_nat m n = ↑m - ↑n := -sub_nat_nat_elim m n (λm n i, i = ↑m - ↑n) - (λi n, by simp [int.coe_nat_add]; refl) - (λi n, by simp [int.coe_nat_add, int.coe_nat_one, int.neg_succ_of_nat_eq]; - apply congr_arg; rw[add_left_comm]; simp) - -def to_nat : ℤ → ℕ +def to_nat : int → ℕ | (n : ℕ) := n | -[1+ n] := 0 -theorem to_nat_sub (m n : ℕ) : to_nat (m - n) = m - n := -by rw [← int.sub_nat_nat_eq_coe]; exact sub_nat_nat_elim m n - (λm n i, to_nat i = m - n) - (λi n, by rw [nat.add_sub_cancel_left]; refl) - (λi n, by rw [add_assoc, nat.sub_eq_zero_of_le (nat.le_add_right _ _)]; refl) +def nat_mod (m n : int) : ℕ := (m % n).to_nat --- Since mod x y is always nonnegative when y ≠ 0, we can make a nat version of it -def nat_mod (m n : ℤ) : ℕ := (m % n).to_nat +private def nonneg : int → Prop +| (of_nat _) := true +| -[1+ _] := false -theorem sign_mul_nat_abs : ∀ (a : ℤ), sign a * nat_abs a = a -| (n+1:ℕ) := one_mul _ -| 0 := rfl -| -[1+ n] := (neg_eq_neg_one_mul _).symm +protected def le (a b : int) : Prop := nonneg (b - a) + +instance : has_le int := ⟨int.le⟩ + +protected def lt (a b : int) : Prop := (a + 1) ≤ b + +instance : has_lt int := ⟨int.lt⟩ + +private def decidable_nonneg : Π (a : int), decidable (nonneg a) +| (of_nat m) := decidable.true +| -[1+ m] := decidable.false + +instance decidable_le (a b : int) : decidable (a ≤ b) := +decidable_nonneg _ + +instance decidable_lt (a b : int) : decidable (a < b) := +decidable_nonneg _ end int diff --git a/library/init/data/int/comp_lemmas.lean b/library/init/data/int/comp_lemmas.lean deleted file mode 100644 index e1ac0f9d4f..0000000000 --- a/library/init/data/int/comp_lemmas.lean +++ /dev/null @@ -1,120 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura - -Auxiliary lemmas used to compare int numerals. --/ -prelude -import init.data.int.order - -namespace int -/- Auxiliary lemmas for proving that to int numerals are different -/ - -/- 1. Lemmas for reducing the problem to the case where the numerals are positive -/ - -protected lemma ne_neg_of_ne {a b : ℤ} : a ≠ b → -a ≠ -b := -λ h₁ h₂, absurd (neg_inj h₂) h₁ - -protected lemma neg_ne_zero_of_ne {a : ℤ} : a ≠ 0 → -a ≠ 0 := -λ h₁ h₂, - have -a = -0, by rwa neg_zero, - have a = 0, from neg_inj this, - by contradiction - -protected lemma zero_ne_neg_of_ne {a : ℤ} (h : 0 ≠ a) : 0 ≠ -a := -ne.symm (int.neg_ne_zero_of_ne (ne.symm h)) - -protected lemma neg_ne_of_pos {a b : ℤ} : a > 0 → b > 0 → -a ≠ b := -λ h₁ h₂ h, -begin - rw [← h] at h₂, - exact absurd (le_of_lt h₁) (not_le_of_gt (neg_of_neg_pos h₂)) -end - -protected lemma ne_neg_of_pos {a b : ℤ} : a > 0 → b > 0 → a ≠ -b := -λ h₁ h₂, ne.symm (int.neg_ne_of_pos h₂ h₁) - -/- 2. Lemmas for proving that positive int numerals are nonneg and positive -/ - -protected lemma one_pos : (1:int) > 0 := -zero_lt_one - -protected lemma bit0_pos {a : ℤ} : a > 0 → bit0 a > 0 := -λ h, add_pos h h - -protected lemma bit1_pos {a : ℤ} : a ≥ 0 → bit1 a > 0 := -λ h, lt_add_of_le_of_pos (add_nonneg h h) zero_lt_one - -protected lemma zero_nonneg : (0:int) ≥ 0 := -le_refl 0 - -protected lemma one_nonneg : (1:int) ≥ 0 := -le_of_lt (zero_lt_one) - -protected lemma bit0_nonneg {a : ℤ} : a ≥ 0 → bit0 a ≥ 0 := -λ h, add_nonneg h h - -protected lemma bit1_nonneg {a : ℤ} : a ≥ 0 → bit1 a ≥ 0 := -λ h, le_of_lt (int.bit1_pos h) - -protected lemma nonneg_of_pos {a : ℤ} : a > 0 → a ≥ 0 := -le_of_lt - -/- 3. nat_abs auxiliary lemmas -/ - -lemma neg_succ_of_nat_lt_zero (n : ℕ) : neg_succ_of_nat n < 0 := -@lt.intro _ _ n (by simp [neg_succ_of_nat_coe, int.coe_nat_succ, int.coe_nat_add, int.coe_nat_one]) - -lemma of_nat_ge_zero (n : ℕ) : of_nat n ≥ 0 := -@le.intro _ _ n (by rw [zero_add, int.coe_nat_eq]) - -lemma of_nat_nat_abs_eq_of_nonneg : ∀ {a : ℤ}, a ≥ 0 → of_nat (nat_abs a) = a -| (of_nat n) h := rfl -| (neg_succ_of_nat n) h := absurd (neg_succ_of_nat_lt_zero n) (not_lt_of_ge h) - -lemma ne_of_nat_abs_ne_nat_abs_of_nonneg {a b : ℤ} (ha : a ≥ 0) (hb : b ≥ 0) (h : nat_abs a ≠ nat_abs b) : a ≠ b := -assume h, - have of_nat (nat_abs a) = of_nat (nat_abs b), by rwa [of_nat_nat_abs_eq_of_nonneg ha, of_nat_nat_abs_eq_of_nonneg hb], - begin injection this, contradiction end - -protected lemma ne_of_nat_ne_nonneg_case {a b : ℤ} {n m : nat} (ha : a ≥ 0) (hb : b ≥ 0) (e1 : nat_abs a = n) (e2 : nat_abs b = m) (h : n ≠ m) : a ≠ b := -have nat_abs a ≠ nat_abs b, by rwa [e1, e2], -ne_of_nat_abs_ne_nat_abs_of_nonneg ha hb this - -/- 4. Aux lemmas for pushing nat_abs inside numerals - nat_abs_zero and nat_abs_one are defined at init/data/int/basic.lean -/ - -lemma nat_abs_of_nat_core (n : ℕ) : nat_abs (of_nat n) = n := -rfl - -lemma nat_abs_of_neg_succ_of_nat (n : ℕ) : nat_abs (neg_succ_of_nat n) = nat.succ n := -rfl - -protected lemma nat_abs_add_nonneg : ∀ {a b : int}, a ≥ 0 → b ≥ 0 → nat_abs (a + b) = nat_abs a + nat_abs b -| (of_nat n) (of_nat m) h₁ h₂ := - have of_nat n + of_nat m = of_nat (n + m), from rfl, - by simp [nat_abs_of_nat_core, this] -| _ (neg_succ_of_nat m) h₁ h₂ := absurd (neg_succ_of_nat_lt_zero m) (not_lt_of_ge h₂) -| (neg_succ_of_nat n) _ h₁ h₂ := absurd (neg_succ_of_nat_lt_zero n) (not_lt_of_ge h₁) - -protected lemma nat_abs_add_neg : ∀ {a b : int}, a < 0 → b < 0 → nat_abs (a + b) = nat_abs a + nat_abs b -| (neg_succ_of_nat n) (neg_succ_of_nat m) h₁ h₂ := - have -[1+ n] + -[1+ m] = -[1+ nat.succ (n + m)], from rfl, - begin simp [nat_abs_of_neg_succ_of_nat, this, nat.succ_add, nat.add_succ] end - -protected lemma nat_abs_bit0 : ∀ (a : int), nat_abs (bit0 a) = bit0 (nat_abs a) -| (of_nat n) := int.nat_abs_add_nonneg (of_nat_ge_zero n) (of_nat_ge_zero n) -| (neg_succ_of_nat n) := int.nat_abs_add_neg (neg_succ_of_nat_lt_zero n) (neg_succ_of_nat_lt_zero n) - -protected lemma nat_abs_bit0_step {a : int} {n : nat} (h : nat_abs a = n) : nat_abs (bit0 a) = bit0 n := -begin rw [← h], apply int.nat_abs_bit0 end - -protected lemma nat_abs_bit1_nonneg {a : int} (h : a ≥ 0) : nat_abs (bit1 a) = bit1 (nat_abs a) := -show nat_abs (bit0 a + 1) = bit0 (nat_abs a) + nat_abs 1, from -by rw [int.nat_abs_add_nonneg (int.bit0_nonneg h) (le_of_lt (zero_lt_one)), int.nat_abs_bit0] - -protected lemma nat_abs_bit1_nonneg_step {a : int} {n : nat} (h₁ : a ≥ 0) (h₂ : nat_abs a = n) : nat_abs (bit1 a) = bit1 n := -begin rw [← h₂], apply int.nat_abs_bit1_nonneg h₁ end - -end int diff --git a/library/init/data/int/default.lean b/library/init/data/int/default.lean index 07e5cc3227..a6abbc610b 100644 --- a/library/init/data/int/default.lean +++ b/library/init/data/int/default.lean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.data.int.basic init.data.int.order init.data.int.comp_lemmas +import init.data.int.basic diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean deleted file mode 100644 index 115813b37e..0000000000 --- a/library/init/data/int/order.lean +++ /dev/null @@ -1,307 +0,0 @@ -/- -Copyright (c) 2016 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad - -The order relation on the integers. --/ -prelude -import init.data.int.basic init.data.ordering.basic - -namespace int - -private def nonneg (a : ℤ) : Prop := int.cases_on a (assume n, true) (assume n, false) - -protected def le (a b : ℤ) : Prop := nonneg (b - a) - -instance : has_le int := ⟨int.le⟩ - -protected def lt (a b : ℤ) : Prop := (a + 1) ≤ b - -instance : has_lt int := ⟨int.lt⟩ - -private def decidable_nonneg (a : ℤ) : decidable (nonneg a) := -int.cases_on a (assume a, decidable.true) (assume a, decidable.false) - -instance decidable_le (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _ - -instance decidable_lt (a b : ℤ) : decidable (a < b) := decidable_nonneg _ - -lemma lt_iff_add_one_le (a b : ℤ) : a < b ↔ a + 1 ≤ b := iff.refl _ - -private lemma nonneg.elim {a : ℤ} : nonneg a → ∃ n : ℕ, a = n := -int.cases_on a (assume n H, exists.intro n rfl) (assume n', false.elim) - -private lemma nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) := -int.cases_on a (assume n, or.inl trivial) (assume n, or.inr trivial) - -lemma le.intro_sub {a b : ℤ} {n : ℕ} (h : b - a = n) : a ≤ b := -show nonneg (b - a), by rw h; trivial - -lemma le.intro {a b : ℤ} {n : ℕ} (h : a + n = b) : a ≤ b := -le.intro_sub (by rw [← h]; simp) - -lemma le.dest_sub {a b : ℤ} (h : a ≤ b) : ∃ n : ℕ, b - a = n := nonneg.elim h - -lemma le.dest {a b : ℤ} (h : a ≤ b) : ∃ n : ℕ, a + n = b := -match (le.dest_sub h) with -| ⟨n, h₁⟩ := exists.intro n begin rw [← h₁, add_comm], simp end -end - -lemma le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P := -exists.elim (le.dest h) h' - -protected lemma le_total (a b : ℤ) : a ≤ b ∨ b ≤ a := -or.imp_right - (assume H : nonneg (-(b - a)), - have -(b - a) = a - b, by simp, - show nonneg (a - b), from this ▸ H) - (nonneg_or_nonneg_neg (b - a)) - -lemma coe_nat_le_coe_nat_of_le {m n : ℕ} (h : m ≤ n) : (↑m : ℤ) ≤ ↑n := -match nat.le.dest h with -| ⟨k, (hk : m + k = n)⟩ := le.intro (begin rw [← hk], reflexivity end) -end - -lemma le_of_coe_nat_le_coe_nat {m n : ℕ} (h : (↑m : ℤ) ≤ ↑n) : m ≤ n := -le.elim h (assume k, assume hk : ↑m + ↑k = ↑n, - have m + k = n, from int.coe_nat_inj ((int.coe_nat_add m k).trans hk), - nat.le.intro this) - -lemma coe_nat_le_coe_nat_iff (m n : ℕ) : (↑m : ℤ) ≤ ↑n ↔ m ≤ n := -iff.intro le_of_coe_nat_le_coe_nat coe_nat_le_coe_nat_of_le - -lemma coe_zero_le (n : ℕ) : 0 ≤ (↑n : ℤ) := -coe_nat_le_coe_nat_of_le n.zero_le - -lemma eq_coe_of_zero_le {a : ℤ} (h : 0 ≤ a) : ∃ n : ℕ, a = n := -by have t := le.dest_sub h; simp at t; exact t - -lemma eq_succ_of_zero_lt {a : ℤ} (h : 0 < a) : ∃ n : ℕ, a = n.succ := -let ⟨n, (h : ↑(1+n) = a)⟩ := le.dest h in -⟨n, by rw add_comm at h; exact h.symm⟩ - -lemma lt_add_succ (a : ℤ) (n : ℕ) : a < a + ↑(nat.succ n) := -le.intro (show a + 1 + n = a + nat.succ n, begin simp [int.coe_nat_eq], reflexivity end) - -lemma lt.intro {a b : ℤ} {n : ℕ} (h : a + nat.succ n = b) : a < b := -h ▸ lt_add_succ a n - -lemma lt.dest {a b : ℤ} (h : a < b) : ∃ n : ℕ, a + ↑(nat.succ n) = b := -le.elim h (assume n, assume hn : a + 1 + n = b, - exists.intro n begin rw [← hn, add_assoc, add_comm (1 : int)], reflexivity end) - -lemma lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(nat.succ n) = b → P) : P := -exists.elim (lt.dest h) h' - -lemma coe_nat_lt_coe_nat_iff (n m : ℕ) : (↑n : ℤ) < ↑m ↔ n < m := -begin rw [lt_iff_add_one_le, ← int.coe_nat_succ, coe_nat_le_coe_nat_iff], reflexivity end - -lemma lt_of_coe_nat_lt_coe_nat {m n : ℕ} (h : (↑m : ℤ) < ↑n) : m < n := -(coe_nat_lt_coe_nat_iff _ _).mp h - -lemma coe_nat_lt_coe_nat_of_lt {m n : ℕ} (h : m < n) : (↑m : ℤ) < ↑n := -(coe_nat_lt_coe_nat_iff _ _).mpr h - -/- show that the integers form an ordered additive group -/ - -protected lemma le_refl (a : ℤ) : a ≤ a := -le.intro (add_zero a) - -protected lemma le_trans {a b c : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := -le.elim h₁ (assume n, assume hn : a + n = b, -le.elim h₂ (assume m, assume hm : b + m = c, -begin apply le.intro, rw [← hm, ← hn, add_assoc], reflexivity end)) - -protected lemma le_antisymm {a b : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b := -le.elim h₁ (assume n, assume hn : a + n = b, -le.elim h₂ (assume m, assume hm : b + m = a, - have a + ↑(n + m) = a + 0, by rw [int.coe_nat_add, ← add_assoc, hn, hm, add_zero a], - have (↑(n + m) : ℤ) = 0, from add_left_cancel this, - have n + m = 0, from int.coe_nat_inj this, - have n = 0, from nat.eq_zero_of_add_eq_zero_right this, - show a = b, begin rw [← hn, this, int.coe_nat_zero, add_zero a] end)) - -protected lemma lt_irrefl (a : ℤ) : ¬ a < a := -assume : a < a, -lt.elim this (assume n, assume hn : a + nat.succ n = a, - have a + nat.succ n = a + 0, by rw [hn, add_zero], - have nat.succ n = 0, from int.coe_nat_inj (add_left_cancel this), - show false, from nat.succ_ne_zero _ this) - -protected lemma ne_of_lt {a b : ℤ} (h : a < b) : a ≠ b := -(assume : a = b, absurd (begin rewrite this at h, exact h end) (int.lt_irrefl b)) - -lemma le_of_lt {a b : ℤ} (h : a < b) : a ≤ b := -lt.elim h (assume n, assume hn : a + nat.succ n = b, le.intro hn) - -protected lemma lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) := -iff.intro - (assume h, ⟨le_of_lt h, int.ne_of_lt h⟩) - (assume ⟨aleb, aneb⟩, - le.elim aleb (assume n, assume hn : a + n = b, - have n ≠ 0, - from (assume : n = 0, aneb begin rw [← hn, this, int.coe_nat_zero, add_zero] end), - have n = nat.succ (nat.pred n), - from eq.symm (nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero this)), - lt.intro (begin rewrite this at hn, exact hn end))) - -lemma lt_succ (a : ℤ) : a < a + 1 := -int.le_refl (a + 1) - -protected lemma add_le_add_left {a b : ℤ} (h : a ≤ b) (c : ℤ) : c + a ≤ c + b := -le.elim h (assume n, assume hn : a + n = b, - le.intro (show c + a + n = c + b, begin rw [add_assoc, hn] end)) - -protected lemma add_lt_add_left {a b : ℤ} (h : a < b) (c : ℤ) : c + a < c + b := -iff.mpr (int.lt_iff_le_and_ne _ _) - (and.intro - (int.add_le_add_left (le_of_lt h) _) - (assume heq, int.lt_irrefl b begin rw add_left_cancel heq at h, exact h end)) - -protected lemma mul_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b := -le.elim ha (assume n, assume hn, -le.elim hb (assume m, assume hm, - le.intro (show 0 + ↑n * ↑m = a * b, begin rw [← hn, ← hm], simp [zero_add] end))) - -protected lemma mul_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := -lt.elim ha (assume n, assume hn, -lt.elim hb (assume m, assume hm, - lt.intro (show 0 + ↑(nat.succ (nat.succ n * m + n)) = a * b, - begin rw [← hn, ← hm], simp [int.coe_nat_zero], - rw [← int.coe_nat_mul], simp [nat.mul_succ, nat.succ_add] end))) - -protected lemma zero_lt_one : (0 : ℤ) < 1 := trivial - -protected lemma lt_iff_le_not_le {a b : ℤ} : a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := -begin -simp [int.lt_iff_le_and_ne], split; intro h, -{ cases h with hab hn, split, - { assumption }, - { intro hba, simp [int.le_antisymm hab hba] at *, contradiction } }, -{ cases h with hab hn, split, - { assumption }, - { intro h, simp [*] at * } } -end - -instance : decidable_linear_ordered_comm_ring int := -{ le := int.le, - le_refl := int.le_refl, - le_trans := @int.le_trans, - le_antisymm := @int.le_antisymm, - lt := int.lt, - lt_iff_le_not_le := @int.lt_iff_le_not_le, - add_le_add_left := @int.add_le_add_left, - add_lt_add_left := @int.add_lt_add_left, - zero_ne_one := zero_ne_one, - mul_nonneg := @int.mul_nonneg, - mul_pos := @int.mul_pos, - le_total := int.le_total, - zero_lt_one := int.zero_lt_one, - decidable_eq := int.decidable_eq, - decidable_le := int.decidable_le, - decidable_lt := int.decidable_lt, - ..int.comm_ring } - -instance : decidable_linear_ordered_comm_group int := -by apply_instance - -lemma eq_nat_abs_of_zero_le {a : ℤ} (h : 0 ≤ a) : a = nat_abs a := -let ⟨n, e⟩ := eq_coe_of_zero_le h in by rw e; refl - -lemma le_nat_abs {a : ℤ} : a ≤ nat_abs a := -or.elim (le_total 0 a) - (λh, by rw eq_nat_abs_of_zero_le h; refl) - (λh, le_trans h (coe_zero_le _)) - -lemma neg_succ_lt_zero (n : ℕ) : -[1+ n] < 0 := -lt_of_not_ge $ λ h, let ⟨m, h⟩ := eq_coe_of_zero_le h in by contradiction - -lemma eq_neg_succ_of_lt_zero : ∀ {a : ℤ}, a < 0 → ∃ n : ℕ, a = -[1+ n] -| (n : ℕ) h := absurd h (not_lt_of_ge (coe_zero_le _)) -| -[1+ n] h := ⟨n, rfl⟩ - -/- more facts specific to int -/ - -theorem of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial - -theorem coe_succ_pos (n : nat) : (nat.succ n : ℤ) > 0 := -coe_nat_lt_coe_nat_of_lt (nat.succ_pos _) - -theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n := -let ⟨n, h⟩ := eq_coe_of_zero_le (neg_nonneg_of_nonpos H) in -⟨n, eq_neg_of_eq_neg h.symm⟩ - -theorem nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : (nat_abs a : ℤ) = a := -match a, eq_coe_of_zero_le H with ._, ⟨n, rfl⟩ := rfl end - -theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : (nat_abs a : ℤ) = -a := -by rw [← nat_abs_neg, nat_abs_of_nonneg (neg_nonneg_of_nonpos H)] - -theorem abs_eq_nat_abs : ∀ a : ℤ, abs 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 (abs a) = nat_abs a := -by rw [abs_eq_nat_abs]; refl - -theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b := H - -theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := H - -theorem lt_add_one_of_le {a b : ℤ} (H : a ≤ b) : a < b + 1 := -add_le_add_right H 1 - -theorem le_of_lt_add_one {a b : ℤ} (H : a < b + 1) : a ≤ b := -le_of_add_le_add_right H - -theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b := -sub_right_lt_of_lt_add $ lt_add_one_of_le H - -theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b := -le_of_lt_add_one $ lt_add_of_sub_right_lt H - -theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 := -le_sub_right_of_add_le H - -theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := -add_le_of_le_sub_right H - -theorem sign_of_succ (n : nat) : sign (nat.succ n) = 1 := rfl - -theorem sign_eq_one_of_pos {a : ℤ} (h : 0 < a) : sign a = 1 := -match a, eq_succ_of_zero_lt h with ._, ⟨n, rfl⟩ := rfl end - -theorem sign_eq_neg_one_of_neg {a : ℤ} (h : a < 0) : sign a = -1 := -match a, eq_neg_succ_of_lt_zero h with ._, ⟨n, rfl⟩ := rfl end - -lemma eq_zero_of_sign_eq_zero : Π {a : ℤ}, sign a = 0 → a = 0 -| 0 _ := rfl - -theorem pos_of_sign_eq_one : ∀ {a : ℤ}, sign a = 1 → 0 < a -| (n+1:ℕ) _ := coe_nat_lt_coe_nat_of_lt (nat.succ_pos _) - -theorem neg_of_sign_eq_neg_one : ∀ {a : ℤ}, sign a = -1 → a < 0 -| (n+1:ℕ) h := match h with end -| 0 h := match h with end -| -[1+ n] _ := neg_succ_lt_zero _ - -theorem sign_eq_one_iff_pos (a : ℤ) : sign a = 1 ↔ 0 < a := -⟨pos_of_sign_eq_one, sign_eq_one_of_pos⟩ - -theorem sign_eq_neg_one_iff_neg (a : ℤ) : sign a = -1 ↔ a < 0 := -⟨neg_of_sign_eq_neg_one, sign_eq_neg_one_of_neg⟩ - -theorem sign_eq_zero_iff_zero (a : ℤ) : sign a = 0 ↔ a = 0 := -⟨eq_zero_of_sign_eq_zero, λ h, by rw [h, sign_zero]⟩ - -theorem sign_mul_abs (a : ℤ) : sign a * abs a = a := -by rw [abs_eq_nat_abs, sign_mul_nat_abs] - -theorem eq_one_of_mul_eq_self_left {a b : ℤ} (Hpos : a ≠ 0) (H : b * a = a) : b = 1 := -eq_of_mul_eq_mul_right Hpos (by rw [one_mul, H]) - -theorem eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 := -eq_of_mul_eq_mul_left Hpos (by rw [mul_one, H]) - -end int