From 53f486835e66929a5febb40112fff7cce8d77c7c Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 26 Dec 2014 16:57:10 -0500 Subject: [PATCH] fix(library/data/nat/order): delete unused material at end of file --- library/data/int/order.lean | 528 ------------------------------------ 1 file changed, 528 deletions(-) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 24007321f..1c21ce864 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -481,532 +481,4 @@ calc of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg ... = -a : of_nat_nat_abs_of_nonneg H1 -exit - - - - - - - - - - - --- ### interaction with add - -theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n := -le.intro (eq.refl (a + n)) - -theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a := -le.intro (add.comm a n) - - -theorem add_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a + c ≤ b + c := -add.comm c b ▸ add.comm c a ▸ add_le_add_left H c - -theorem add_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : c ≤ d) : a + c ≤ b + d := -le_trans (add_le_right H1 c) (add_le_add_left H2 b) - -theorem add_le_cancel_right {a b c : ℤ} (H : a + c ≤ b + c) : a ≤ b := -have H1 : a + c + -c ≤ b + c + -c, from add_le_right H (-c), -!add_neg_cancel_right ▸ !add_neg_cancel_right ▸ H1 - -theorem add_le_cancel_left {a b c : ℤ} (H : c + a ≤ c + b) : a ≤ b := -add_le_cancel_right (add.comm c b ▸ add.comm c a ▸ H) - -theorem add_le_inv {a b c d : ℤ} (H1 : a + b ≤ c + d) (H2 : c ≤ a) : b ≤ d := -obtain (n : ℕ) (Hn : c + n = a), from le.elim H2, -have H3 : c + (n + b) ≤ c + d, from add.assoc c n b ▸ Hn⁻¹ ▸ H1, -have H4 : n + b ≤ d, from add_le_cancel_left H3, -show b ≤ d, from le_trans (le_add_of_nat_left b n) H4 - -theorem le_add_of_nat_right_trans {a b : ℤ} (H : a ≤ b) (n : ℕ) : a ≤ b + n := -le_trans H (le_add_of_nat_right b n) - -theorem le_imp_succ_le_or_eq {a b : ℤ} (H : a ≤ b) : a + 1 ≤ b ∨ a = b := -obtain (n : ℕ) (Hn : a + n = b), from le.elim H, -discriminate - (assume H2 : n = 0, - have H3 : a = b, from - calc - a = a + 0 : (add_zero a)⁻¹ - ... = a + n : {H2⁻¹} - ... = b : Hn, - or.inr H3) - (take k : ℕ, - assume H2 : n = succ k, - have H3 : a + 1 + k = b, from - calc - a + 1 + k = a + succ k : by simp - ... = a + n : by simp - ... = b : Hn, - or.inl (le.intro H3)) - --- ### interaction with neg and sub - -theorem le_neg {a b : ℤ} (H : a ≤ b) : -b ≤ -a := -obtain (n : ℕ) (Hn : a + n = b), from le.elim H, -have H2 : b - n = a, from (iff.mp !add_eq_iff_eq_add_neg Hn)⁻¹, -have H3 : -b + n = -a, from - calc - -b + n = -b + -(-n) : {(neg_neg n)⁻¹} - ... = -(b + -n) : (neg_add_distrib b (-n))⁻¹ - ... = -a : {H2}, -le.intro H3 - -theorem neg_le_zero {a : ℤ} (H : 0 ≤ a) : -a ≤ 0 := -neg_zero ▸ (le_neg H) - -theorem zero_le_neg {a : ℤ} (H : a ≤ 0) : 0 ≤ -a := -neg_zero ▸ (le_neg H) - -theorem le_neg_inv {a b : ℤ} (H : -a ≤ -b) : b ≤ a := -neg_neg b ▸ neg_neg a ▸ le_neg H - -theorem le_sub_of_nat (a : ℤ) (n : ℕ) : a - n ≤ a := -le.intro (neg_add_cancel_right a n) - -theorem sub_le_right {a b : ℤ} (H : a ≤ b) (c : ℤ) : a - c ≤ b - c := -add_le_right H _ - -theorem sub_le_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c - b ≤ c - a := -add_le_add_left (le_neg H) _ - -theorem sub_le {a b c d : ℤ} (H1 : a ≤ b) (H2 : d ≤ c) : a - c ≤ b - d := -add_le H1 (le_neg H2) - -theorem sub_le_right_inv {a b c : ℤ} (H : a - c ≤ b - c) : a ≤ b := -add_le_cancel_right H - -theorem sub_le_left_inv {a b c : ℤ} (H : c - a ≤ c - b) : b ≤ a := -le_neg_inv (add_le_cancel_left H) - -theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a := -iff.intro - (assume H, !sub_self ▸ sub_le_right H a) - (assume H, - have H1 : a ≤ b - a + a, from zero_add a ▸ add_le_right H a, - !neg_add_cancel_right ▸ H1) - - --- Less than, Greater than, Greater than or equal --- ---------------------------------------------- - -definition ge (a b : ℤ) := b ≤ a -notation a >= b := int.ge a b -notation a ≥ b := int.ge a b - -definition gt (a b : ℤ) := b < a -notation a > b := int.gt a b - -theorem lt_def (a b : ℤ) : a < b ↔ a + 1 ≤ b := -iff.refl (a < b) - -theorem gt_def (n m : ℕ) : n > m ↔ m < n := -iff.refl (n > m) - -theorem ge_def (n m : ℕ) : n ≥ m ↔ m ≤ n := -iff.refl (n ≥ m) - --- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2 - - --- -- ### basic facts - -theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) := -of_nat_lt_of_nat m n - --- ### interaction with le - - -theorem le_imp_lt_or_eq {a b : ℤ} (H : a ≤ b) : a < b ∨ a = b := -le_imp_succ_le_or_eq H - -theorem le_ne_imp_lt {a b : ℤ} (H1 : a ≤ b) (H2 : a ≠ b) : a < b := -or_resolve_left (le_imp_lt_or_eq H1) H2 - -theorem le_imp_lt_succ {a b : ℤ} (H : a ≤ b) : a < b + 1 := -add_le_right H 1 - -theorem lt_succ_imp_le {a b : ℤ} (H : a < b + 1) : a ≤ b := -add_le_cancel_right H - - --- ### transitivity, antisymmmetry - -theorem lt_le_trans {a b c : ℤ} (H1 : a < b) (H2 : b ≤ c) : a < c := -le_trans H1 H2 - -theorem le_lt_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b < c) : a < c := -le_trans (add_le_right H1 1) H2 - -theorem lt_trans {a b c : ℤ} (H1 : a < b) (H2 : b < c) : a < c := -lt_le_trans H1 (le_of_lt H2) - -theorem le_imp_not_gt {a b : ℤ} (H : a ≤ b) : ¬ a > b := -(assume H2 : a > b, absurd (le_lt_trans H H2) (lt.irrefl a)) - -theorem lt_imp_not_ge {a b : ℤ} (H : a < b) : ¬ a ≥ b := -(assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt.irrefl a)) - -theorem lt_antisym {a b : ℤ} (H : a < b) : ¬ b < a := -le_imp_not_gt (le_of_lt H) - --- ### interaction with addition - --- TODO: note: no longer works without the "show" -theorem add_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b := -show (c + a) + 1 ≤ c + b, from (add.assoc c a 1)⁻¹ ▸ add_le_add_left H c - -theorem add_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a + c < b + c := -add.comm c b ▸ add.comm c a ▸ add_lt_left H c - -theorem add_le_lt {a b c d : ℤ} (H1 : a ≤ c) (H2 : b < d) : a + b < c + d := -le_lt_trans (add_le_right H1 b) (add_lt_left H2 c) - -theorem add_lt_le {a b c d : ℤ} (H1 : a < c) (H2 : b ≤ d) : a + b < c + d := -lt_le_trans (add_lt_right H1 b) (add_le_add_left H2 c) - -theorem add_lt {a b c d : ℤ} (H1 : a < c) (H2 : b < d) : a + b < c + d := -add_lt_le H1 (le_of_lt H2) - -theorem add_lt_cancel_left {a b c : ℤ} (H : c + a < c + b) : a < b := -show a + 1 ≤ b, from add_le_cancel_left (add.assoc c a 1 ▸ H) - -theorem add_lt_cancel_right {a b c : ℤ} (H : a + c < b + c) : a < b := -add_lt_cancel_left (add.comm b c ▸ add.comm a c ▸ H) - --- ### interaction with neg and sub - -theorem lt_neg {a b : ℤ} (H : a < b) : -b < -a := -have H2 : -(a + 1) + 1 = -a, by simp, -have H3 : -b ≤ -(a + 1), from le_neg H, -have H4 : -b + 1 ≤ -(a + 1) + 1, from add_le_right H3 1, -H2 ▸ H4 - -theorem neg_lt_zero {a : ℤ} (H : 0 < a) : -a < 0 := -neg_zero ▸ lt_neg H - -theorem zero_lt_neg {a : ℤ} (H : a < 0) : 0 < -a := -neg_zero ▸ lt_neg H - -theorem lt_neg_inv {a b : ℤ} (H : -a < -b) : b < a := -neg_neg b ▸ neg_neg a ▸ lt_neg H - -theorem lt_sub_of_nat_succ (a : ℤ) (n : ℕ) : a - succ n < a := -lt.intro (neg_add_cancel_right a (succ n)) - -theorem sub_lt_right {a b : ℤ} (H : a < b) (c : ℤ) : a - c < b - c := -add_lt_right H _ - -theorem sub_lt_left {a b : ℤ} (H : a < b) (c : ℤ) : c - b < c - a := -add_lt_left (lt_neg H) _ - -theorem sub_lt {a b c d : ℤ} (H1 : a < b) (H2 : d < c) : a - c < b - d := -add_lt H1 (lt_neg H2) - -theorem sub_lt_right_inv {a b c : ℤ} (H : a - c < b - c) : a < b := -add_lt_cancel_right H - -theorem sub_lt_left_inv {a b c : ℤ} (H : c - a < c - b) : b < a := -lt_neg_inv (add_lt_cancel_left H) - --- ### totality of lt and le - --- add_rewrite succ_pos zero_le --move some of these to nat.lean --- add_rewrite le_of_nat lt_of_nat gt_of_nat --remove gt_of_nat in Lean 0.2 --- add_rewrite le_neg lt_neg neg_le_zero zero_le_neg zero_lt_neg neg_lt_zero - -theorem neg_le_pos (n m : ℕ) : -n ≤ m := -have H1 : of_nat 0 ≤ of_nat m, by simp, -have H2 : -n ≤ 0, by simp, -le_trans H2 H1 - -theorem le_or_gt (a b : ℤ) : a ≤ b ∨ a > b := -by_cases_of_nat a - (take n : ℕ, - by_cases_of_nat_succ b - (take m : ℕ, - show of_nat n ≤ m ∨ of_nat n > m, from - proof - or.elim (@nat.le_or_gt n m) - (assume H : n ≤ m, or.inl (iff.mp' !of_nat_le_of_nat H)) - (assume H : n > m, or.inr (iff.mp' !of_nat_lt_of_nat H)) - qed) - (take m : ℕ, - show n ≤ -succ m ∨ n > -succ m, from - have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ lt_succ m), - have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n), - or.inr H)) - (take n : ℕ, - by_cases_of_nat_succ b - (take m : ℕ, - show -n ≤ m ∨ -n > m, from - or.inl (neg_le_pos n m)) - (take m : ℕ, - show -n ≤ -succ m ∨ -n > -succ m, from - or_of_or_of_imp_of_imp le_or_gt - (assume H : succ m ≤ n, - le_neg (iff.elim_left (iff.symm (of_nat_le_of_nat (succ m) n)) H)) - (assume H : succ m > n, - lt_neg (iff.elim_left (iff.symm (of_nat_lt_of_nat n (succ m))) H)))) - -theorem trichotomy_alt (a b : ℤ) : (a < b ∨ a = b) ∨ a > b := -or_of_or_of_imp_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H) - -theorem trichotomy (a b : ℤ) : a < b ∨ a = b ∨ a > b := -iff.elim_left or.assoc (trichotomy_alt a b) - -theorem le_total (a b : ℤ) : a ≤ b ∨ b ≤ a := -or_of_or_of_imp_right (le_or_gt a b) (assume H : b < a, le_of_lt H) - -theorem not_le_of_lt {a b : ℤ} (H : ¬ a < b) : b ≤ a := -or_resolve_left (le_or_gt b a) H - -theorem not_le_imp_lt {a b : ℤ} (H : ¬ a ≤ b) : b < a := -or_resolve_right (le_or_gt a b) H - --- (non)positivity and (non)negativity --- ------------------------------------- - --- ### basic - --- see also "int_by_cases" and similar theorems - -theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n := -obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le.elim H, -exists.intro n (Hn⁻¹ ⬝ zero_add n) - -theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n := -have H2 : -a ≥ 0, from zero_le_neg H, -obtain (n : ℕ) (Hn : -a = n), from pos_imp_exists_nat H2, -have H3 : a = -n, from (eq_neg_of_eq_neg (Hn⁻¹)), -exists.intro n H3 - -theorem nat_abs_nonneg_eq {a : ℤ} (H : a ≥ 0) : (nat_abs a) = a := -obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H, -Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n) - -theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 := -iff.mp (iff.symm !of_nat_le_of_nat) !zero_le - -definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _ -definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _ -definition gt_decidable [instance] {a b : ℤ} : decidable (a > b) := _ - ---nat_abs_neg is already taken... rename? -theorem nat_abs_negative {a : ℤ} (H : a ≤ 0) : (nat_abs a) = -a := -obtain (n : ℕ) (Hn : a = -n), from neg_imp_exists_nat H, -calc - (nat_abs a) = (nat_abs (-n)) : {Hn} - ... = (nat_abs n) : nat_abs_neg - ... = n : {nat_abs_of_nat n} - ... = -a : (eq_neg_of_eq_neg Hn)⁻¹ - -theorem nat_abs_cases (a : ℤ) : a = (nat_abs a) ∨ a = - (nat_abs a) := -or_of_or_of_imp_of_imp (le_total 0 a) - (assume H : a ≥ 0, (nat_abs_nonneg_eq H)⁻¹) - (assume H : a ≤ 0, (eq_neg_of_eq_neg (nat_abs_negative H))) - --- ### interaction of mul with le and lt - -theorem mul_le_left_nonneg {a b c : ℤ} (Ha : a ≥ 0) (H : b ≤ c) : a * b ≤ a * c := -obtain (n : ℕ) (Hn : b + n = c), from le.elim H, -have H2 : a * b + of_nat ((nat_abs a) * n) = a * c, from - calc - a * b + of_nat ((nat_abs a) * n) = a * b + (nat_abs a) * of_nat n : by simp - ... = a * b + a * n : {nat_abs_nonneg_eq Ha} - ... = a * (b + n) : by simp - ... = a * c : by simp, -le.intro H2 - -theorem mul_le_right_nonneg {a b c : ℤ} (Hb : b ≥ 0) (H : a ≤ c) : a * b ≤ c * b := -!mul.comm ▸ !mul.comm ▸ mul_le_left_nonneg Hb H - -theorem mul_le_left_nonpos {a b c : ℤ} (Ha : a ≤ 0) (H : b ≤ c) : a * c ≤ a * b := -have H2 : -a * b ≤ -a * c, from mul_le_left_nonneg (zero_le_neg Ha) H, -have H3 : -(a * b) ≤ -(a * c), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H2, -le_neg_inv H3 - -theorem mul_le_right_nonpos {a b c : ℤ} (Hb : b ≤ 0) (H : c ≤ a) : a * b ≤ c * b := -!mul.comm ▸ !mul.comm ▸ mul_le_left_nonpos Hb H - ----this theorem can be made more general by replacing either Ha with 0 ≤ a or Hb with 0 ≤ d... -theorem mul_le_nonneg {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b ≤ d) - : a * b ≤ c * d := -le_trans (mul_le_right_nonneg Hb Hc) (mul_le_left_nonneg (le_trans Ha Hc) Hd) - -theorem mul_le_nonpos {a b c d : ℤ} (Ha : a ≤ 0) (Hb :b ≤ 0) (Hc : c ≤ a) (Hd : d ≤ b) - : a * b ≤ c * d := -le_trans (mul_le_right_nonpos Hb Hc) (mul_le_left_nonpos (le_trans Hc Ha) Hd) - -theorem mul_lt_left_pos {a b c : ℤ} (Ha : a > 0) (H : b < c) : a * b < a * c := -have H2 : a * b < a * b + a, from add_zero (a * b) ▸ add_lt_left Ha (a * b), -have H3 : a * b + a ≤ a * c, from (by simp) ▸ mul_le_left_nonneg (le_of_lt Ha) H, -lt_le_trans H2 H3 - -theorem mul_lt_right_pos {a b c : ℤ} (Hb : b > 0) (H : a < c) : a * b < c * b := -mul.comm b c ▸ mul.comm b a ▸ mul_lt_left_pos Hb H - -theorem mul_lt_left_neg {a b c : ℤ} (Ha : a < 0) (H : b < c) : a * c < a * b := -have H2 : -a * b < -a * c, from mul_lt_left_pos (zero_lt_neg Ha) H, -have H3 : -(a * b) < -(a * c), from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_mul_eq_neg_mul⁻¹ ▸ H2, -lt_neg_inv H3 - -theorem mul_lt_right_neg {a b c : ℤ} (Hb : b < 0) (H : c < a) : a * b < c * b := -!mul.comm ▸ !mul.comm ▸ mul_lt_left_neg Hb H - -theorem mul_le_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b ≥ 0) (Hc : a ≤ c) (Hd : b < d) - : a * b < c * d := -le_lt_trans (mul_le_right_nonneg Hb Hc) (mul_lt_left_pos (lt_le_trans Ha Hc) Hd) - -theorem mul_lt_le_pos {a b c d : ℤ} (Ha : a ≥ 0) (Hb : b > 0) (Hc : a < c) (Hd : b ≤ d) - : a * b < c * d := -lt_le_trans (mul_lt_right_pos Hb Hc) (mul_le_left_nonneg (le_trans Ha (le_of_lt Hc)) Hd) - -theorem mul_lt_pos {a b c d : ℤ} (Ha : a > 0) (Hb : b > 0) (Hc : a < c) (Hd : b < d) - : a * b < c * d := -mul_lt_le_pos (le_of_lt Ha) Hb Hc (le_of_lt Hd) - -theorem mul_lt_neg {a b c d : ℤ} (Ha : a < 0) (Hb : b < 0) (Hc : c < a) (Hd : d < b) - : a * b < c * d := -lt_trans (mul_lt_right_neg Hb Hc) (mul_lt_left_neg (lt_trans Hc Ha) Hd) - --- theorem mul_le_lt_neg and mul_lt_le_neg? - -theorem mul_lt_cancel_left_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : c * a < c * b) : a < b := -or.elim (le_or_gt b a) - (assume H2 : b ≤ a, - have H3 : c * b ≤ c * a, from mul_le_left_nonneg Hc H2, - absurd H3 (lt_imp_not_ge H)) - (assume H2 : a < b, H2) - -theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b := -mul_lt_cancel_left_nonneg Hc (mul.comm b c ▸ mul.comm a c ▸ H) - -theorem mul_lt_cancel_left_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : c * b < c * a) : a < b := -have H2 : -(c * a) < -(c * b), from lt_neg H, -have H3 : -c * a < -c * b, from !neg_mul_eq_neg_mul ▸ !neg_mul_eq_neg_mul ▸ H2, -have H4 : -c ≥ 0, from zero_le_neg Hc, -mul_lt_cancel_left_nonneg H4 H3 - -theorem mul_lt_cancel_right_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : b * c < a * c) : a < b := -mul_lt_cancel_left_nonpos Hc (!mul.comm ▸ !mul.comm ▸ H) - -theorem mul_le_cancel_left_pos {a b c : ℤ} (Hc : c > 0) (H : c * a ≤ c * b) : a ≤ b := -or.elim (le_or_gt a b) - (assume H2 : a ≤ b, H2) - (assume H2 : a > b, - have H3 : c * a > c * b, from mul_lt_left_pos Hc H2, - absurd H3 (le_imp_not_gt H)) - -theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b := -mul_le_cancel_left_pos Hc (!mul.comm ▸ !mul.comm ▸ H) - -theorem mul_le_cancel_left_neg {a b c : ℤ} (Hc : c < 0) (H : c * b ≤ c * a) : a ≤ b := -have H2 : -(c * a) ≤ -(c * b), from le_neg H, -have H3 : -c * a ≤ -c * b, - from neg_mul_eq_neg_mul c b ▸ neg_mul_eq_neg_mul c a ▸ H2, -have H4 : -c > 0, from zero_lt_neg Hc, -mul_le_cancel_left_pos H4 H3 - -theorem mul_le_cancel_right_neg {a b c : ℤ} (Hc : c < 0) (H : b * c ≤ a * c) : a ≤ b := -mul_le_cancel_left_neg Hc (!mul.comm ▸ !mul.comm ▸ H) - -theorem mul_eq_one_left {a b : ℤ} (H : a * b = 1) : a = 1 ∨ a = - 1 := -have H2 : (nat_abs a) * (nat_abs b) = 1, from - calc - (nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : !mul_nat_abs⁻¹ - ... = (nat_abs 1) : {H} - ... = 1 : nat_abs_of_nat 1, -have H3 : (nat_abs a) = 1, from mul_eq_one_left H2, -or_of_or_of_imp_of_imp (nat_abs_cases a) - (assume H4 : a = (nat_abs a), H3 ▸ H4) - (assume H4 : a = - (nat_abs a), H3 ▸ H4) - -theorem mul_eq_one_right {a b : ℤ} (H : a * b = 1) : b = 1 ∨ b = - 1 := -mul_eq_one_left (!mul.comm ▸ H) - - --- sign function --- ------------- - -definition sign (a : ℤ) : ℤ := if a > 0 then 1 else (if a < 0 then - 1 else 0) - -theorem sign_pos {a : ℤ} (H : a > 0) : sign a = 1 := -if_pos H - -theorem sign_negative {a : ℤ} (H : a < 0) : sign a = - 1 := -if_neg (lt_antisym H) ⬝ if_pos H - -theorem sign_zero : sign 0 = 0 := -if_neg (lt.irrefl 0) ⬝ if_neg (lt.irrefl 0) - --- add_rewrite sign_negative sign_pos nat_abs_negative nat_abs_nonneg_eq sign_zero mul_nat_abs - -theorem mul_sign_nat_abs (a : ℤ) : sign a * (nat_abs a) = a := -have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, le_of_lt, -have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, le_of_lt, -or.elim3 (trichotomy a 0) - (assume H : a < 0, by simp) - (assume H : a = 0, by simp) - (assume H : a > 0, by simp) - --- TODO: show decidable for equality (and avoid classical library) -theorem sign_mul (a b : ℤ) : sign (a * b) = sign a * sign b := -or.elim (em (a = 0)) - (assume Ha : a = 0, by simp) - (assume Ha : a ≠ 0, - or.elim (em (b = 0)) - (assume Hb : b = 0, by simp) - (assume Hb : b ≠ 0, - have H : sign (a * b) * (nat_abs (a * b)) = sign a * sign b * (nat_abs (a * b)), from - calc - sign (a * b) * (nat_abs (a * b)) = a * b : mul_sign_nat_abs (a * b) - ... = sign a * (nat_abs a) * b : {(mul_sign_nat_abs a)⁻¹} - ... = sign a * (nat_abs a) * (sign b * (nat_abs b)) : {(mul_sign_nat_abs b)⁻¹} - ... = sign a * sign b * (nat_abs (a * b)) : by simp, - have H2 : (nat_abs (a * b)) ≠ 0, from - take H2', mul_ne_zero Ha Hb (nat_abs_eq_zero H2'), - have H3 : (nat_abs (a * b)) ≠ of_nat 0, from mt of_nat_inj H2, - mul.cancel_right H3 H)) - -theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a := -have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (of_nat_lt_of_nat 0 1)) !succ_pos, - --this should be done with simp -or.elim3 (trichotomy a 0) sorry sorry sorry --- (by simp) --- (by simp) --- (by simp) - -theorem sign_succ (n : ℕ) : sign (succ n) = 1 := -sign_pos (iff.elim_left (iff.symm (of_nat_lt_of_nat 0 (succ n))) !succ_pos) - --this should be done with simp - -theorem sign_neg (a : ℤ) : sign (-a) = - sign a := -have temp1 : a > 0 → -a < 0, from neg_lt_zero, -have temp2 : a < 0 → -a > 0, from zero_lt_neg, -or.elim3 (trichotomy a 0) sorry sorry sorry --- (by simp) --- (by simp) --- (by simp) - --- add_rewrite sign_neg - -theorem nat_abs_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (nat_abs (sign a)) = 1 := -or.elim3 (trichotomy a 0) sorry --- (by simp) - (assume H2 : a = 0, absurd H2 H) - sorry --- (by simp) - -theorem sign_nat_abs (a : ℤ) : sign (nat_abs a) = nat_abs (sign a) := -have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, le_of_lt, -have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, le_of_lt, -or.elim3 (trichotomy a 0) sorry sorry sorry --- (by simp) --- (by simp) --- (by simp) - end int