diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 4caf59b4a5..489e38d4a2 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -332,6 +332,12 @@ section (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply H₂) (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply H₁) + theorem le_max_left_iff_true [simp] (a b : A) : a ≤ max a b ↔ true := + iff_true_intro (le_max_left a b) + + theorem le_max_right_iff_true [simp] (a b : A) : b ≤ max a b ↔ true := + iff_true_intro (le_max_right a b) + /- these are also proved for lattices, but with inf and sup in place of min and max -/ theorem eq_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) (H₃ : ∀{d}, d ≤ a → d ≤ b → d ≤ c) : diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 6f2526315d..d93101e7c4 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -185,8 +185,7 @@ eq_zero_of_add_eq_zero_right (!nat.add_comm ⬝ H) theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H) -theorem add_one [simp] (n : ℕ) : n + 1 = succ n := -!nat.add_zero ▸ !add_succ +theorem add_one [simp] (n : ℕ) : n + 1 = succ n := rfl theorem one_add (n : ℕ) : 1 + n = succ n := !nat.zero_add ▸ !succ_add diff --git a/library/data/nat/fact.lean b/library/data/nat/fact.lean index 6ddc99f0c3..c915f7f456 100644 --- a/library/data/nat/fact.lean +++ b/library/data/nat/fact.lean @@ -51,6 +51,6 @@ begin {transitivity (fact n), exact ih (le_of_lt_succ h₂), rewrite [fact_succ, -one_mul at {1}], - exact mul_le_mul (succ_le_succ (zero_le n)) !le.refl}} + exact nat.mul_le_mul (succ_le_succ (zero_le n)) !le.refl}} end end nat diff --git a/library/data/nat/find.lean b/library/data/nat/find.lean index 3a9c859e1b..782840b013 100644 --- a/library/data/nat/find.lean +++ b/library/data/nat/find.lean @@ -11,7 +11,7 @@ choose {p : nat → Prop} [d : decidable_pred p] : (∃ x, p x) → nat choose_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) -/ import data.nat.basic data.nat.order -open nat subtype decidable well_founded +open nat subtype decidable well_founded algebra namespace nat section find_x @@ -46,7 +46,7 @@ acc.intro x (λ (y : nat) (l : y ≺ x), (suppose y = succ x, by substvars; assumption) (suppose y ≠ succ x, have x < y, from and.elim_left l, - have succ x < y, from lt_of_le_and_ne this (ne.symm `y ≠ succ x`), + have succ x < y, from lt_of_le_of_ne this (ne.symm `y ≠ succ x`), acc.inv h (and.intro this (and.elim_right l)))) private lemma acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y := @@ -61,7 +61,7 @@ private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gt assert acc gtb x, from acc_of_acc_succ asx, by_cases (suppose y = x, by substvars; assumption) - (suppose y ≠ x, acc_of_acc_of_lt `acc gtb x` (lt_of_le_and_ne (le_of_lt_succ yltsx) this)) + (suppose y ≠ x, acc_of_acc_of_lt `acc gtb x` (lt_of_le_of_ne (le_of_lt_succ yltsx) this)) parameter (ex : ∃ a, p a) parameter [dp : decidable_pred p] diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 5ab8328bc2..79b4d31676 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -12,22 +12,22 @@ namespace nat /- lt and le -/ -theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n := +protected theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n := le_of_eq_or_lt (or.swap H) -theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n := +protected theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n := or.swap (eq_or_lt_of_le H) -theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n := -iff.intro lt_or_eq_of_le le_of_lt_or_eq +protected theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n := +iff.intro nat.lt_or_eq_of_le nat.le_of_lt_or_eq -theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) : m ≠ n → m < n := +protected theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) : m ≠ n → m < n := or_resolve_right (eq_or_lt_of_le H1) -theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n := +protected theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n := iff.intro (take H, and.intro (le_of_lt H) (take H1, !lt.irrefl (H1 ▸ H))) - (and.rec lt_of_le_and_ne) + (and.rec nat.lt_of_le_and_ne) theorem le_add_right (n k : ℕ) : n ≤ n + k := nat.rec !le.refl (λ k, le_succ_of_le) k @@ -38,36 +38,36 @@ theorem le_add_left (n m : ℕ): n ≤ m + n := theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m := h ▸ !le_add_right -theorem le.elim {n m : ℕ} : n ≤ m → ∃k, n + k = m := +theorem le.elim {n m : ℕ} : n ≤ m → ∃ k, n + k = m := le.rec (exists.intro 0 rfl) (λm h, Exists.rec (λ k H, exists.intro (succ k) (H ▸ rfl))) -theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m := +protected theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m := or.imp_left le_of_lt !lt_or_ge /- addition -/ -theorem add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := +protected theorem add_le_add_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := obtain l Hl, from le.elim H, le.intro (Hl ▸ !add.assoc) -theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k := -!add.comm ▸ !add.comm ▸ add_le_add_left H k +protected theorem add_le_add_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k := +!add.comm ▸ !add.comm ▸ nat.add_le_add_left H k -theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m := +protected theorem le_of_add_le_add_left {k n m : ℕ} (H : k + n ≤ k + m) : n ≤ m := obtain l Hl, from le.elim H, le.intro (add.cancel_left (!add.assoc⁻¹ ⬝ Hl)) -theorem lt_of_add_lt_add_left {k n m : ℕ} (H : k + n < k + m) : n < m := +protected theorem lt_of_add_lt_add_left {k n m : ℕ} (H : k + n < k + m) : n < m := let H' := le_of_lt H in -lt_of_le_and_ne (le_of_add_le_add_left H') (assume Heq, !lt.irrefl (Heq ▸ H)) +nat.lt_of_le_and_ne (nat.le_of_add_le_add_left H') (assume Heq, !lt.irrefl (Heq ▸ H)) -theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m := -lt_of_succ_le (!add_succ ▸ add_le_add_left (succ_le_of_lt H) k) +protected theorem add_lt_add_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m := +lt_of_succ_le (!add_succ ▸ nat.add_le_add_left (succ_le_of_lt H) k) -theorem add_lt_add_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k := -!add.comm ▸ !add.comm ▸ add_lt_add_left H k +protected theorem add_lt_add_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k := +!add.comm ▸ !add.comm ▸ nat.add_lt_add_left H k -theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k := -!add_zero ▸ add_lt_add_left H n +protected theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k := +!add_zero ▸ nat.add_lt_add_left H n /- multiplication -/ @@ -79,58 +79,14 @@ le.intro this theorem mul_le_mul_right {n m : ℕ} (k : ℕ) (H : n ≤ m) : n * k ≤ m * k := !mul.comm ▸ !mul.comm ▸ !mul_le_mul_left H -theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l := -le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2) +protected theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l := +le.trans (!nat.mul_le_mul_right H1) (!nat.mul_le_mul_left H2) -theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m := -lt_of_lt_of_le (lt_add_of_pos_right Hk) (!mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H)) +protected theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m := +lt_of_lt_of_le (nat.lt_add_of_pos_right Hk) (!mul_succ ▸ nat.mul_le_mul_left k (succ_le_of_lt H)) -theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k := -!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk - -/- min and max -/ -/- -definition max (a b : ℕ) : ℕ := if a < b then b else a -definition min (a b : ℕ) : ℕ := if a < b then a else b - -theorem max_self [simp] (a : ℕ) : max a a = a := -eq.rec_on !if_t_t rfl - -theorem max_le {n m k : ℕ} (H₁ : n ≤ k) (H₂ : m ≤ k) : max n m ≤ k := -if H : n < m then by rewrite [↑max, if_pos H]; apply H₂ -else by rewrite [↑max, if_neg H]; apply H₁ - -theorem min_le_left (n m : ℕ) : min n m ≤ n := -if H : n < m then by rewrite [↑min, if_pos H] -else assert H' : m ≤ n, from or_resolve_right !lt_or_ge H, - by rewrite [↑min, if_neg H]; apply H' - -theorem min_le_right (n m : ℕ) : min n m ≤ m := -if H : n < m then by rewrite [↑min, if_pos H]; apply le_of_lt H -else assert H' : m ≤ n, from or_resolve_right !lt_or_ge H, - by rewrite [↑min, if_neg H] - -theorem le_min {n m k : ℕ} (H₁ : k ≤ n) (H₂ : k ≤ m) : k ≤ min n m := -if H : n < m then by rewrite [↑min, if_pos H]; apply H₁ -else by rewrite [↑min, if_neg H]; apply H₂ - -theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b := -(if_pos H)⁻¹ - -theorem eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b := -(if_neg H)⁻¹ - -open decidable -theorem le_max_right (a b : ℕ) : b ≤ max a b := -lt.by_cases - (suppose a < b, (eq_max_right this) ▸ !le.refl) - (suppose a = b, this ▸ !max_self⁻¹ ▸ !le.refl) - (suppose b < a, (eq_max_left (lt.asymm this)) ▸ (le_of_lt this)) - -theorem le_max_left (a b : ℕ) : a ≤ max a b := -if h : a < b then le_of_lt (eq.rec_on (eq_max_right h) h) -else (eq_max_left h) ▸ !le.refl --/ +protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k := +!mul.comm ▸ !mul.comm ▸ nat.mul_lt_mul_of_pos_left H Hk /- nat is an instance of a linearly ordered semiring and a lattice -/ @@ -147,20 +103,20 @@ algebra.decidable_linear_ordered_semiring nat := le_trans := @le.trans, le_antisymm := @le.antisymm, le_total := @le.total, - le_iff_lt_or_eq := @le_iff_lt_or_eq, + le_iff_lt_or_eq := @nat.le_iff_lt_or_eq, le_of_lt := @le_of_lt, lt_irrefl := @lt.irrefl, lt_of_lt_of_le := @lt_of_lt_of_le, lt_of_le_of_lt := @lt_of_le_of_lt, - lt_of_add_lt_add_left := @lt_of_add_lt_add_left, - add_lt_add_left := @add_lt_add_left, - add_le_add_left := @add_le_add_left, - le_of_add_le_add_left := @le_of_add_le_add_left, + lt_of_add_lt_add_left := @nat.lt_of_add_lt_add_left, + add_lt_add_left := @nat.add_lt_add_left, + add_le_add_left := @nat.add_le_add_left, + le_of_add_le_add_left := @nat.le_of_add_le_add_left, zero_lt_one := zero_lt_succ 0, - mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1), - mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1), - mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left, - mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right, + mul_le_mul_of_nonneg_left := (take a b c H1 H2, nat.mul_le_mul_left c H1), + mul_le_mul_of_nonneg_right := (take a b c H1 H2, nat.mul_le_mul_right c H1), + mul_lt_mul_of_pos_left := @nat.mul_lt_mul_of_pos_left, + mul_lt_mul_of_pos_right := @nat.mul_lt_mul_of_pos_right, decidable_lt := nat.decidable_lt ⦄ @@ -365,7 +321,7 @@ or.elim (le_or_gt n 1) show n = 1, from le.antisymm `n ≤ 1` (succ_le_of_lt this)) (suppose n > 1, have m > 0, from pos_of_mul_pos_left H2, - have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt `n > 1`) (succ_le_of_lt this), + have n * m ≥ 2 * 1, from nat.mul_le_mul (succ_le_of_lt `n > 1`) (succ_le_of_lt this), have 1 ≥ 2, from !mul_one ▸ H ▸ this, absurd !lt_succ_self (not_lt_of_ge this)) @@ -386,12 +342,6 @@ dvd.elim H /- min and max -/ open decidable -theorem le_max_left_iff_true [simp] (a b : ℕ) : a ≤ max a b ↔ true := -iff_true_intro (le_max_left a b) - -theorem le_max_right_iff_true [simp] (a b : ℕ) : b ≤ max a b ↔ true := -iff_true_intro (le_max_right a b) - theorem min_zero [simp] (a : ℕ) : min a 0 = 0 := by rewrite [min_eq_right !zero_le] @@ -417,7 +367,7 @@ or.elim !lt_or_ge /- In algebra.ordered_group, these next four are only proved for additive groups, not additive semigroups. -/ -theorem min_add_add_left (a b c : ℕ) : min (a + b) (a + c) = a + min b c := +protected theorem min_add_add_left (a b c : ℕ) : min (a + b) (a + c) = a + min b c := decidable.by_cases (suppose b ≤ c, assert a + b ≤ a + c, from add_le_add_left this _, @@ -427,10 +377,10 @@ decidable.by_cases assert a + c ≤ a + b, from add_le_add_left this _, by rewrite [min_eq_right `c ≤ b`, min_eq_right this]) -theorem min_add_add_right (a b c : ℕ) : min (a + c) (b + c) = min a b + c := -by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply min_add_add_left +protected theorem min_add_add_right (a b c : ℕ) : min (a + c) (b + c) = min a b + c := +by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply nat.min_add_add_left -theorem max_add_add_left (a b c : ℕ) : max (a + b) (a + c) = a + max b c := +protected theorem max_add_add_left (a b c : ℕ) : max (a + b) (a + c) = a + max b c := decidable.by_cases (suppose b ≤ c, assert a + b ≤ a + c, from add_le_add_left this _, @@ -440,8 +390,8 @@ decidable.by_cases assert a + c ≤ a + b, from add_le_add_left this _, by rewrite [max_eq_left `c ≤ b`, max_eq_left this]) -theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c := -by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left +protected theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c := +by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply nat.max_add_add_left /- least and greatest -/ diff --git a/library/data/nat/sqrt.lean b/library/data/nat/sqrt.lean index 28b691c45a..4d35d6e6a4 100644 --- a/library/data/nat/sqrt.lean +++ b/library/data/nat/sqrt.lean @@ -67,7 +67,7 @@ private theorem le_squared : ∀ (n : nat), n ≤ n*n | 0 := !le.refl | (succ n) := have aux₁ : 1 ≤ succ n, from succ_le_succ !zero_le, - assert aux₂ : 1 * succ n ≤ succ n * succ n, from mul_le_mul aux₁ !le.refl, + assert aux₂ : 1 * succ n ≤ succ n * succ n, from nat.mul_le_mul aux₁ !le.refl, by rewrite [one_mul at aux₂]; exact aux₂ private theorem lt_squared : ∀ {n : nat}, n > 1 → n < n * n @@ -139,7 +139,7 @@ theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n have ssnesn : succ s ≠ succ n, from assume sseqsn : succ s = succ n, by rewrite [sseqsn at l₄]; exact (absurd l₄ !lt.irrefl), - have sslen : s < n, from lt_of_succ_lt_succ (lt_of_le_and_ne sslesn ssnesn), + have sslen : s < n, from lt_of_succ_lt_succ (lt_of_le_of_ne sslesn ssnesn), assert sseqn : succ s = n, from le.antisymm sslen h₂, by rewrite [sqrt_aux_succ_of_pos hl]; exact sseqn) (λ hg : ¬ (succ s)*(succ s) ≤ n*n + k, diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index 77249c1d54..c1b5d555df 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -97,7 +97,7 @@ begin {cases m with m, exact absurd rfl m_ne_0, cases m with m, exact absurd rfl m_ne_1, exact succ_le_succ (succ_le_succ (zero_le _))}, {have m_le_n : m ≤ n, from le_of_dvd (pos_of_ne_zero `n ≠ 0`) m_dvd_n, - exact lt_of_le_and_ne m_le_n m_ne_n} + exact lt_of_le_of_ne m_le_n m_ne_n} end theorem exists_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n := @@ -132,13 +132,13 @@ have p ≥ n, from by_contradiction (suppose ¬ p ≥ n, have p < n, from lt_of_not_ge this, have p ≤ n + 1, from le_of_lt (lt.step this), - have p ∣ m, from dvd_fact `p > 0` this, - have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ `p ∣ m + 1`) this, + have p ∣ m, from dvd_fact `p > 0` this, + have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ `p ∣ m + 1`) this, have p ≤ 1, from le_of_dvd zero_lt_one this, - absurd (le.trans `2 ≤ p` `p ≤ 1`) dec_trivial), + show false, from absurd (le.trans `2 ≤ p` `p ≤ 1`) dec_trivial), subtype.tag p (and.intro this `prime p`) -lemma ex_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p := +lemma exists_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p := ex_of_sub (infinite_primes n) lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=