diff --git a/library/data/fintype/function.lean b/library/data/fintype/function.lean index 5484a6276..2bf225540 100644 --- a/library/data/fintype/function.lean +++ b/library/data/fintype/function.lean @@ -7,6 +7,7 @@ Author : Haitao Zhang import data open nat function eq.ops +open - [notations] algebra namespace list -- this is in preparation for counting the number of finite functions diff --git a/library/data/hf.lean b/library/data/hf.lean index 88d16e82d..7b249f992 100644 --- a/library/data/hf.lean +++ b/library/data/hf.lean @@ -11,8 +11,8 @@ this bijection is implemeted using the Ackermann coding. -/ import data.nat data.finset.equiv data.list open nat binary -open -[notations] finset -open -[notations] algebra +open - [notations] finset +open - [notations] algebra definition hf := nat diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 06231f3fc..40bd59831 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -523,10 +523,10 @@ protected definition integral_domain [reducible] [instance] : algebra.integral_d eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄ definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int := -has_sub.mk algebra.sub +has_sub.mk has_sub.sub definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int := -has_dvd.mk algebra.dvd +has_dvd.mk has_dvd.dvd set_option pp.coercions true diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 11313c974..68ee9ff96 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -24,8 +24,8 @@ sign b * | -[1+m] := -[1+ ((m:nat) div (nat_abs b))] end) -definition int_has_divides [reducible] [instance] [priority int.prio] : has_divides int := -has_divides.mk int.divide +definition int_has_divide [reducible] [instance] [priority int.prio] : has_divide int := +has_divide.mk int.divide lemma divide_of_nat (a : nat) (b : ℤ) : (of_nat a) div b = sign b * (a div (nat_abs b) : nat) := rfl diff --git a/library/data/int/order.lean b/library/data/int/order.lean index e60a76903..63f2623ae 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -116,11 +116,11 @@ obtain (n : ℕ) (Hn : a + n = b), from le.elim H₁, obtain (m : ℕ) (Hm : b + m = a), from le.elim H₂, have a + of_nat (n + m) = a + 0, from calc - a + of_nat (n + m) = a + (of_nat n + m) : of_nat_add - ... = a + n + m : add.assoc - ... = b + m : Hn - ... = a : Hm - ... = a + 0 : add_zero, + a + of_nat (n + m) = a + (of_nat n + m) : by rewrite of_nat_add + ... = a + n + m : by rewrite add.assoc + ... = b + m : by rewrite Hn + ... = a : by rewrite Hm + ... = a + 0 : by rewrite add_zero, have of_nat (n + m) = of_nat 0, from add.left_cancel this, have n + m = 0, from of_nat.inj this, have n = 0, from nat.eq_zero_of_add_eq_zero_right this, @@ -193,11 +193,11 @@ obtain (m : ℕ) (Hm : 0 + m = b), from le.elim Hb, le.intro (eq.symm (calc - a * b = (0 + n) * b : Hn - ... = n * b : zero_add - ... = n * (0 + m) : {Hm⁻¹} - ... = n * m : zero_add - ... = 0 + n * m : zero_add)) + a * b = (0 + n) * b : by rewrite Hn + ... = n * b : by rewrite zero_add + ... = n * (0 + m) : by rewrite Hm + ... = n * m : by rewrite zero_add + ... = 0 + n * m : by rewrite zero_add)) theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b := obtain (n : ℕ) (Hn : 0 + nat.succ n = a), from lt.elim Ha, @@ -205,14 +205,14 @@ obtain (m : ℕ) (Hm : 0 + nat.succ m = b), from lt.elim Hb, lt.intro (eq.symm (calc - a * b = (0 + nat.succ n) * b : Hn - ... = nat.succ n * b : zero_add - ... = nat.succ n * (0 + nat.succ m) : {Hm⁻¹} - ... = nat.succ n * nat.succ m : zero_add - ... = of_nat (nat.succ n * nat.succ m) : of_nat_mul - ... = of_nat (nat.succ n * m + nat.succ n) : nat.mul_succ - ... = of_nat (nat.succ (nat.succ n * m + n)) : nat.add_succ - ... = 0 + nat.succ (nat.succ n * m + n) : zero_add)) + a * b = (0 + nat.succ n) * b : by rewrite Hn + ... = nat.succ n * b : by rewrite zero_add + ... = nat.succ n * (0 + nat.succ m) : by rewrite Hm + ... = nat.succ n * nat.succ m : by rewrite zero_add + ... = of_nat (nat.succ n * nat.succ m) : by rewrite of_nat_mul + ... = of_nat (nat.succ n * m + nat.succ n) : by rewrite nat.mul_succ + ... = of_nat (nat.succ (nat.succ n * m + n)) : by rewrite nat.add_succ + ... = 0 + nat.succ (nat.succ n * m + n) : by rewrite zero_add)) theorem zero_lt_one : (0 : ℤ) < 1 := trivial @@ -321,7 +321,7 @@ theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b := !sub_add_cancel ▸ add_one_le_of_lt H theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 := -le_of_lt_add_one (!sub_add_cancel⁻¹ ▸ H) +le_of_lt_add_one begin rewrite algebra.sub_add_cancel, exact H end theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := !sub_add_cancel ▸ (lt_add_one_of_le H) diff --git a/library/data/int/power.lean b/library/data/int/power.lean index aaee5291c..60418e2cf 100644 --- a/library/data/int/power.lean +++ b/library/data/int/power.lean @@ -11,7 +11,7 @@ namespace int open - [notations] algebra definition int_has_pow_nat : has_pow_nat int := -has_pow_nat.mk pow_nat +has_pow_nat.mk has_pow_nat.pow_nat /- definition nmul (n : ℕ) (a : ℤ) : ℤ := algebra.nmul n a diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 9506ab50a..80da1484a 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -20,10 +20,10 @@ and.rec (λ ypos ylex, sub_lt (lt_of_lt_of_le ypos ylex) ypos) private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero -definition divide := fix div.F +protected definition divide := fix div.F -definition nat_has_divides [reducible] [instance] [priority nat.prio] : has_divides nat := -has_divides.mk divide +definition nat_has_divide [reducible] [instance] [priority nat.prio] : has_divide nat := +has_divide.mk nat.divide theorem divide_def (x y : nat) : divide x y = if 0 < y ∧ y ≤ x then divide (x - y) y + 1 else 0 := congr_fun (fix_eq div.F x) y diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index f6f3ad56b..59cfd9e4d 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -257,6 +257,9 @@ dvd.antisymm definition coprime [reducible] (m n : ℕ) : Prop := gcd m n = 1 +lemma gcd_eq_one_of_coprime {m n : ℕ} : coprime m n → gcd m n = 1 := +λ h, h + theorem coprime_swap {m n : ℕ} (H : coprime n m) : coprime m n := !gcd.comm ▸ H diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 697917c26..40d9895ed 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -134,7 +134,7 @@ else (eq_max_left h) ▸ !le.refl /- nat is an instance of a linearly ordered semiring and a lattice -/ -open -[notations] algebra +open - [notations] algebra protected definition decidable_linear_ordered_semiring [reducible] [instance] : algebra.decidable_linear_ordered_semiring nat := @@ -165,7 +165,7 @@ algebra.decidable_linear_ordered_semiring nat := definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat := -has_dvd.mk algebra.dvd +has_dvd.mk has_dvd.dvd theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b := @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 8c1efaa9e..b9e5bb062 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -10,23 +10,22 @@ open - [notations] algebra namespace nat -definition nat_has_pow_nat : has_pow_nat nat := -has_pow_nat.mk pow_nat +definition nat_has_pow_nat [instance] [reducible] [priority nat.prio] : has_pow_nat nat := +has_pow_nat.mk has_pow_nat.pow_nat theorem pow_le_pow_of_le {x y : ℕ} (i : ℕ) (H : x ≤ y) : x^i ≤ y^i := algebra.pow_le_pow_of_le i !zero_le H - theorem eq_zero_of_pow_eq_zero {a m : ℕ} (H : a^m = 0) : a = 0 := or.elim (eq_zero_or_pos m) (suppose m = 0, - by rewrite [`m = 0` at H, pow_zero at H]; contradiction) + by krewrite [`m = 0` at H, pow_zero at H]; contradiction) (suppose m > 0, have h₁ : ∀ m, a^succ m = 0 → a = 0, begin intro m, induction m with m ih, - {rewrite pow_one; intros; assumption}, + {krewrite pow_one; intros; assumption}, rewrite pow_succ, intro H, cases eq_zero_or_eq_zero_of_mul_eq_zero H with h₃ h₄, diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 102eda8b4..387d10b08 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -289,7 +289,7 @@ sub.cases ... = k - n + n : sub_add_cancel H3, le.intro (add.cancel_right H4)) -open -[notations] algebra +open - [notations] algebra theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 := assert H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹, diff --git a/library/data/pnat.lean b/library/data/pnat.lean index 0794b55a2..9d3d0a02d 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -10,6 +10,7 @@ are those needed for that construction. -/ import data.rat.order data.nat open nat rat subtype eq.ops +open - [notations] algebra namespace pnat diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 899c930aa..1f5f6cfa2 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -102,7 +102,7 @@ structure has_inv [class] (A : Type) := (inv : A → A) structure has_neg [class] (A : Type) := (neg : A → A) structure has_sub [class] (A : Type) := (sub : A → A → A) structure has_division [class] (A : Type) := (division : A → A → A) -structure has_divides [class] (A : Type) := (divides : A → A → A) +structure has_divide [class] (A : Type) := (divide : A → A → A) structure has_modulo [class] (A : Type) := (modulo : A → A → A) structure has_dvd [class] (A : Type) := (dvd : A → A → Prop) structure has_le [class] (A : Type) := (le : A → A → Prop) @@ -112,7 +112,7 @@ definition add {A : Type} [s : has_add A] : A → A → A := has_add.add definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub definition division {A : Type} [s : has_division A] : A → A → A := has_division.division -definition divides {A : Type} [s : has_divides A] : A → A → A := has_divides.divides +definition divide {A : Type} [s : has_divide A] : A → A → A := has_divide.divide definition modulo {A : Type} [s : has_modulo A] : A → A → A := has_modulo.modulo definition dvd {A : Type} [s : has_dvd A] : A → A → Prop := has_dvd.dvd definition neg {A : Type} [s : has_neg A] : A → A := has_neg.neg @@ -126,7 +126,7 @@ infix + := add infix * := mul infix - := sub infix / := division -infix div := divides +infix div := divide infix ∣ := dvd infix mod := modulo prefix - := neg @@ -135,3 +135,14 @@ infix ≤ := le infix ≥ := ge infix < := lt infix > := gt + +notation [parsing-only] x ` +[`:65 A:0 `] `:0 y:65 := @add A _ x y +notation [parsing-only] x ` -[`:65 A:0 `] `:0 y:65 := @sub A _ x y +notation [parsing-only] x ` *[`:70 A:0 `] `:0 y:70 := @mul A _ x y +notation [parsing-only] x ` /[`:70 A:0 `] `:0 y:70 := @division A _ x y +notation [parsing-only] x ` div[`:70 A:0 `] `:0 y:70 := @divide A _ x y +notation [parsing-only] x ` mod[`:70 A:0 `] `:0 y:70 := @modulo A _ x y +notation [parsing-only] x ` ≤[`:50 A:0 `] `:0 y:50 := @le A _ x y +notation [parsing-only] x ` ≥[`:50 A:0 `] `:0 y:50 := @ge A _ x y +notation [parsing-only] x ` <[`:50 A:0 `] `:0 y:50 := @lt A _ x y +notation [parsing-only] x ` >[`:50 A:0 `] `:0 y:50 := @gt A _ x y diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 11ad148bd..0c2fbef1a 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -7,6 +7,7 @@ A proof that if n > 1 and a > 0, then the nth root of a is irrational, unless a -/ import data.rat .prime_factorization open eq.ops +open - [notations] algebra /- First, a textbook proof that sqrt 2 is irrational. -/ @@ -15,15 +16,15 @@ section theorem sqrt_two_irrational {a b : ℕ} (co : coprime a b) : a^2 ≠ 2 * b^2 := assume H : a^2 = 2 * b^2, - have even (a^2), from even_of_exists (exists.intro _ H), - have even a, from even_of_even_pow this, - obtain c (aeq : a = 2 * c), from exists_of_even this, - have 2 * (2 * c^2) = 2 * b^2, by rewrite [-H, aeq, *pow_two, mul.assoc, mul.left_comm c], - have 2 * c^2 = b^2, from eq_of_mul_eq_mul_left dec_trivial this, - have even (b^2), from even_of_exists (exists.intro _ (eq.symm this)), - have even b, from even_of_even_pow this, - have 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`), - have 2 ∣ 1, from co ▸ this, + have even (a^2), from even_of_exists (exists.intro _ H), + have even a, from even_of_even_pow this, + obtain (c : nat) (aeq : a = 2 * c), from exists_of_even this, + have 2 * (2 * c^2) = 2 * b^2, begin rewrite [-H, aeq, *pow_two, algebra.mul.assoc, algebra.mul.left_comm c] end, + have 2 * c^2 = b^2, from eq_of_mul_eq_mul_left dec_trivial this, + have even (b^2), from even_of_exists (exists.intro _ (eq.symm this)), + have even b, from even_of_even_pow this, + assert 2 ∣ gcd a b, from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`), + have 2 ∣ 1, begin rewrite [gcd_eq_one_of_coprime co at this], exact this end, show false, from absurd `2 ∣ 1` dec_trivial end @@ -41,7 +42,7 @@ section b = 1 := have bpos : b > 0, from pos_of_ne_zero (suppose b = 0, - have a^n = 0, by rewrite [H, this, zero_pow npos], + have a^n = 0, by krewrite [H, this, zero_pow npos], assert a = 0, from eq_zero_of_pow_eq_zero this, show false, from ne_of_lt `0 < a` this⁻¹), have H₁ : ∀ p, prime p → ¬ p ∣ b, from @@ -51,12 +52,12 @@ section have p ∣ a, from dvd_of_prime_of_dvd_pow `prime p` this, have ¬ coprime a b, from not_coprime_of_dvd_of_dvd (gt_one_of_prime `prime p`) `p ∣ a` `p ∣ b`, show false, from this `coprime a b`, - have b < 2, from by_contradiction + have blt2 : b < 2, from by_contradiction (suppose ¬ b < 2, have b ≥ 2, from le_of_not_gt this, obtain p [primep pdvdb], from exists_prime_and_dvd this, show false, from H₁ p primep pdvdb), - show b = 1, from (le.antisymm (le_of_lt_succ `b < 2`) (succ_le_of_lt `b > 0`)) + show b = 1, from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos)) end /- @@ -72,13 +73,13 @@ section let a := num q, b := denom q in have b ≠ 0, from ne_of_gt (denom_pos q), have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H), - have bnnz : (#rat b^n ≠ 0), from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz), - have a^n / b^n = c, using bnz, by rewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H], - have a^n = c * b^n, from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹), + have bnnz : ((b : rat)^n ≠ 0), from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz), + have a^n /[rat] b^n = c, using bnz, begin krewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H] end, + have (a^n : rat) = c *[rat] b^n, from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹), have a^n = c * b^n, -- int version using this, by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this, have (abs a)^n = abs c * (abs b)^n, - using this, by rewrite [-int.abs_pow, this, int.abs_mul, int.abs_pow], + using this, by rewrite [-abs_pow, this, abs_mul, abs_pow], have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n, using this, by apply int.of_nat.inj; rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs]; assumption, @@ -87,11 +88,19 @@ section by_cases (suppose q = 0, by rewrite this) (suppose q ≠ 0, - have a ≠ 0, from suppose a = 0, `q ≠ 0` (by rewrite [eq_num_div_denom, `a = 0`, zero_div]), - have nat_abs a ≠ 0, from suppose nat_abs a = 0, `a ≠ 0` (eq_zero_of_nat_abs_eq_zero this), + have ane0 : a ≠ 0, from + suppose aeq0 : a = 0, + have q = 0, begin rewrite eq_num_div_denom, rewrite aeq0, krewrite zero_div end, + absurd `q = 0` `q ≠ 0`, + have nat_abs a ≠ 0, from + suppose nat_abs a = 0, + have a = 0, from eq_zero_of_nat_abs_eq_zero this, + absurd `a = 0` `a ≠ 0`, show nat_abs b = 1, from (root_irrational npos (pos_of_ne_zero this) H₂ H₁)), show b = 1, using this, by rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this] + exit + theorem eq_num_pow_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) : c = (num q)^n := have denom q = 1, from denom_eq_one_of_pow_eq npos H,