fix(library/data/int,library/data/rat): int and rat
This commit is contained in:
Leonardo de Moura
parent
744d1cba3d
commit
07b33ec75e
9 changed files with 43 additions and 36 deletions
|
|
@ -18,6 +18,9 @@ section semiring
|
|||
variable [s : semiring A]
|
||||
include s
|
||||
|
||||
definition semiring_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
monoid_has_pow_nat
|
||||
|
||||
theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) :=
|
||||
have h₁ : ∀ m : nat, (0 : A)^(succ m) = (0 : A),
|
||||
begin
|
||||
|
|
@ -34,6 +37,9 @@ section integral_domain
|
|||
variable [s : integral_domain A]
|
||||
include s
|
||||
|
||||
definition integral_domain_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
monoid_has_pow_nat
|
||||
|
||||
theorem eq_zero_of_pow_eq_zero {a : A} {m : ℕ} (H : a^m = 0) : a = 0 :=
|
||||
or.elim (eq_zero_or_pos m)
|
||||
(suppose m = 0,
|
||||
|
|
@ -128,6 +134,9 @@ section decidable_linear_ordered_comm_ring
|
|||
variable [s : decidable_linear_ordered_comm_ring A]
|
||||
include s
|
||||
|
||||
definition decidable_linear_ordered_comm_ring_has_pow_nat [reducible] [instance] : has_pow_nat A :=
|
||||
monoid_has_pow_nat
|
||||
|
||||
theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n :=
|
||||
begin
|
||||
induction n with n ih,
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ private definition has_decidable_eq₂ : Π (a b : ℤ), decidable (a = b)
|
|||
| -[1+ m] -[1+ n] := if H : m = n then
|
||||
inl (congr_arg neg_succ_of_nat H) else inr (not.mto neg_succ_of_nat.inj H)
|
||||
|
||||
definition has_decidable_eq [instance] : decidable_eq ℤ := has_decidable_eq₂
|
||||
definition has_decidable_eq [instance] [priority int.prio] : decidable_eq ℤ := has_decidable_eq₂
|
||||
|
||||
theorem of_nat_add (n m : nat) : of_nat (n + m) = of_nat n + of_nat m := rfl
|
||||
|
||||
|
|
@ -501,7 +501,7 @@ theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0
|
|||
or.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero
|
||||
(eq_zero_or_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H]))
|
||||
|
||||
protected definition integral_domain [reducible] [instance] : algebra.integral_domain int :=
|
||||
protected definition integral_domain [reducible] [trans_instance] : algebra.integral_domain int :=
|
||||
⦃algebra.integral_domain,
|
||||
add := int.add,
|
||||
add_assoc := add.assoc,
|
||||
|
|
|
|||
|
|
@ -233,7 +233,7 @@ theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c :=
|
|||
(iff.mpr !lt_iff_le_and_ne) (and.intro Hac
|
||||
(assume Heq, not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab))
|
||||
|
||||
protected definition linear_ordered_comm_ring [reducible] [instance] :
|
||||
protected definition linear_ordered_comm_ring [reducible] [trans_instance] :
|
||||
algebra.linear_ordered_comm_ring int :=
|
||||
⦃algebra.linear_ordered_comm_ring, int.integral_domain,
|
||||
le := int.le,
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ import data.int.basic data.int.order data.int.div algebra.group_power data.nat.p
|
|||
namespace int
|
||||
open - [notations] algebra
|
||||
|
||||
definition int_has_pow_nat : has_pow_nat int :=
|
||||
definition int_has_pow_nat [reducible] [instance] [priority int.prio] : has_pow_nat int :=
|
||||
has_pow_nat.mk has_pow_nat.pow_nat
|
||||
|
||||
/-
|
||||
|
|
|
|||
|
|
@ -290,9 +290,10 @@ nat.cases_on n
|
|||
!succ_ne_zero))
|
||||
|
||||
open - [notations] algebra
|
||||
protected definition comm_semiring [reducible] [instance] : algebra.comm_semiring nat :=
|
||||
protected definition comm_semiring [reducible] [trans_instance] : algebra.comm_semiring nat :=
|
||||
⦃algebra.comm_semiring,
|
||||
add := nat.add,
|
||||
|
||||
add_assoc := add.assoc,
|
||||
zero := nat.zero,
|
||||
zero_add := zero_add,
|
||||
|
|
|
|||
|
|
@ -136,7 +136,7 @@ else (eq_max_left h) ▸ !le.refl
|
|||
|
||||
open - [notations] algebra
|
||||
|
||||
protected definition decidable_linear_ordered_semiring [reducible] [instance] :
|
||||
protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] :
|
||||
algebra.decidable_linear_ordered_semiring nat :=
|
||||
⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring,
|
||||
add_left_cancel := @add.cancel_left,
|
||||
|
|
|
|||
|
|
@ -535,7 +535,7 @@ decidable.by_cases
|
|||
end))
|
||||
|
||||
|
||||
protected definition discrete_field [reducible] [instance] : algebra.discrete_field rat :=
|
||||
protected definition discrete_field [reducible] [trans_instance] : algebra.discrete_field rat :=
|
||||
⦃algebra.discrete_field,
|
||||
add := rat.add,
|
||||
add_assoc := add.assoc,
|
||||
|
|
@ -560,10 +560,10 @@ protected definition discrete_field [reducible] [instance] : algebra.discrete_fi
|
|||
has_decidable_eq := has_decidable_eq⦄
|
||||
|
||||
definition rat_has_division [instance] [reducible] [priority rat.prio] : has_division rat :=
|
||||
has_division.mk algebra.division
|
||||
has_division.mk has_division.division
|
||||
|
||||
definition rat_has_pow_nat [instance] [reducible] [priority rat.prio] : has_pow_nat rat :=
|
||||
has_pow_nat.mk pow_nat
|
||||
has_pow_nat.mk has_pow_nat.pow_nat
|
||||
|
||||
theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
|
||||
have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'),
|
||||
|
|
|
|||
|
|
@ -302,7 +302,7 @@ let H' := le_of_lt H in
|
|||
(take Heq, let Heq' := add_left_cancel Heq in
|
||||
!lt_irrefl (Heq' ▸ H)))
|
||||
|
||||
protected definition discrete_linear_ordered_field [reducible] [instance] :
|
||||
protected definition discrete_linear_ordered_field [reducible] [trans_instance] :
|
||||
algebra.discrete_linear_ordered_field rat :=
|
||||
⦃algebra.discrete_linear_ordered_field,
|
||||
rat.discrete_field,
|
||||
|
|
@ -386,7 +386,7 @@ section
|
|||
rewrite [-mul_denom],
|
||||
apply mul_neg_of_neg_of_pos H,
|
||||
change of_int (denom q) > of_int 0,
|
||||
rewrite [of_int_lt_of_int_iff],
|
||||
xrewrite [of_int_lt_of_int_iff],
|
||||
exact !denom_pos
|
||||
end,
|
||||
show num q < 0, from lt_of_of_int_lt_of_int this
|
||||
|
|
@ -397,7 +397,7 @@ section
|
|||
rewrite [-mul_denom],
|
||||
apply mul_nonpos_of_nonpos_of_nonneg H,
|
||||
change of_int (denom q) ≥ of_int 0,
|
||||
rewrite [of_int_le_of_int_iff],
|
||||
xrewrite [of_int_le_of_int_iff],
|
||||
exact int.le_of_lt !denom_pos
|
||||
end,
|
||||
show num q ≤ 0, from le_of_of_int_le_of_int this
|
||||
|
|
|
|||
|
|
@ -38,26 +38,25 @@ section
|
|||
open nat decidable
|
||||
|
||||
theorem root_irrational {a b c n : ℕ} (npos : n > 0) (apos : a > 0) (co : coprime a b)
|
||||
(H : a^n = c * b^n) :
|
||||
b = 1 :=
|
||||
(H : a^n = c * b^n) : b = 1 :=
|
||||
have bpos : b > 0, from pos_of_ne_zero
|
||||
(suppose b = 0,
|
||||
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⁻¹),
|
||||
show false, from ne_of_lt `0 < a` this⁻¹),
|
||||
have H₁ : ∀ p, prime p → ¬ p ∣ b, from
|
||||
take p, suppose prime p, suppose p ∣ b,
|
||||
assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`,
|
||||
have p ∣ a^n, by rewrite H; apply dvd_mul_of_dvd_right this,
|
||||
have p ∣ a, from dvd_of_prime_of_dvd_pow `prime p` this,
|
||||
assert p ∣ b^n, from dvd_pow_of_dvd_of_pos `p ∣ b` `n > 0`,
|
||||
have p ∣ a^n, by rewrite H; apply dvd_mul_of_dvd_right this,
|
||||
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 blt2 : b < 2, from by_contradiction
|
||||
show false, from this `coprime a b`,
|
||||
have blt2 : b < 2, from by_contradiction
|
||||
(suppose ¬ b < 2,
|
||||
have b ≥ 2, from le_of_not_gt this,
|
||||
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 blt2) (succ_le_of_lt bpos))
|
||||
show false, from H₁ p primep pdvdb),
|
||||
show b = 1, from (le.antisymm (le_of_lt_succ blt2) (succ_le_of_lt bpos))
|
||||
end
|
||||
|
||||
/-
|
||||
|
|
@ -71,10 +70,10 @@ section
|
|||
theorem denom_eq_one_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) :
|
||||
denom q = 1 :=
|
||||
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 : ((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 b ≠ 0, from ne_of_gt (denom_pos q),
|
||||
have bnz : b ≠ (0 : ℚ), from assume H, `b ≠ 0` (of_int.inj H),
|
||||
have bnnz : ((b : rat)^n ≠ 0), from assume bneqz, bnz (algebra.eq_zero_of_pow_eq_zero bneqz),
|
||||
have a^n /[rat] b^n = c, using bnz, begin rewrite [*of_int_pow, -algebra.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,
|
||||
|
|
@ -82,7 +81,7 @@ section
|
|||
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,
|
||||
begin apply int.of_nat.inj, rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs], exact this end,
|
||||
have H₂ : nat.coprime (nat_abs a) (nat_abs b), from of_nat.inj !coprime_num_denom,
|
||||
have nat_abs b = 1, from
|
||||
by_cases
|
||||
|
|
@ -99,13 +98,11 @@ section
|
|||
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,
|
||||
have of_int c = (num q)^n, using this,
|
||||
by rewrite [-H, eq_num_div_denom q at {1}, this, div_one, of_int_pow],
|
||||
have of_int c = of_int ((num q)^n), using this,
|
||||
by krewrite [-H, eq_num_div_denom q at {1}, this, div_one, of_int_pow],
|
||||
show c = (num q)^n , from of_int.inj this
|
||||
end
|
||||
|
||||
|
|
@ -121,11 +118,11 @@ section
|
|||
(suppose p = 0,
|
||||
show false,
|
||||
by let H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H),
|
||||
have agtz : a > 0, from pos_of_ne_zero
|
||||
assert agtz : a > 0, from pos_of_ne_zero
|
||||
(suppose a = 0,
|
||||
show false, using npos pnez, by revert peq; rewrite [this, zero_pow npos]; exact pnez),
|
||||
show false, using npos pnez, by revert peq; krewrite [this, zero_pow npos]; exact pnez),
|
||||
have n * mult p a = 1, from calc
|
||||
n * mult p a = mult p (a^n) : using agtz, by rewrite [mult_pow n agtz primep]
|
||||
n * mult p a = mult p (a^n) : begin krewrite [mult_pow n agtz primep] end
|
||||
... = mult p p : peq
|
||||
... = 1 : mult_self (gt_one_of_prime primep),
|
||||
have n ∣ 1, from dvd_of_mul_right_eq this,
|
||||
|
|
@ -163,7 +160,7 @@ section
|
|||
have a * a = c * b * b, by rewrite -mul.assoc at H; apply H,
|
||||
have a div (gcd a b) = c * b div gcd (c * b) a, from div_gcd_eq_div_gcd this bpos apos,
|
||||
have a = c * b div gcd c a,
|
||||
using this, by revert this; rewrite [↑coprime at co, co, div_one, H₁]; intros; assumption,
|
||||
using this, by revert this; krewrite [↑coprime at co, co, int.div_one, H₁]; intros; assumption,
|
||||
have a = b * (c div gcd c a),
|
||||
using this,
|
||||
by revert this; rewrite [mul.comm, !mul_div_assoc !gcd_dvd_left]; intros; assumption,
|
||||
|
|
|
|||
Loading…
Reference in a new issue