fix(library/data/int/basic): change notation from -[n+1] to -[1+n] to avoid conflict e.g. with -[coercions]
This commit is contained in:
Jeremy Avigad
parent
3bf18c174e
commit
130eb3f6d9
5 changed files with 45 additions and 43 deletions
|
|
@ -96,38 +96,38 @@ open nat int algebra
|
|||
|
||||
definition ipow (a : A) : ℤ → A
|
||||
| (of_nat n) := a^n
|
||||
| -[n +1] := (a^(nat.succ n))⁻¹
|
||||
| -[1+n] := (a^(nat.succ n))⁻¹
|
||||
|
||||
private lemma ipow_add_aux (a : A) (m n : nat) :
|
||||
ipow a ((of_nat m) + -[n +1]) = ipow a (of_nat m) * ipow a (-[n +1]) :=
|
||||
ipow a ((of_nat m) + -[1+n]) = ipow a (of_nat m) * ipow a (-[1+n]) :=
|
||||
or.elim (nat.lt_or_ge m (nat.succ n))
|
||||
(assume H : (#nat m < nat.succ n),
|
||||
assert H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
|
||||
calc
|
||||
ipow a ((of_nat m) + -[n +1]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl
|
||||
... = ipow a (-[nat.pred (nat.sub (nat.succ n) m) +1]) : {sub_nat_nat_of_lt H}
|
||||
ipow a ((of_nat m) + -[1+n]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl
|
||||
... = ipow a (-[1+ nat.pred (nat.sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H}
|
||||
... = (pow a (nat.succ (nat.pred (nat.sub (nat.succ n) m))))⁻¹ : rfl
|
||||
... = (pow a (nat.succ n) * (pow a m)⁻¹)⁻¹ :
|
||||
by rewrite [nat.succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)]
|
||||
... = pow a m * (pow a (nat.succ n))⁻¹ :
|
||||
by rewrite [mul_inv, inv_inv]
|
||||
... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl)
|
||||
... = ipow a (of_nat m) * ipow a (-[1+n]) : rfl)
|
||||
(assume H : (#nat m ≥ nat.succ n),
|
||||
calc
|
||||
ipow a ((of_nat m) + -[n +1]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl
|
||||
ipow a ((of_nat m) + -[1+n]) = ipow a (sub_nat_nat m (nat.succ n)) : rfl
|
||||
... = ipow a (#nat m - nat.succ n) : {sub_nat_nat_of_ge H}
|
||||
... = pow a m * (pow a (nat.succ n))⁻¹ : pow_sub a H
|
||||
... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl)
|
||||
... = ipow a (of_nat m) * ipow a (-[1+n]) : rfl)
|
||||
|
||||
theorem ipow_add (a : A) : ∀i j : int, ipow a (i + j) = ipow a i * ipow a j
|
||||
| (of_nat m) (of_nat n) := !pow_add
|
||||
| (of_nat m) -[n +1] := !ipow_add_aux
|
||||
| -[ m+1] (of_nat n) := by rewrite [int.add.comm, ipow_add_aux, ↑ipow, -*inv_pow, pow_inv_comm]
|
||||
| -[ m+1] -[n+1] :=
|
||||
| (of_nat m) -[1+n] := !ipow_add_aux
|
||||
| -[1+m] (of_nat n) := by rewrite [int.add.comm, ipow_add_aux, ↑ipow, -*inv_pow, pow_inv_comm]
|
||||
| -[1+m] -[1+n] :=
|
||||
calc
|
||||
ipow a (-[ m+1] + -[n+1]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl
|
||||
ipow a (-[1+m] + -[1+n]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl
|
||||
... = (a^(nat.succ m))⁻¹ * (a^(nat.succ n))⁻¹ : by rewrite [pow_add, pow_comm, mul_inv]
|
||||
... = ipow a (-[ m+1]) * ipow a (-[n+1]) : rfl
|
||||
... = ipow a (-[1+m]) * ipow a (-[1+n]) : rfl
|
||||
|
||||
theorem ipow_comm (a : A) (i j : ℤ) : ipow a i * ipow a j = ipow a j * ipow a i :=
|
||||
by rewrite [-*ipow_add, int.add.comm]
|
||||
|
|
|
|||
|
|
@ -85,7 +85,7 @@ definition mul (a b : ℤ) : ℤ :=
|
|||
|
||||
/- notation -/
|
||||
|
||||
notation `-[` n `+1]` := int.neg_succ_of_nat n -- for pretty-printing output
|
||||
notation `-[1+` n `]` := int.neg_succ_of_nat n -- for pretty-printing output
|
||||
prefix - := int.neg
|
||||
infix + := int.add
|
||||
infix * := int.mul
|
||||
|
|
@ -101,7 +101,7 @@ iff.intro of_nat.inj !congr_arg
|
|||
theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n :=
|
||||
by injection H; assumption
|
||||
|
||||
theorem neg_succ_of_nat_eq (n : ℕ) : -[n +1] = -(n + 1) := rfl
|
||||
theorem neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl
|
||||
|
||||
definition has_decidable_eq [instance] : decidable_eq ℤ :=
|
||||
take a b,
|
||||
|
|
@ -641,7 +641,7 @@ have H1 : m = (#nat m - n + n), from (nat.sub_add_cancel H)⁻¹,
|
|||
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 :=
|
||||
theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=
|
||||
by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add]
|
||||
|
||||
definition succ (a : ℤ) := a + (nat.succ zero)
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ definition divide (a b : ℤ) : ℤ :=
|
|||
sign b *
|
||||
(match a with
|
||||
| of_nat m := #nat m div (nat_abs b)
|
||||
| -[ m +1] := -[ (#nat m div (nat_abs b)) +1]
|
||||
| -[1+m] := -[1+ (#nat m div (nat_abs b))]
|
||||
end)
|
||||
notation a div b := divide a b
|
||||
|
||||
|
|
@ -37,17 +37,17 @@ nat.cases_on n
|
|||
(take n, by rewrite [↑divide, sign_of_succ, one_mul])
|
||||
|
||||
theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) :
|
||||
-[m +1] div b = -(m div b + 1) :=
|
||||
-[1+m] div b = -(m div b + 1) :=
|
||||
calc
|
||||
-[m +1] div b = sign b * _ : rfl
|
||||
... = -[(#nat m div (nat_abs b)) +1] : by rewrite [sign_of_pos H, one_mul]
|
||||
-[1+m] div b = sign b * _ : rfl
|
||||
... = -[1+(#nat m div (nat_abs b))] : by rewrite [sign_of_pos H, one_mul]
|
||||
... = -(m div b + 1) : by rewrite [↑divide, sign_of_pos H, one_mul]
|
||||
|
||||
theorem div_neg (a b : ℤ) : a div -b = -(a div b) :=
|
||||
by rewrite [↑divide, sign_neg, neg_mul_eq_neg_mul, nat_abs_neg]
|
||||
|
||||
theorem div_of_neg_of_pos {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b = -((-a - 1) div b + 1) :=
|
||||
obtain m (H1 : a = -[m +1]), from exists_eq_neg_succ_of_nat Ha,
|
||||
obtain m (H1 : a = -[1+m]), from exists_eq_neg_succ_of_nat Ha,
|
||||
calc
|
||||
a div b = -(m div b + 1) : by rewrite [H1, neg_succ_of_nat_div _ Hb]
|
||||
... = -((-a -1) div b + 1) : by rewrite [H1, neg_succ_of_nat_eq', neg_sub, sub_neg_eq_add,
|
||||
|
|
@ -100,12 +100,12 @@ int.cases_on a
|
|||
m div n = #nat m div n : of_nat_div
|
||||
... = 0 : nat.div_eq_zero_of_lt (lt_of_of_nat_lt_of_nat H))
|
||||
(take n,
|
||||
assume H : m < -[ n +1],
|
||||
have H1 : ¬(m < -[ n +1]), from dec_trivial,
|
||||
assume H : m < -[1+n],
|
||||
have H1 : ¬(m < -[1+n]), from dec_trivial,
|
||||
absurd H H1))
|
||||
(take m,
|
||||
assume H : 0 ≤ -[ m +1],
|
||||
have H1 : ¬ (0 ≤ -[ m +1]), from dec_trivial,
|
||||
assume H : 0 ≤ -[1+m],
|
||||
have H1 : ¬ (0 ≤ -[1+m]), from dec_trivial,
|
||||
absurd H H1)
|
||||
|
||||
theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a div b = 0 :=
|
||||
|
|
@ -134,14 +134,14 @@ Hm⁻¹ ▸ (calc
|
|||
private theorem add_mul_div_self_aux2 {a : ℤ} {k : ℕ} (n : ℕ)
|
||||
(H1 : a < 0) (H2 : #nat k > 0) :
|
||||
(a + n * k) div k = a div k + n :=
|
||||
obtain m (Hm : a = -[m +1]), from exists_eq_neg_succ_of_nat H1,
|
||||
obtain m (Hm : a = -[1+m]), from exists_eq_neg_succ_of_nat H1,
|
||||
or.elim (nat.lt_or_ge m (#nat n * k))
|
||||
(assume m_lt_nk : #nat m < n * k,
|
||||
have H3 : #nat (m + 1 ≤ n * k), from nat.succ_le_of_lt m_lt_nk,
|
||||
have H4 : #nat m div k + 1 ≤ n,
|
||||
from nat.succ_le_of_lt (nat.div_lt_of_lt_mul m_lt_nk),
|
||||
Hm⁻¹ ▸ (calc
|
||||
(-[m +1] + n * k) div k = (n * k - (m + 1)) div k : by rewrite [add.comm, neg_succ_of_nat_eq]
|
||||
(-[1+m] + n * k) div k = (n * k - (m + 1)) div k : by rewrite [add.comm, neg_succ_of_nat_eq]
|
||||
... = ((#nat n * k) - (#nat m + 1)) div k : rfl
|
||||
... = (#nat n * k - (m + 1)) div k : {(of_nat_sub H3)⁻¹}
|
||||
... = #nat (n * k - (m + 1)) div k : of_nat_div
|
||||
|
|
@ -152,11 +152,11 @@ or.elim (nat.lt_or_ge m (#nat n * k))
|
|||
... = n - (#nat m div k + 1) : of_nat_sub H4
|
||||
... = -(m div k + 1) + n :
|
||||
by rewrite [add.comm, -sub_eq_add_neg, of_nat_add, of_nat_div]
|
||||
... = -[m +1] div k + n :
|
||||
... = -[1+m] div k + n :
|
||||
neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2)))
|
||||
(assume nk_le_m : #nat n * k ≤ m,
|
||||
eq.symm (Hm⁻¹ ▸ (calc
|
||||
-[m +1] div k + n = -(m div k + 1) + n :
|
||||
-[1+m] div k + n = -(m div k + 1) + n :
|
||||
neg_succ_of_nat_div m (of_nat_lt_of_nat_of_lt H2)
|
||||
... = -((#nat m div k) + 1) + n : of_nat_div
|
||||
... = -((#nat (m - n * k + n * k) div k) + 1) + n : nat.sub_add_cancel nk_le_m
|
||||
|
|
@ -164,13 +164,13 @@ or.elim (nat.lt_or_ge m (#nat n * k))
|
|||
... = -((#nat m - n * k) div k + 1) :
|
||||
by rewrite [of_nat_add, *neg_add, add.right_comm, neg_add_cancel_right,
|
||||
of_nat_div]
|
||||
... = -[(#nat m - n * k) +1] div k :
|
||||
... = -[1+(#nat m - n * k)] div k :
|
||||
neg_succ_of_nat_div _ (of_nat_lt_of_nat_of_lt H2)
|
||||
... = -((#nat m - n * k) + 1) div k : rfl
|
||||
... = -(m - (#nat n * k) + 1) div k : of_nat_sub nk_le_m
|
||||
... = (-(m + 1) + n * k) div k :
|
||||
by rewrite [sub_eq_add_neg, -*add.assoc, *neg_add, neg_neg, add.right_comm]
|
||||
... = (-[m +1] + n * k) div k : rfl)))
|
||||
... = (-[1+m] + n * k) div k : rfl)))
|
||||
|
||||
private theorem add_mul_div_self_aux3 (a : ℤ) {b c : ℤ} (H1 : b ≥ 0) (H2 : c > 0) :
|
||||
(a + b * c) div c = a div c + b :=
|
||||
|
|
@ -236,9 +236,9 @@ calc
|
|||
... = (#nat m mod n) : sub_eq_of_eq_add H
|
||||
|
||||
theorem neg_succ_of_nat_mod (m : ℕ) {b : ℤ} (bpos : b > 0) :
|
||||
-[m +1] mod b = b - 1 - m mod b :=
|
||||
-[1+m] mod b = b - 1 - m mod b :=
|
||||
calc
|
||||
-[m +1] mod b = -(m + 1) - -[m +1] div b * b : rfl
|
||||
-[1+m] mod b = -(m + 1) - -[1+m] div b * b : rfl
|
||||
... = -(m + 1) - -(m div b + 1) * b : neg_succ_of_nat_div _ bpos
|
||||
... = -m + -1 + (b + m div b * b) :
|
||||
by rewrite [neg_add, -neg_mul_eq_neg_mul, sub_neg_eq_add, mul.right_distrib,
|
||||
|
|
@ -300,7 +300,7 @@ have H2 : a mod (abs b) ≥ 0, from
|
|||
have H3 : 1 + m mod (abs b) ≤ (abs b),
|
||||
from (!add.comm ▸ add_one_le_of_lt (of_nat_mod_abs_lt m H)),
|
||||
calc
|
||||
-[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1
|
||||
-[1+m] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1
|
||||
... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc]
|
||||
... ≥ 0 : iff.mp' !sub_nonneg_iff_le H3),
|
||||
!mod_abs ▸ H2
|
||||
|
|
@ -314,7 +314,7 @@ have H2 : a mod (abs b) < abs b, from
|
|||
have H3 : abs b ≠ 0, from assume H', H (eq_zero_of_abs_eq_zero H'),
|
||||
have H4 : 1 + m mod (abs b) > 0, from add_pos_of_pos_of_nonneg dec_trivial (mod_nonneg _ H3),
|
||||
calc
|
||||
-[ m +1] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1
|
||||
-[1+m] mod (abs b) = abs b - 1 - m mod (abs b) : neg_succ_of_nat_mod _ H1
|
||||
... = abs b - (1 + m mod (abs b)) : by rewrite [*sub_eq_add_neg, neg_add, add.assoc]
|
||||
... < abs b : sub_lt_self _ H4),
|
||||
!mod_abs ▸ H2
|
||||
|
|
|
|||
|
|
@ -363,7 +363,7 @@ theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b :=
|
|||
theorem sign_of_succ (n : nat) : sign (nat.succ n) = 1 :=
|
||||
sign_of_pos (of_nat_pos !nat.succ_pos)
|
||||
|
||||
theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[m +1] :=
|
||||
theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → ∃m : ℕ, a = -[1+m] :=
|
||||
int.cases_on a
|
||||
(take m H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H))
|
||||
(take m H, exists.intro m rfl)
|
||||
|
|
|
|||
|
|
@ -105,9 +105,9 @@ theorem of_int.inj {a b : ℤ} : of_int a ≡ of_int b → a = b :=
|
|||
by rewrite [↑of_int, ↑equiv, *mul_one]; intros; assumption
|
||||
|
||||
definition inv : prerat → prerat
|
||||
| inv (prerat.mk nat.zero d dp) := zero
|
||||
| inv (prerat.mk nat.zero d dp) := zero
|
||||
| inv (prerat.mk (nat.succ n) d dp) := prerat.mk d (nat.succ n) !of_nat_succ_pos
|
||||
| inv (prerat.mk -[n +1] d dp) := prerat.mk (-d) (nat.succ n) !of_nat_succ_pos
|
||||
| inv (prerat.mk -[1+n] d dp) := prerat.mk (-d) (nat.succ n) !of_nat_succ_pos
|
||||
|
||||
theorem equiv_zero_of_num_eq_zero {a : prerat} (H : num a = 0) : a ≡ zero :=
|
||||
by rewrite [↑equiv, H, ↑zero, ↑num, ↑of_int, *zero_mul]
|
||||
|
|
@ -132,9 +132,9 @@ obtain (n' : nat) (Hn' : n = of_nat n'), from exists_eq_of_nat (le_of_lt np),
|
|||
have H1 : (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
|
||||
obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt H1,
|
||||
have H2 : -d * n = -d * nat.succ k, by rewrite [Hn', Hk],
|
||||
have H3 : inv (mk -[k +1] d dp) ≡ mk (-d) n np, from H2,
|
||||
have H4 : -[k +1] = -n, from calc
|
||||
-[k +1] = -(nat.succ k) : rfl
|
||||
have H3 : inv (mk -[1+k] d dp) ≡ mk (-d) n np, from H2,
|
||||
have H4 : -[1+k] = -n, from calc
|
||||
-[1+k] = -(nat.succ k) : rfl
|
||||
... = -n : by rewrite [Hk⁻¹, Hn'],
|
||||
H4 ▸ H3
|
||||
|
||||
|
|
@ -298,13 +298,15 @@ theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b
|
|||
decidable.by_cases
|
||||
(assume anz : an = 0,
|
||||
have H' : bn * ad = 0, by rewrite [-H, anz, zero_mul],
|
||||
assert bnz : bn = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos),
|
||||
assert bnz : bn = 0,
|
||||
from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos),
|
||||
by rewrite [↑reduce, if_pos anz, if_pos bnz])
|
||||
(assume annz : an ≠ 0,
|
||||
assert bnnz : bn ≠ 0, from
|
||||
assume bnz,
|
||||
have H' : an * bd = 0, by rewrite [H, bnz, zero_mul],
|
||||
have anz : an = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt bdpos),
|
||||
have anz : an = 0,
|
||||
from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt bdpos),
|
||||
show false, from annz anz,
|
||||
begin
|
||||
rewrite [↑reduce, if_neg annz, if_neg bnnz],
|
||||
|
|
@ -395,7 +397,7 @@ calc
|
|||
... = of_int a - of_int b : {of_int_neg b}
|
||||
|
||||
theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b :=
|
||||
sorry
|
||||
prerat.of_int.inj (quot.exact H)
|
||||
|
||||
theorem of_nat_eq (a : ℕ) : of_nat a = of_int (int.of_nat a) := rfl
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue