refactor(library/data/int/*): use better direction for of_nat theorems

This commit is contained in:
Jeremy Avigad 2015-05-25 20:00:41 +10:00 committed by Leonardo de Moura
parent fdc89cd285
commit 4ed9e46532
3 changed files with 10 additions and 10 deletions

View file

@ -115,11 +115,11 @@ int.cases_on a
(if H : m' = n' then inl (congr_arg neg_succ_of_nat H) else
inr (take H1, H (neg_succ_of_nat.inj H1)))))
theorem of_nat_add_of_nat (n m : nat) : #int n + m = #nat n + m := rfl
theorem of_nat_add (n m : nat) : of_nat (n + m) = of_nat n + of_nat m := rfl
theorem of_nat_succ (n : ) : of_nat (succ n) = of_nat n + 1 := rfl
theorem of_nat_mul_of_nat (n m : ) : of_nat n * of_nat m = n * m := rfl
theorem of_nat_mul (n m : ) : of_nat (n * m) = of_nat n * of_nat m := rfl
theorem sub_nat_nat_of_ge {m n : } (H : m ≥ n) : sub_nat_nat m n = of_nat (m - n) :=
have H1 : n - m = 0, from sub_eq_zero_of_le H,
@ -649,6 +649,6 @@ have H2 : m = (#nat m - n) + n, from congr_arg of_nat H1,
sub_eq_of_eq_add H2
theorem neg_succ_of_nat_eq' (m : ) : -[m +1] = -m - 1 :=
by rewrite [neg_succ_of_nat_eq, -of_nat_add_of_nat, neg_add]
by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add]
end int

View file

@ -246,7 +246,7 @@ or.elim (nat.lt_or_ge m (#nat n * k))
... = #nat n - (m div k + 1) : nat.sub_sub
... = n - (#nat m div k + 1) : of_nat_sub_of_nat H4
... = -(m div k + 1) + n :
by rewrite [add.comm, -sub_eq_add_neg, -of_nat_add_of_nat, of_nat_div_of_nat]
by rewrite [add.comm, -sub_eq_add_neg, of_nat_add, of_nat_div_of_nat]
... = -[m +1] div k + n :
neg_succ_of_nat_div m (of_nat_lt_of_nat H2)))
(assume nk_le_m : #nat n * k ≤ m,
@ -257,7 +257,7 @@ or.elim (nat.lt_or_ge m (#nat n * k))
... = -((#nat (m - n * k + n * k) div k) + 1) + n : nat.sub_add_cancel nk_le_m
... = -((#nat (m - n * k) div k + n) + 1) + n : nat.add_mul_div_self H2
... = -((#nat m - n * k) div k + 1) :
by rewrite [-of_nat_add_of_nat, *neg_add, add.right_comm, neg_add_cancel_right,
by rewrite [of_nat_add, *neg_add, add.right_comm, neg_add_cancel_right,
of_nat_div_of_nat]
... = -[(#nat m - n * k) +1] div k :
neg_succ_of_nat_div _ (of_nat_lt_of_nat H2)

View file

@ -53,11 +53,11 @@ or.elim (nonneg_or_nonneg_neg (b - a))
theorem of_nat_le_of_nat {m n : } (H : #nat m ≤ n) : of_nat m ≤ of_nat n :=
obtain (k : ) (Hk : m + k = n), from nat.le.elim H,
le.intro (Hk ▸ of_nat_add_of_nat m k)
le.intro (Hk ▸ (of_nat_add m k)⁻¹)
theorem le_of_of_nat_le_of_nat {m n : } (H : of_nat m ≤ of_nat n) : (#nat m ≤ n) :=
obtain (k : ) (Hk : of_nat m + of_nat k = of_nat n), from le.elim H,
have H1 : m + k = n, from of_nat.inj ((of_nat_add_of_nat m k)⁻¹ ⬝ Hk),
have H1 : m + k = n, from of_nat.inj (of_nat_add m k ⬝ Hk),
nat.le.intro H1
theorem of_nat_le_of_nat_iff (m n : ) : of_nat m ≤ of_nat n ↔ m ≤ n :=
@ -104,7 +104,7 @@ obtain (n : ) (Hn : a + n = b), from le.elim H1,
obtain (m : ) (Hm : b + m = c), from le.elim H2,
have H3 : a + of_nat (n + m) = c, from
calc
a + of_nat (n + m) = a + (of_nat n + m) : {(of_nat_add_of_nat n m)⁻¹}
a + of_nat (n + m) = a + (of_nat n + m) : {of_nat_add n m}
... = a + n + m : (add.assoc a n m)⁻¹
... = b + m : {Hn}
... = c : Hm,
@ -116,7 +116,7 @@ obtain (n : ) (Hn : a + n = b), from le.elim H₁,
obtain (m : ) (Hm : b + m = a), from le.elim H₂,
have H₃ : a + of_nat (n + m) = a + 0, from
calc
a + of_nat (n + m) = a + (of_nat n + m) : of_nat_add_of_nat
a + of_nat (n + m) = a + (of_nat n + m) : of_nat_add
... = a + n + m : add.assoc
... = b + m : Hn
... = a : Hm
@ -211,7 +211,7 @@ lt.intro
... = succ n * b : nat.zero_add
... = succ n * (0 + succ m) : {Hm⁻¹}
... = succ n * succ m : nat.zero_add
... = of_nat (succ n * succ m) : of_nat_mul_of_nat
... = of_nat (succ n * succ m) : of_nat_mul
... = of_nat (succ n * m + succ n) : nat.mul_succ
... = of_nat (succ (succ n * m + n)) : nat.add_succ
... = 0 + succ (succ n * m + n) : zero_add))