michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/int,library/data/rat): rename theorems: of_nat_zero, of_nat_one, of_int_zero, of_int_one

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-12 17:18:10 -07:00
parent e8454fad26
commit 6e44a42779
5 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/int/basic.lean
View file

@ -54,10 +54,10 @@ has_zero.mk (of_nat 0)
definition int_has_one [reducible] [instance] : has_one int := definition int_has_one [reducible] [instance] : has_one int :=
has_one.mk (of_nat 1) has_one.mk (of_nat 1)
theorem int_zero_eq_nat_zero : (0:int) = of_nat (0:nat) := theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
rfl rfl
theorem int_one_eq_nat_one : (1:int) = of_nat (1:nat) := theorem of_nat_one : of_nat (1:nat) = (1:int) :=
rfl rfl
/- definitions of basic functions -/ /- definitions of basic functions -/

4
library/data/int/div.lean
View file

@ -108,8 +108,8 @@ by krewrite [divide.def, sign_zero, zero_mul]
theorem div_one (a : ℤ) : a div 1 = a := theorem div_one (a : ℤ) : a div 1 = a :=
assert (1 : int) > 0, from dec_trivial, assert (1 : int) > 0, from dec_trivial,
int.cases_on a int.cases_on a
(take m : nat, by rewrite [int_one_eq_nat_one, -of_nat_div, nat.div_one]) (take m : nat, by rewrite [-of_nat_one, -of_nat_div, nat.div_one])
(take m : nat, by rewrite [!neg_succ_of_nat_div this, int_one_eq_nat_one, -of_nat_div, nat.div_one]) (take m : nat, by rewrite [!neg_succ_of_nat_div this, -of_nat_one, -of_nat_div, nat.div_one])
theorem eq_div_mul_add_mod (a b : ℤ) : a = a div b * b + a mod b := theorem eq_div_mul_add_mod (a b : ℤ) : a = a div b * b + a mod b :=
!add.comm ▸ eq_add_of_sub_eq rfl !add.comm ▸ eq_add_of_sub_eq rfl

2
library/data/int/gcd.lean
View file

@ -265,7 +265,7 @@ theorem gcd_mul_left_cancel_of_coprime {c : ℤ} (a : ℤ) {b : ℤ} (H : coprim
gcd (c * a) b = gcd a b := gcd (c * a) b = gcd a b :=
begin begin
revert H, unfold [coprime, gcd], revert H, unfold [coprime, gcd],
rewrite [int_one_eq_nat_one], rewrite [-of_nat_one],
rewrite [+of_nat_eq_of_nat_iff, nat_abs_mul], rewrite [+of_nat_eq_of_nat_iff, nat_abs_mul],
apply nat.gcd_mul_left_cancel_of_coprime, apply nat.gcd_mul_left_cancel_of_coprime,
end end

4
library/data/rat/basic.lean
View file

@ -364,10 +364,10 @@ has_zero.mk (0:int)
definition rat_has_one [reducible] [instance] [priority rat.prio] : has_one rat := definition rat_has_one [reducible] [instance] [priority rat.prio] : has_one rat :=
has_one.mk (1:int) has_one.mk (1:int)
theorem rat_zero_eq_int_zero : (0:rat) = of_int (0:int) := theorem of_int_zero : of_int (0:int) = (0:rat) :=
rfl rfl
theorem rat_one_eq_int_one : (1:rat) = of_int (1:int) := theorem of_int_one : of_int (1:int) = (1:rat) :=
rfl rfl
protected definition add : ℚ → ℚ → ℚ := protected definition add : ℚ → ℚ → ℚ :=

4
library/data/rat/order.lean
View file

@ -368,7 +368,7 @@ section
begin begin
rewrite [-mul_denom], rewrite [-mul_denom],
apply mul_nonneg H, apply mul_nonneg H,
rewrite [rat_zero_eq_int_zero, of_int_le_of_int_iff], rewrite [-of_int_zero, of_int_le_of_int_iff],
exact int.le_of_lt !denom_pos exact int.le_of_lt !denom_pos
end, end,
show num q ≥ 0, from le_of_of_int_le_of_int this show num q ≥ 0, from le_of_of_int_le_of_int this
@ -378,7 +378,7 @@ section
begin begin
rewrite [-mul_denom], rewrite [-mul_denom],
apply mul_pos H, apply mul_pos H,
rewrite [rat_zero_eq_int_zero, of_int_lt_of_int_iff], rewrite [-of_int_zero, of_int_lt_of_int_iff],
exact !denom_pos exact !denom_pos
end, end,
show num q > 0, from lt_of_of_int_lt_of_int this show num q > 0, from lt_of_of_int_lt_of_int this