From a618bd7d6c3efdfc052c6bcbdeac9e1367154839 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Oct 2015 16:44:47 -0700 Subject: [PATCH] refactor(library): use type classes for encoding all arithmetic operations Before this commit we were using overloading for concrete structures and type classes for abstract ones. This is the first of series of commits that implement this modification --- library/algebra/complete_lattice.lean | 4 +- library/algebra/field.lean | 33 ++--- library/algebra/group.lean | 26 +--- library/algebra/group_power.lean | 17 +-- library/algebra/order.lean | 34 ----- library/algebra/ordered_field.lean | 4 +- library/algebra/ordered_group.lean | 9 +- library/algebra/ordered_ring.lean | 10 +- library/algebra/ring.lean | 6 +- library/algebra/ring_power.lean | 2 +- library/data/int/basic.lean | 172 +++++++++++++------------- library/data/int/div.lean | 36 ++++-- library/data/int/order.lean | 145 +++++++++------------- library/data/list/basic.lean | 5 +- library/data/nat/basic.lean | 52 ++++---- library/data/nat/div.lean | 97 ++++++++------- library/data/nat/fact.lean | 1 + library/data/nat/gcd.lean | 3 +- library/data/nat/order.lean | 138 +++++++++------------ library/data/nat/pairing.lean | 1 + library/data/nat/sqrt.lean | 1 + library/data/nat/sub.lean | 24 ++-- library/data/quotient/util.lean | 2 +- library/data/sigma.lean | 3 +- library/init/nat.lean | 40 +++--- library/init/num.lean | 7 +- library/init/prod.lean | 6 - library/init/reserved_notation.lean | 40 ++++++ library/init/wf.lean | 4 +- src/frontends/lean/parser.cpp | 4 +- 30 files changed, 447 insertions(+), 479 deletions(-) diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index d7e24a56f1..3c3e196d7c 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -68,10 +68,10 @@ lemma le_inf {a b c : A} : c ≤ a → c ≤ b → c ≤ a ⊓ b := assume h₁ h₂, le_Inf (take x, suppose x ∈ '{a, b}, or.elim (eq_or_mem_of_mem_insert this) - (suppose x = a, by subst x; assumption) + (suppose x = a, begin subst x, exact h₁ end) (suppose x ∈ '{b}, assert x = b, from !eq_of_mem_singleton this, - by subst x; assumption)) + begin subst x, exact h₂ end)) lemma le_sup_left (a b : A) : a ≤ a ⊔ b := le_Sup !mem_insert diff --git a/library/algebra/field.lean b/library/algebra/field.lean index a8cb2a2e03..1a7e7e3550 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -24,11 +24,13 @@ section division_ring variables [s : division_ring A] {a b c : A} include s - definition divide (a b : A) : A := a * b⁻¹ - infix [priority algebra.prio] / := divide + protected definition division (a b : A) : A := a * b⁻¹ - -- only in this file - local attribute divide [reducible] + definition division_ring_has_division [reducible] [instance] : has_division A := + has_division.mk algebra.division + + lemma division.def (a b : A) : a / b = a * b⁻¹ := + rfl theorem mul_inv_cancel (H : a ≠ 0) : a * a⁻¹ = 1 := division_ring.mul_inv_cancel H @@ -39,7 +41,7 @@ section division_ring theorem inv_eq_one_div (a : A) : a⁻¹ = 1 / a := !one_mul⁻¹ theorem div_eq_mul_one_div (a b : A) : a / b = a * (1 / b) := - by rewrite [↑divide, one_mul] + by rewrite [*division.def, one_mul] theorem mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 := by rewrite [-inv_eq_one_div, (mul_inv_cancel H)] @@ -62,7 +64,7 @@ section division_ring by rewrite [-mul_one, inv_mul_cancel (ne.symm (@zero_ne_one A _))] theorem div_one (a : A) : a / 1 = a := - by rewrite [↑divide, one_inv_eq, mul_one] + by rewrite [*division.def, one_inv_eq, mul_one] theorem zero_div (a : A) : 0 / a = 0 := !zero_mul @@ -129,7 +131,7 @@ section division_ring theorem div_neg_eq_neg_div (b : A) (Ha : a ≠ 0) : b / (- a) = - (b / a) := calc - b / (- a) = b * (1 / (- a)) : inv_eq_one_div + b / (- a) = b * (1 / (- a)) : by rewrite -inv_eq_one_div ... = b * -(1 / a) : division_ring.one_div_neg_eq_neg_one_div Ha ... = -(b * (1 / a)) : neg_mul_eq_mul_neg ... = - (b * a⁻¹) : inv_eq_one_div @@ -155,10 +157,10 @@ section division_ring ... = (b * a)⁻¹ : inv_eq_one_div) theorem mul_div_cancel (a : A) {b : A} (Hb : b ≠ 0) : a * b / b = a := - by rewrite [↑divide, mul.assoc, (mul_inv_cancel Hb), mul_one] + by rewrite [*division.def, mul.assoc, (mul_inv_cancel Hb), mul_one] theorem div_mul_cancel (a : A) {b : A} (Hb : b ≠ 0) : a / b * b = a := - by rewrite [↑divide, mul.assoc, (inv_mul_cancel Hb), mul_one] + by rewrite [*division.def, mul.assoc, (inv_mul_cancel Hb), mul_one] theorem div_add_div_same (a b c : A) : a / c + b / c = (a + b) / c := !right_distrib⁻¹ @@ -173,7 +175,7 @@ section division_ring theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (b - a) * (1 / b) = 1 / a - 1 / b := by rewrite [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel Ha), mul_sub_right_distrib, - one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one, one_mul] + one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one] theorem div_eq_one_iff_eq (a : A) {b : A} (Hb : b ≠ 0) : a / b = 1 ↔ a = b := iff.intro @@ -218,7 +220,6 @@ structure field [class] (A : Type) extends division_ring A, comm_ring A section field variables [s : field A] {a b c d: A} include s - local attribute divide [reducible] theorem field.one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (a * b) := by rewrite [(division_ring.one_div_mul_one_div Ha Hb), mul.comm b] @@ -246,12 +247,12 @@ section field theorem one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) := assert a * b ≠ 0, from (division_ring.mul_ne_zero Ha Hb), - by rewrite [add.comm, -(field.div_mul_left Ha this), -(field.div_mul_right Hb this), ↑divide, + by rewrite [add.comm, -(field.div_mul_left Ha this), -(field.div_mul_right Hb this), *division.def, -right_distrib] theorem field.div_mul_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) := - by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)] + by rewrite [*division.def, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)] theorem mul_div_mul_left (a : A) {b c : A} (Hb : b ≠ 0) (Hc : c ≠ 0) : (c * a) / (c * b) = a / b := @@ -262,7 +263,7 @@ section field by rewrite [(mul.comm a), (mul.comm b), (!mul_div_mul_left Hb Hc)] theorem div_mul_eq_mul_div (a b c : A) : (b / c) * a = (b * a) / c := - by rewrite [↑divide, mul.assoc, (mul.comm c⁻¹), -mul.assoc] + by rewrite [*division.def, mul.assoc, (mul.comm c⁻¹), -mul.assoc] theorem field.div_mul_eq_mul_div_comm (a b : A) {c : A} (Hc : c ≠ 0) : (b / c) * a = b * (a / c) := @@ -275,7 +276,7 @@ section field theorem div_sub_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) := - by rewrite [↑sub, neg_eq_neg_one_mul, -mul_div_assoc, (!div_add_div Hb Hd), + by rewrite [*sub_eq_add_neg, neg_eq_neg_one_mul, -mul_div_assoc, (!div_add_div Hb Hd), -mul.assoc, (mul.comm b), mul.assoc, -neg_eq_neg_one_mul] theorem mul_eq_mul_of_div_eq_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0) @@ -339,7 +340,7 @@ section discrete_field theorem one_div_zero : 1 / 0 = (0:A) := calc 1 / 0 = 1 * 0⁻¹ : refl - ... = 1 * 0 : discrete_field.inv_zero A + ... = 1 * 0 : inv_zero ... = 0 : mul_zero theorem div_zero (a : A) : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero] diff --git a/library/algebra/group.lean b/library/algebra/group.lean index df872ecab2..6dae42483b 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -16,30 +16,12 @@ namespace algebra variable {A : Type} -/- overloaded symbols -/ - -structure has_mul [class] (A : Type) := -(mul : A → A → A) - -structure has_add [class] (A : Type) := -(add : A → A → A) - structure has_one [class] (A : Type) := (one : A) structure has_zero [class] (A : Type) := (zero : A) -structure has_inv [class] (A : Type) := -(inv : A → A) - -structure has_neg [class] (A : Type) := -(neg : A → A) - -infixl [priority algebra.prio] ` * ` := has_mul.mul -infixl [priority algebra.prio] ` + ` := has_add.add -postfix [priority algebra.prio] `⁻¹` := has_inv.inv -prefix [priority algebra.prio] `-` := has_neg.neg notation 1 := !has_one.one notation 0 := !has_zero.zero @@ -478,7 +460,8 @@ section add_group -- TODO: derive corresponding facts for div in a field definition sub [reducible] (a b : A) : A := a + -b - infix [priority algebra.prio] - := sub + definition add_group_has_sub [reducible] [instance] : has_sub A := + has_sub.mk algebra.sub theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl @@ -499,7 +482,8 @@ section add_group theorem zero_sub (a : A) : 0 - a = -a := !zero_add - theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero + theorem sub_zero (a : A) : a - 0 = a := + by rewrite [sub_eq_add_neg, neg_zero, add_zero] theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := by change a + -(-b) = a + b; rewrite neg_neg @@ -515,7 +499,7 @@ section add_group theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b := calc - a - (b + c) = a + (-c - b) : neg_add_rev + a - (b + c) = a + (-c - b) : by rewrite [sub_eq_add_neg, neg_add_rev] ... = a - c - b : by krewrite -add.assoc theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b := diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index fb10d5854e..497459b36d 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -107,23 +107,24 @@ theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m end nat -open int +open nat int definition gpow (a : A) : ℤ → A | (of_nat n) := a^n | -[1+n] := (a^(nat.succ n))⁻¹ +/- private lemma gpow_add_aux (a : A) (m n : nat) : gpow a ((of_nat m) + -[1+n]) = gpow a (of_nat m) * gpow 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, + (assume H : (m < nat.succ n), + assert H1 : (nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H, calc gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n)) : rfl - ... = gpow 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 + ... = gpow a (-[1+ nat.pred (sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H} + ... = (pow a (nat.succ (nat.pred (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)] + by rewrite [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] ... = gpow a (of_nat m) * gpow a (-[1+n]) : rfl) @@ -146,8 +147,9 @@ theorem gpow_add (a : A) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j theorem gpow_comm (a : A) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i := by rewrite [-*gpow_add, int.add.comm] +-/ end group - +/- section ordered_ring open nat variable [s : linear_ordered_ring A] @@ -248,5 +250,6 @@ theorem add_imul (i j : ℤ) (a : A) : imul (i + j) a = imul i a + imul j a := theorem imul_comm (i j : ℤ) (a : A) : imul i a + imul j a = imul j a + imul i a := gpow_comm a i j end add_group +-/ end algebra diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 017d517a85..9afefb9497 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -12,25 +12,6 @@ namespace algebra variable {A : Type} -/- overloaded symbols -/ - -structure has_le [class] (A : Type) := -(le : A → A → Prop) - -structure has_lt [class] (A : Type) := -(lt : A → A → Prop) - -infixl [priority algebra.prio] <= := has_le.le -infixl [priority algebra.prio] ≤ := has_le.le -infixl [priority algebra.prio] < := has_lt.lt - -definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a -notation [priority algebra.prio] a ≥ b := has_le.ge a b -notation [priority algebra.prio] a >= b := has_le.ge a b - -definition has_lt.gt [reducible] {A : Type} [s : has_lt A] (a b : A) := b < a -notation [priority algebra.prio] a > b := has_lt.gt a b - /- weak orders -/ structure weak_order [class] (A : Type) extends has_le A := @@ -443,18 +424,3 @@ section end end algebra - -/- -For reference, these are all the transitivity rules defined in this file: -calc_trans le.trans -calc_trans lt.trans - -calc_trans lt_of_lt_of_le -calc_trans lt_of_le_of_lt - -calc_trans ge.trans -calc_trans gt.trans - -calc_trans gt_of_gt_of_ge -calc_trans gt_of_ge_of_gt --/ diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index c92d76ac58..40a9373c0e 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -169,14 +169,14 @@ section linear_ordered_field assert H1 : (a * d - c * b) / (c * d) < 0, by rewrite [mul.comm c b]; exact H, assert H2 : a / c - b / d < 0, by rewrite [!div_sub_div Hc Hd]; exact H1, assert H3 : a / c - b / d + b / d < 0 + b / d, from add_lt_add_right H2 _, - begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end + begin rewrite [zero_add at H3, sub_eq_add_neg at H3, neg_add_cancel_right at H3], exact H3 end theorem div_le_div_of_mul_sub_mul_div_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0) (H : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d := assert H1 : (a * d - c * b) / (c * d) ≤ 0, by rewrite [mul.comm c b]; exact H, assert H2 : a / c - b / d ≤ 0, by rewrite [!div_sub_div Hc Hd]; exact H1, assert H3 : a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right H2 _, - begin rewrite [zero_add at H3, neg_add_cancel_right at H3], exact H3 end + begin rewrite [zero_add at H3, sub_eq_add_neg at H3, neg_add_cancel_right at H3], exact H3 end theorem div_pos_of_pos_of_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a / b := begin diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 75afaae809..fa0cc2ff9a 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -137,7 +137,7 @@ section have Hb' : b ≤ 0, from calc b = 0 + b : by rewrite zero_add - ... ≤ a + b : add_le_add_right Ha + ... ≤ a + b : by exact add_le_add_right Ha _ ... = 0 : Hab, have Hbz : b = 0, from le.antisymm Hb' Hb, and.intro Haz Hbz) @@ -368,7 +368,7 @@ section theorem le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b := assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff), - by rewrite add_neg_cancel_right at H; exact H + by rewrite [sub_eq_add_neg (b+c) c at H, add_neg_cancel_right at H]; exact H theorem le_add_of_sub_right_le {a b c : A} : a - c ≤ b → a ≤ b + c := iff.mpr !le_add_iff_sub_right_le @@ -448,7 +448,7 @@ section theorem add_lt_iff_lt_sub_right : a + b < c ↔ a < c - b := assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff), - by rewrite add_neg_cancel_right at H; exact H + by rewrite [sub_eq_add_neg at H, add_neg_cancel_right at H]; exact H theorem add_lt_of_lt_sub_right {a b c : A} : a < c - b → a + b < c := iff.mpr !add_lt_iff_lt_sub_right @@ -793,8 +793,7 @@ section theorem abs_sub_le (a b c : A) : abs (a - c) ≤ abs (a - b) + abs (b - c) := calc - abs (a - c) = abs (a - b + (b - c)) : - by rewrite [sub_eq_add_neg, add.assoc, neg_add_cancel_left] + abs (a - c) = abs (a - b + (b - c)) : by rewrite [*sub_eq_add_neg, add.assoc, neg_add_cancel_left] ... ≤ abs (a - b) + abs (b - c) : abs_add_le_abs_add_abs theorem abs_add_three (a b c : A) : abs (a + b + c) ≤ abs a + abs b + abs c := diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index a56d4828b5..c7559b41f2 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -686,9 +686,13 @@ section sub_lt_of_abs_sub_lt_left (!abs_sub ▸ H) theorem abs_sub_square (a b : A) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b := - by rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib, - sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul, - *add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc] + begin + rewrite [abs_mul_abs_self, *mul_sub_left_distrib, *mul_sub_right_distrib, + sub_eq_add_neg (a*b), sub_add_eq_sub_sub, sub_neg_eq_add, *right_distrib, sub_add_eq_sub_sub, *one_mul, + *add.assoc, {_ + b * b}add.comm, *sub_eq_add_neg], + rewrite [{a*a + b*b}add.comm], + rewrite [mul.comm b a, *add.assoc] + end theorem abs_abs_sub_abs_le_abs_sub (a b : A) : abs (abs a - abs b) ≤ abs (a - b) := begin diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 5ca55133fe..8181ebdfed 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -72,8 +72,10 @@ section comm_semiring variables [s : comm_semiring A] (a b c : A) include s - definition dvd (a b : A) : Prop := ∃c, b = a * c - notation [priority algebra.prio] a ∣ b := dvd a b + protected definition dvd (a b : A) : Prop := ∃c, b = a * c + + definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A := + has_dvd.mk algebra.dvd theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b := exists.intro _ H⁻¹ diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean index 1d29c64c1e..47c848bde1 100644 --- a/library/algebra/ring_power.lean +++ b/library/algebra/ring_power.lean @@ -116,7 +116,7 @@ begin induction i with [i, ih], {exfalso, exact !nat.lt.irrefl ipos}, have xige1 : x^i ≥ 1, from pow_ge_one _ (le_of_lt xgt1), - rewrite [pow_succ, -mul_one 1, ↑has_lt.gt], + rewrite [pow_succ, -mul_one 1], apply mul_lt_mul xgt1 xige1 zero_lt_one, apply le_of_lt xpos end diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 550def4933..bda0430071 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -30,6 +30,7 @@ import algebra.relation algebra.binary algebra.ordered_ring open eq.ops open prod relation nat open decidable binary +open - [notations] algebra /- the type of integers -/ @@ -54,21 +55,21 @@ definition neg_of_nat : ℕ → ℤ | (succ m) := -[1+ m] definition sub_nat_nat (m n : ℕ) : ℤ := -match n - m with - | 0 := m - n -- m ≥ n - | (succ k) := -[1+ k] -- m < n, and n - m = succ k +match (n - m : nat) with + | 0 := (m - n : nat) -- m ≥ n + | (succ k) := -[1+ k] -- m < n, and n - m = succ k end -definition neg (a : ℤ) : ℤ := +protected definition neg (a : ℤ) : ℤ := int.cases_on a neg_of_nat succ -definition add : ℤ → ℤ → ℤ +protected definition add : ℤ → ℤ → ℤ | (of_nat m) (of_nat n) := m + n | (of_nat m) -[1+ n] := sub_nat_nat m (succ n) | -[1+ m] (of_nat n) := sub_nat_nat n (succ m) | -[1+ m] -[1+ n] := neg_of_nat (succ m + succ n) -definition mul : ℤ → ℤ → ℤ +protected definition mul : ℤ → ℤ → ℤ | (of_nat m) (of_nat n) := m * n | (of_nat m) -[1+ n] := neg_of_nat (m * succ n) | -[1+ m] (of_nat n) := neg_of_nat (succ m * n) @@ -76,11 +77,11 @@ definition mul : ℤ → ℤ → ℤ /- notation -/ -protected definition prio : num := num.pred std.priority.default +protected definition prio : num := num.pred nat.prio -prefix [priority int.prio] - := int.neg -infix [priority int.prio] + := int.add -infix [priority int.prio] * := int.mul +definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add +definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg +definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul /- some basic functions and properties -/ @@ -115,14 +116,14 @@ theorem of_nat_succ (n : ℕ) : of_nat (succ n) = of_nat n + 1 := 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) := -show sub_nat_nat m n = nat.cases_on 0 (m - n) _, from (sub_eq_zero_of_le H) ▸ rfl +show sub_nat_nat m n = nat.cases_on 0 (m - n : nat) _, from (sub_eq_zero_of_le H) ▸ rfl section local attribute sub_nat_nat [reducible] theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) : sub_nat_nat m n = -[1+ pred (n - m)] := -have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹, -show sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (m - n) _, from H1 ▸ rfl +have H1 : n - m = succ (pred (n - m)), from eq.symm (succ_pred_of_pos (sub_pos_of_lt H)), +show sub_nat_nat m n = nat.cases_on (succ (nat.pred (n - m))) (m - n : nat) _, from H1 ▸ rfl end definition nat_abs (a : ℤ) : ℕ := int.cases_on a function.id succ @@ -143,31 +144,31 @@ protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm protected theorem equiv.symm [symm] {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p := calc - pr1 q + pr2 p = pr2 p + pr1 q : add.comm + pr1 q + pr2 p = pr2 p + pr1 q : by rewrite add.comm ... = pr1 p + pr2 q : H⁻¹ - ... = pr2 q + pr1 p : add.comm + ... = pr2 q + pr1 p : by rewrite add.comm protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r := add.cancel_right (calc - pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : add.right_comm + pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite add.right_comm ... = pr2 p + pr1 q + pr2 r : {H1} - ... = pr2 p + (pr1 q + pr2 r) : add.assoc + ... = pr2 p + (pr1 q + pr2 r) : by rewrite add.assoc ... = pr2 p + (pr2 q + pr1 r) : {H2} - ... = pr2 p + pr2 q + pr1 r : add.assoc - ... = pr2 p + pr1 r + pr2 q : add.right_comm) + ... = pr2 p + pr2 q + pr1 r : by rewrite add.assoc + ... = pr2 p + pr1 r + pr2 q : by rewrite add.right_comm) protected theorem equiv_equiv : is_equivalence int.equiv := is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans protected theorem equiv_cases {p q : ℕ × ℕ} (H : p ≡ q) : (pr1 p ≥ pr2 p ∧ pr1 q ≥ pr2 q) ∨ (pr1 p < pr2 p ∧ pr1 q < pr2 q) := -or.elim (@le_or_gt (pr2 p) (pr1 p)) +or.elim (@le_or_gt _ _ (pr2 p) (pr1 p)) (suppose pr1 p ≥ pr2 p, have pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_add_right this (pr2 q), or.inl (and.intro `pr1 p ≥ pr2 p` (le_of_add_le_add_left this))) - (suppose pr1 p < pr2 p, - have pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right this (pr2 q), - or.inr (and.intro `pr1 p < pr2 p` (lt_of_add_lt_add_left this))) + (suppose H₁ : pr1 p < pr2 p, + have pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right H₁ (pr2 q), + or.inr (and.intro H₁ (lt_of_add_lt_add_left this))) protected theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl @@ -208,20 +209,20 @@ or.elim (int.equiv_cases Hequiv) (and.rec (assume (Hp : pr1 p ≥ pr2 p) (Hq : pr1 q ≥ pr2 q), have H : pr1 p - pr2 p = pr1 q - pr2 q, from calc pr1 p - pr2 p - = pr1 p + pr2 q - pr2 q - pr2 p : add_sub_cancel + = pr1 p + pr2 q - pr2 q - pr2 p : by rewrite add_sub_cancel ... = pr2 p + pr1 q - pr2 q - pr2 p : Hequiv ... = pr2 p + (pr1 q - pr2 q) - pr2 p : add_sub_assoc Hq - ... = pr1 q - pr2 q + pr2 p - pr2 p : add.comm - ... = pr1 q - pr2 q : add_sub_cancel, + ... = pr1 q - pr2 q + pr2 p - pr2 p : by rewrite add.comm + ... = pr1 q - pr2 q : by rewrite add_sub_cancel, abstr_of_ge Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_ge Hq)⁻¹)) (and.rec (assume (Hp : pr1 p < pr2 p) (Hq : pr1 q < pr2 q), have H : pr2 p - pr1 p = pr2 q - pr1 q, from calc pr2 p - pr1 p - = pr2 p + pr1 q - pr1 q - pr1 p : add_sub_cancel + = pr2 p + pr1 q - pr1 q - pr1 p : by rewrite add_sub_cancel ... = pr1 p + pr2 q - pr1 q - pr1 p : Hequiv ... = pr1 p + (pr2 q - pr1 q) - pr1 p : add_sub_assoc (le_of_lt Hq) - ... = pr2 q - pr1 q + pr1 p - pr1 p : add.comm - ... = pr2 q - pr1 q : add_sub_cancel, + ... = pr2 q - pr1 q + pr1 p - pr1 p : by rewrite add.comm + ... = pr2 q - pr1 q : by rewrite add_sub_cancel, abstr_of_lt Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_lt Hq)⁻¹)) theorem equiv_iff (p q : ℕ × ℕ) : (p ≡ q) ↔ (abstr p = abstr q) := @@ -280,8 +281,8 @@ definition padd (p q : ℕ × ℕ) : ℕ × ℕ := (pr1 p + pr1 q, pr2 p + pr2 q theorem repr_add : Π (a b : ℤ), repr (add a b) ≡ padd (repr a) (repr b) | (of_nat m) (of_nat n) := !equiv.refl -| (of_nat m) -[1+ n] := (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat -| -[1+ m] (of_nat n) := (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat +| (of_nat m) -[1+ n] := sorry -- begin end -- (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat +| -[1+ m] (of_nat n) := sorry -- begin end -- (!zero_add ▸ rfl)⁻¹ ▸ !repr_sub_nat_nat | -[1+ m] -[1+ n] := !repr_sub_nat_nat theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' := @@ -293,13 +294,13 @@ calc pr1 p + pr1 q + (pr2 p' + pr2 q') theorem padd_comm (p q : ℕ × ℕ) : padd p q = padd q p := calc (pr1 p + pr1 q, pr2 p + pr2 q) - = (pr1 q + pr1 p, pr2 p + pr2 q) : add.comm - ... = (pr1 q + pr1 p, pr2 q + pr2 p) : add.comm + = (pr1 q + pr1 p, pr2 p + pr2 q) : by rewrite add.comm + ... = (pr1 q + pr1 p, pr2 q + pr2 p) : by rewrite (add.comm (pr2 p) (pr2 q)) theorem padd_assoc (p q r : ℕ × ℕ) : padd (padd p q) r = padd p (padd q r) := calc (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r) - = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : add.assoc - ... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : add.assoc + = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : by rewrite add.assoc + ... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : by rewrite add.assoc theorem add.comm (a b : ℤ) : a + b = b + a := eq_of_repr_equiv_repr (equiv.trans !repr_add @@ -349,7 +350,7 @@ calc pr1 p + pr1 q + pr2 q + pr2 p = pr1 p + (pr1 q + pr2 q) + pr2 p : nat.add.assoc ... = pr1 p + (pr1 q + pr2 q + pr2 p) : nat.add.assoc ... = pr1 p + (pr2 q + pr1 q + pr2 p) : nat.add.comm - ... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm + ... = pr1 p + (pr2 q + pr2 p + pr1 q) : by rewrite add.right_comm ... = pr1 p + (pr2 p + pr2 q + pr1 q) : nat.add.comm ... = pr2 p + pr2 q + pr1 q + pr1 p : nat.add.comm @@ -404,16 +405,16 @@ nat.cases_on m rfl (take m', rfl) -- note: we have =, not just ≡ theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b) | (of_nat m) (of_nat n) := calc - (m * n + 0 * 0, m * 0 + 0) = (m * n + 0 * 0, m * 0 + 0 * n) : zero_mul + (m * n + 0 * 0, m * 0 + 0) = (m * n + 0 * 0, m * 0 + 0 * n) : by rewrite *zero_mul | (of_nat m) -[1+ n] := calc - repr (m * -[1+ n]) = (m * 0 + 0, m * succ n + 0 * 0) : repr_neg_of_nat - ... = (m * 0 + 0 * succ n, m * succ n + 0 * 0) : zero_mul + repr ((m : int) * -[1+ n]) = (m * 0 + 0, m * succ n + 0 * 0) : repr_neg_of_nat + ... = (m * 0 + 0 * succ n, m * succ n + 0 * 0) : by rewrite *zero_mul | -[1+ m] (of_nat n) := calc - repr (-[1+ m] * n) = (0 + succ m * 0, succ m * n) : repr_neg_of_nat + repr (-[1+ m] * (n:int)) = (0 + succ m * 0, succ m * n) : repr_neg_of_nat ... = (0 + succ m * 0, 0 + succ m * n) : nat.zero_add - ... = (0 * n + succ m * 0, 0 + succ m * n) : zero_mul + ... = (0 * n + succ m * 0, 0 + succ m * n) : by rewrite zero_mul | -[1+ m] -[1+ n] := calc - (succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : zero_mul + (succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : by rewrite zero_mul ... = (0 + succ m * succ n, 0 * succ n) : nat.zero_add theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ} @@ -421,16 +422,16 @@ theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ} : xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) := nat.add.cancel_right (calc xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn)) - = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : add.comm4 - ... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : nat.add.comm - ... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : !congr_arg2 add.comm4 add.comm4 - ... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) - : by rewrite[-+mul.left_distrib,-+mul.right_distrib]; exact H1 ▸ H2 ▸ rfl - ... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : !congr_arg2 add.comm4 add.comm4 - ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : !nat.add.comm ▸ !nat.add.comm ▸ rfl - ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : add.comm4 - ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : nat.add.comm - ... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : add.comm4) + = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : by rewrite add.comm4 + ... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : by rewrite {xb*ym+yb*xm +_}nat.add.comm + ... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : by exact !congr_arg2 add.comm4 add.comm4 + ... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) : by rewrite[-+mul.left_distrib,-+mul.right_distrib]; exact H1 ▸ H2 ▸ rfl + ... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by exact !congr_arg2 add.comm4 add.comm4 + ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by rewrite {xa*yn + _}nat.add.comm + ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : by rewrite {xb*yn + _}nat.add.comm + ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : by rewrite add.comm4 + ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : by rewrite {xb*xn+yb*yn + _}nat.add.comm + ... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : by rewrite add.comm4) theorem pmul_congr {p p' q q' : ℕ × ℕ} : p ≡ p' → q ≡ q' → pmul p q ≡ pmul p' q' := equiv_mul_prep @@ -498,41 +499,34 @@ assume H : 0 = 1, !succ_ne_zero (of_nat.inj H)⁻¹ theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0) : a = 0 ∨ b = 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 (H ▸ (nat_abs_mul a b)⁻¹)) + (eq_zero_or_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H])) -section migrate_algebra - open [classes] algebra +protected definition integral_domain [reducible] [instance] : algebra.integral_domain int := +⦃algebra.integral_domain, + add := int.add, + add_assoc := add.assoc, + zero := zero, + zero_add := zero_add, + add_zero := add_zero, + neg := int.neg, + add_left_inv := add.left_inv, + add_comm := add.comm, + mul := int.mul, + mul_assoc := mul.assoc, + one := 1, + one_mul := one_mul, + mul_one := mul_one, + left_distrib := mul.left_distrib, + right_distrib := mul.right_distrib, + mul_comm := mul.comm, + zero_ne_one := zero_ne_one, + eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄ - protected definition integral_domain [reducible] : algebra.integral_domain int := - ⦃algebra.integral_domain, - add := add, - add_assoc := add.assoc, - zero := zero, - zero_add := zero_add, - add_zero := add_zero, - neg := neg, - add_left_inv := add.left_inv, - add_comm := add.comm, - mul := mul, - mul_assoc := mul.assoc, - one := 1, - one_mul := one_mul, - mul_one := mul_one, - left_distrib := mul.left_distrib, - right_distrib := mul.right_distrib, - mul_comm := mul.comm, - zero_ne_one := zero_ne_one, - 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 - local attribute int.integral_domain [instance] - definition sub (a b : ℤ) : ℤ := algebra.sub a b - infix [priority int.prio] - := int.sub - definition dvd (a b : ℤ) : Prop := algebra.dvd a b - notation [priority int.prio] a ∣ b := dvd a b - - migrate from algebra with int - replacing sub → sub, dvd → dvd -end migrate_algebra +definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int := +has_dvd.mk algebra.dvd /- additional properties -/ theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : m - n = sub m n := @@ -540,24 +534,28 @@ assert m - n + n = m, from nat.sub_add_cancel H, begin symmetry, apply sub_eq_of_eq_add, - rewrite [-of_nat_add, this] + rewrite this end -- (sub_eq_of_eq_add (!congr_arg (nat.sub_add_cancel H)⁻¹))⁻¹ theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 := -by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add] +by rewrite [neg_succ_of_nat_eq, neg_add] definition succ (a : ℤ) := a + (succ zero) definition pred (a : ℤ) := a - (succ zero) theorem pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel theorem succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel + theorem neg_succ (a : ℤ) : -succ a = pred (-a) := by rewrite [↑succ,neg_add] + theorem succ_neg_succ (a : ℤ) : succ (-succ a) = -a := by rewrite [neg_succ,succ_pred] + theorem neg_pred (a : ℤ) : -pred a = succ (-a) := -by rewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm] +by krewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm] + theorem pred_neg_pred (a : ℤ) : pred (-pred a) = -a := by rewrite [neg_pred,pred_succ] diff --git a/library/data/int/div.lean b/library/data/int/div.lean index 5e88ea0633..aa14b64483 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -9,38 +9,50 @@ Following SSReflect and the SMTlib standard, we define a mod b so that 0 ≤ a m -/ import data.int.order data.nat.div open [coercions] [reduce-hints] nat -open [declarations] nat (succ) +open [declarations] [classes] nat (succ) +open - [notations] algebra open eq.ops namespace int /- definitions -/ -definition divide (a b : ℤ) : ℤ := +protected definition divide (a b : ℤ) : ℤ := sign b * (match a with - | of_nat m := #nat m div (nat_abs b) - | -[1+m] := -[1+ (#nat m div (nat_abs b))] + | of_nat m := (m div (nat_abs b) : nat) + | -[1+m] := -[1+ ((m:nat) div (nat_abs b))] end) -notation [priority int.prio] a div b := divide a b -definition modulo (a b : ℤ) : ℤ := a - a div b * b -notation [priority int.prio] a mod b := modulo a b +definition int_has_divides [reducible] [instance] [priority int.prio] : has_divides int := +has_divides.mk int.divide + +lemma divide_of_nat (a : nat) (b : ℤ) : (of_nat a) div b = sign b * (a div (nat_abs b) : nat) := +rfl + +lemma divide_of_neg_succ (a : nat) (b : ℤ) : -[1+a] div b = sign b * -[1+ (a div (nat_abs b))] := +rfl + +protected definition modulo (a b : ℤ) : ℤ := a - a div b * b + +definition int_has_modulo [reducible] [instance] [priority int.prio] : has_modulo int := +has_modulo.mk int.modulo + notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c /- div -/ -theorem of_nat_div (m n : nat) : of_nat (#nat m div n) = m div n := +theorem of_nat_div (m n : nat) : of_nat (m div n) = m div n := nat.cases_on n - (by rewrite [↑divide, sign_zero, zero_mul, nat.div_zero]) - (take n, by rewrite [↑divide, sign_of_succ, one_mul]) + (begin krewrite [divide_of_nat, sign_zero, zero_mul, nat.div_zero] end) + (take (n : nat), by krewrite [divide_of_nat, sign_of_succ, one_mul]) theorem neg_succ_of_nat_div (m : nat) {b : ℤ} (H : b > 0) : -[1+m] div b = -(m div b + 1) := calc -[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] + ... = -[1+(m div (nat_abs b))] : begin krewrite [sign_of_pos H, one_mul] end + ... = -(m div b + 1) : by krewrite [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] diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 68c535820b..e60a76903a 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -8,19 +8,22 @@ and transfer the results. -/ import .basic algebra.ordered_ring open nat +open - [notations] algebra open decidable open int eq.ops namespace int private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false) -definition le (a b : ℤ) : Prop := nonneg (b - a) -definition lt (a b : ℤ) : Prop := le (a + 1) b +protected definition le (a b : ℤ) : Prop := nonneg (b - a) -infix [priority int.prio] - := int.sub -infix [priority int.prio] <= := int.le -infix [priority int.prio] ≤ := int.le -infix [priority int.prio] < := int.lt +definition int_has_le [instance] [reducible] [priority int.prio]: has_le int := +has_le.mk int.le + +protected definition lt (a b : ℤ) : Prop := (a + 1) ≤ b + +definition int_has_lt [instance] [reducible] [priority int.prio]: has_lt int := +has_lt.mk int.lt local attribute nonneg [reducible] private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := int.cases_on a _ _ @@ -34,7 +37,7 @@ private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) := int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial) theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b := -have n = b - a, from eq_add_neg_of_add_eq (!add.comm ▸ H), +have n = b - a, from eq_add_neg_of_add_eq (begin rewrite [add.comm, H] end), -- !add.comm ▸ H), show nonneg (b - a), from this ▸ trivial theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b := @@ -64,7 +67,7 @@ theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n := le.intro (show a + 1 + n = a + succ n, from calc a + 1 + n = a + (1 + n) : add.assoc - ... = a + (n + 1) : nat.add.comm + ... = a + (n + 1) : by rewrite (add.comm 1 n) ... = a + succ n : rfl) theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b := @@ -191,9 +194,9 @@ le.intro (eq.symm (calc a * b = (0 + n) * b : Hn - ... = n * b : nat.zero_add + ... = n * b : zero_add ... = n * (0 + m) : {Hm⁻¹} - ... = n * m : nat.zero_add + ... = n * m : zero_add ... = 0 + n * m : zero_add)) theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b := @@ -203,15 +206,14 @@ lt.intro (eq.symm (calc a * b = (0 + nat.succ n) * b : Hn - ... = nat.succ n * b : nat.zero_add + ... = nat.succ n * b : zero_add ... = nat.succ n * (0 + nat.succ m) : {Hm⁻¹} - ... = nat.succ n * nat.succ m : nat.zero_add + ... = 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)) - theorem zero_lt_one : (0 : ℤ) < 1 := trivial theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a := @@ -231,61 +233,32 @@ 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)) -section migrate_algebra - open [classes] algebra - - protected definition linear_ordered_comm_ring [reducible] : +protected definition linear_ordered_comm_ring [reducible] [instance] : algebra.linear_ordered_comm_ring int := - ⦃algebra.linear_ordered_comm_ring, int.integral_domain, - le := le, - le_refl := le.refl, - le_trans := @le.trans, - le_antisymm := @le.antisymm, - lt := lt, - le_of_lt := @le_of_lt, - lt_irrefl := lt.irrefl, - lt_of_lt_of_le := @lt_of_lt_of_le, - lt_of_le_of_lt := @lt_of_le_of_lt, - add_le_add_left := @add_le_add_left, - mul_nonneg := @mul_nonneg, - mul_pos := @mul_pos, - le_iff_lt_or_eq := le_iff_lt_or_eq, - le_total := le.total, - zero_ne_one := zero_ne_one, - zero_lt_one := zero_lt_one, - add_lt_add_left := @add_lt_add_left⦄ +⦃algebra.linear_ordered_comm_ring, int.integral_domain, + le := int.le, + le_refl := le.refl, + le_trans := @le.trans, + le_antisymm := @le.antisymm, + lt := int.lt, + le_of_lt := @le_of_lt, + lt_irrefl := lt.irrefl, + lt_of_lt_of_le := @lt_of_lt_of_le, + lt_of_le_of_lt := @lt_of_le_of_lt, + add_le_add_left := @add_le_add_left, + mul_nonneg := @mul_nonneg, + mul_pos := @mul_pos, + le_iff_lt_or_eq := le_iff_lt_or_eq, + le_total := le.total, + zero_ne_one := zero_ne_one, + zero_lt_one := zero_lt_one, + add_lt_add_left := @add_lt_add_left⦄ - protected definition decidable_linear_ordered_comm_ring [reducible] : +protected definition decidable_linear_ordered_comm_ring [reducible] [instance] : algebra.decidable_linear_ordered_comm_ring int := - ⦃algebra.decidable_linear_ordered_comm_ring, - int.linear_ordered_comm_ring, - decidable_lt := decidable_lt⦄ - - local attribute int.integral_domain [instance] - local attribute int.linear_ordered_comm_ring [instance] - local attribute int.decidable_linear_ordered_comm_ring [instance] - - definition ge [reducible] (a b : ℤ) := algebra.has_le.ge a b - definition gt [reducible] (a b : ℤ) := algebra.has_lt.gt a b - infix [priority int.prio] >= := int.ge - infix [priority int.prio] ≥ := int.ge - infix [priority int.prio] > := int.gt - definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) := - show decidable (b ≤ a), from _ - definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := - show decidable (b < a), from _ - definition min : ℤ → ℤ → ℤ := algebra.min - definition max : ℤ → ℤ → ℤ := algebra.max - definition abs : ℤ → ℤ := algebra.abs - definition sign : ℤ → ℤ := algebra.sign - - migrate from algebra with int - replacing dvd → dvd, sub → sub, has_le.ge → ge, has_lt.gt → gt, min → min, max → max, - abs → abs, sign → sign - - attribute le.trans ge.trans lt.trans gt.trans [trans] - attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans] -end migrate_algebra +⦃algebra.decidable_linear_ordered_comm_ring, + int.linear_ordered_comm_ring, + decidable_lt := decidable_lt⦄ /- more facts specific to int -/ @@ -325,12 +298,12 @@ theorem nat_abs_abs (a : ℤ) : nat_abs (abs a) = nat_abs a := abs.by_cases rfl !nat_abs_neg theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b := -obtain n (H1 : a + 1 + n = b), from le.elim H, +obtain (n : nat) (H1 : a + 1 + n = b), from le.elim H, have a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1], lt.intro this theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := -obtain n (H1 : a + succ n = b), from lt.elim H, +obtain (n : nat) (H1 : a + succ n = b), from lt.elim H, have a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1], le.intro this @@ -342,7 +315,7 @@ have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H, le_of_add_le_add_right H1 theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b := -lt_of_add_one_le (!sub_add_cancel⁻¹ ▸ H) +lt_of_add_one_le (begin rewrite algebra.sub_add_cancel, exact H end) theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b := !sub_add_cancel ▸ add_one_le_of_lt H @@ -358,8 +331,8 @@ sign_of_pos (of_nat_pos !nat.succ_pos) 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) + (take (m : nat) H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H)) + (take (m : nat) H, exists.intro m rfl) theorem eq_one_of_mul_eq_one_right {a b : ℤ} (H : a ≥ 0) (H' : a * b = 1) : a = 1 := have a * b > 0, by rewrite H'; apply trivial, @@ -397,13 +370,13 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] cases Hinh with [elt, Helt], existsi b + of_nat (least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b)))), have Heltb : elt > b, begin - apply int.lt_of_not_ge, + apply lt_of_not_ge, intro Hge, apply (Hb _ Hge) Helt end, have H' : P (b + of_nat (nat_abs (elt - b))), begin - rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)), - int.add.comm, int.sub_add_cancel], + rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)), + add.comm, algebra.sub_add_cancel], apply Helt end, apply and.intro, @@ -411,16 +384,16 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] intros z Hz, cases em (z ≤ b) with [Hzb, Hzb], apply Hb _ Hzb, - let Hzb' := int.lt_of_not_ge Hzb, - let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb', + let Hzb' := lt_of_not_ge Hzb, + let Hpos := iff.mpr !sub_pos_iff_lt Hzb', have Hzbk : z = b + of_nat (nat_abs (z - b)), - by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, int.sub_add_cancel], + by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, algebra.sub_add_cancel], have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin - let Hz' := iff.mp !int.lt_add_iff_sub_lt_left Hz, + let Hz' := iff.mp !lt_add_iff_sub_lt_left Hz, rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], apply lt_of_of_nat_lt_of_nat Hz' end, - let Hk' := nat.not_le_of_gt Hk, + let Hk' := algebra.not_le_of_gt Hk, rewrite Hzbk, apply λ p, mt (ge_least_of_lt _ p) Hk', apply nat.lt.trans Hk, @@ -435,13 +408,13 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] cases Hinh with [elt, Helt], existsi b - of_nat (least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt)))), have Heltb : elt < b, begin - apply int.lt_of_not_ge, + apply lt_of_not_ge, intro Hge, apply (Hb _ Hge) Helt end, have H' : P (b - of_nat (nat_abs (b - elt))), begin - rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)), - int.sub_sub_self], + rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)), + sub_sub_self], apply Helt end, apply and.intro, @@ -449,16 +422,16 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] intros z Hz, cases em (z ≥ b) with [Hzb, Hzb], apply Hb _ Hzb, - let Hzb' := int.lt_of_not_ge Hzb, - let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb', + let Hzb' := lt_of_not_ge Hzb, + let Hpos := iff.mpr !sub_pos_iff_lt Hzb', have Hzbk : z = b - of_nat (nat_abs (b - z)), - by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.sub_sub_self], + by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), sub_sub_self], have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin - let Hz' := iff.mp !int.lt_add_iff_sub_lt_left (iff.mpr !int.lt_add_iff_sub_lt_right Hz), + let Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz), rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], apply lt_of_of_nat_lt_of_nat Hz' end, - let Hk' := nat.not_le_of_gt Hk, + let Hk' := algebra.not_le_of_gt Hk, rewrite Hzbk, apply λ p, mt (ge_least_of_lt _ p) Hk', apply nat.lt.trans Hk, diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 90d6b9ee9d..7c6a338aa4 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -7,6 +7,7 @@ Basic properties of lists. -/ import logic tools.helper_tactics data.nat.order open eq.ops helper_tactics nat prod function option +open - [notations] algebra inductive list (T : Type) : Type := | nil {} : list T @@ -70,8 +71,8 @@ theorem length_cons [simp] (x : T) (t : list T) : length (x::t) = length t + 1 theorem length_append [simp] : ∀ (s t : list T), length (s ++ t) = length s + length t | [] t := calc - length ([] ++ t) = length t : rfl - ... = length [] + length t : zero_add + length ([] ++ t) = length t : rfl + ... = length [] + length t : by rewrite [length_nil, zero_add] | (a :: s) t := calc length (a :: s ++ t) = length (s ++ t) + 1 : rfl ... = length s + length t + 1 : length_append diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 6364c0fcb6..4cb8567867 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -211,7 +211,7 @@ nat.induction_on n theorem succ_mul [simp] (n m : ℕ) : (succ n) * m = (n * m) + m := nat.induction_on m - (!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹) + (by rewrite mul_zero) (take k IH, calc succ n * succ k = succ n * k + succ n : mul_succ ... = n * k + k + succ n : IH @@ -289,35 +289,31 @@ nat.cases_on n ... = succ (succ n' * m' + n') : add_succ)⁻¹ !succ_ne_zero)) -section migrate_algebra - open [classes] algebra +open - [notations] algebra +protected definition comm_semiring [reducible] [instance] : algebra.comm_semiring nat := +⦃algebra.comm_semiring, + add := nat.add, + add_assoc := add.assoc, + zero := nat.zero, + zero_add := zero_add, + add_zero := add_zero, + add_comm := add.comm, + mul := nat.mul, + mul_assoc := mul.assoc, + one := nat.succ nat.zero, + one_mul := one_mul, + mul_one := mul_one, + left_distrib := mul.left_distrib, + right_distrib := mul.right_distrib, + zero_mul := zero_mul, + mul_zero := mul_zero, + mul_comm := mul.comm⦄ - protected definition comm_semiring [reducible] : algebra.comm_semiring nat := - ⦃algebra.comm_semiring, - add := add, - add_assoc := add.assoc, - zero := zero, - zero_add := zero_add, - add_zero := add_zero, - add_comm := add.comm, - mul := mul, - mul_assoc := mul.assoc, - one := succ zero, - one_mul := one_mul, - mul_one := mul_one, - left_distrib := mul.left_distrib, - right_distrib := mul.right_distrib, - zero_mul := zero_mul, - mul_zero := mul_zero, - mul_comm := mul.comm⦄ +definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat := +has_zero.mk zero - local attribute nat.comm_semiring [instance] - definition dvd (a b : ℕ) : Prop := algebra.dvd a b - notation a ∣ b := dvd a b - - migrate from algebra with nat replacing dvd → dvd - -end migrate_algebra +definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat := +has_one.mk (succ zero) end nat section diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 211cfa466d..9506ab50af 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -7,6 +7,7 @@ Definitions and properties of div and mod. Much of the development follows Isabe -/ import data.nat.sub open eq.ops well_founded decidable prod +open - [notations] algebra namespace nat @@ -20,7 +21,9 @@ private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero definition divide := fix div.F -notation a div b := divide a b + +definition nat_has_divides [reducible] [instance] [priority nat.prio] : has_divides nat := +has_divides.mk 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 @@ -76,8 +79,11 @@ theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n := private definition mod.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 else x -definition modulo := fix mod.F -notation a mod b := modulo a b +protected definition modulo := fix mod.F + +definition nat_has_modulo [reducible] [instance] [priority nat.prio] : has_modulo nat := +has_modulo.mk nat.modulo + notation a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c theorem modulo_def (x y : nat) : modulo x y = if 0 < y ∧ y ≤ x then modulo (x - y) y else x := @@ -150,41 +156,44 @@ have H1 : n mod 1 < 1, from !mod_lt !succ_pos, eq_zero_of_le_zero (le_of_lt_succ H1) /- properties of div and mod -/ +set_option pp.all true -- the quotient / remainder theorem theorem eq_div_mul_add_mod (x y : ℕ) : x = x div y * y + x mod y := -by_cases_zero_pos y - (show x = x div 0 * 0 + x mod 0, from +begin + eapply by_cases_zero_pos y, + show x = x div 0 * 0 + x mod 0, from (calc x div 0 * 0 + x mod 0 = 0 + x mod 0 : mul_zero ... = x mod 0 : zero_add - ... = x : mod_zero)⁻¹) - (take y, - assume H : y > 0, - show x = x div y * y + x mod y, from - nat.case_strong_induction_on x - (show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, zero_div, zero_mul]) - (take x, - assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y, - show succ x = succ x div y * y + succ x mod y, from - if H1 : succ x < y then - have H2 : succ x div y = 0, from div_eq_zero_of_lt H1, - have H3 : succ x mod y = succ x, from mod_eq_of_lt H1, - H2⁻¹ ▸ H3⁻¹ ▸ !zero_mul⁻¹ ▸ !zero_add⁻¹ - else - have H2 : y ≤ succ x, from le_of_not_gt H1, - have H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2, - have H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2, - have H5 : succ x - y < succ x, from sub_lt !succ_pos H, - have H6 : succ x - y ≤ x, from le_of_lt_succ H5, - (calc - succ x div y * y + succ x mod y = - succ ((succ x - y) div y) * y + succ x mod y : H3 - ... = ((succ x - y) div y) * y + y + succ x mod y : succ_mul - ... = ((succ x - y) div y) * y + y + (succ x - y) mod y : H4 - ... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm - ... = succ x - y + y : {!(IH _ H6)⁻¹} - ... = succ x : sub_add_cancel H2)⁻¹)) + ... = x : mod_zero)⁻¹, + intro y H, + show x = x div y * y + x mod y, + begin + eapply nat.case_strong_induction_on x, + show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, zero_div, zero_mul], + intro x IH, + show succ x = succ x div y * y + succ x mod y, from + if H1 : succ x < y then + assert H2 : succ x div y = 0, from div_eq_zero_of_lt H1, + assert H3 : succ x mod y = succ x, from mod_eq_of_lt H1, + begin rewrite [H2, H3, zero_mul, zero_add] end + else + have H2 : y ≤ succ x, from le_of_not_gt H1, + assert H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2, + assert H4 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2, + have H5 : succ x - y < succ x, from sub_lt !succ_pos H, + assert H6 : succ x - y ≤ x, from le_of_lt_succ H5, + (calc + succ x div y * y + succ x mod y = + succ ((succ x - y) div y) * y + succ x mod y : by rewrite H3 + ... = ((succ x - y) div y) * y + y + succ x mod y : by rewrite succ_mul + ... = ((succ x - y) div y) * y + y + (succ x - y) mod y : by rewrite H4 + ... = ((succ x - y) div y) * y + (succ x - y) mod y + y : add.right_comm + ... = succ x - y + y : by rewrite -(IH _ H6) + ... = succ x : sub_add_cancel H2)⁻¹ + end +end theorem mod_eq_sub_div_mul (x y : ℕ) : x mod y = x - x div y * y := eq_sub_of_add_eq (!add.comm ▸ !eq_div_mul_add_mod)⁻¹ @@ -244,7 +253,8 @@ have H6 : y > 0, from lt_of_le_of_lt !zero_le H1, show q1 = q2, from eq_of_mul_eq_mul_right H6 H5 theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y := -if H : y = 0 then H⁻¹ ▸ !mul_zero⁻¹ ▸ !div_zero⁻¹ ▸ !div_zero +if H : y = 0 then + by rewrite [H, mul_zero, *div_zero] else have ypos : y > 0, from pos_of_ne_zero H, have zypos : z * y > 0, from mul_pos zpos ypos, @@ -533,15 +543,16 @@ iff.mp (!div_le_iff_le_mul_of_div H1 H2) H3 -- needed for integer division theorem mul_sub_div_of_lt {m n k : ℕ} (H : k < m * n) : (m * n - (k + 1)) div m = n - k div m - 1 := -have H1 : k div m < n, from div_lt_of_lt_mul (!mul.comm ▸ H), -have H2 : n - k div m ≥ 1, from - le_sub_of_add_le (calc - 1 + k div m = succ (k div m) : add.comm - ... ≤ n : succ_le_of_lt H1), -assert H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹, -assert H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)), -have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4), -assert H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos, +begin + have H1 : k div m < n, from div_lt_of_lt_mul (!mul.comm ▸ H), + have H2 : n - k div m ≥ 1, from + le_sub_of_add_le (calc + 1 + k div m = succ (k div m) : add.comm + ... ≤ n : succ_le_of_lt H1), + have H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹, + have H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)), + have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4), + have H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos, calc (m * n - (k + 1)) div m = (m * n - (k div m * m + k mod m + 1)) div m : eq_div_mul_add_mod ... = (m * n - k div m * m - (k mod m + 1)) div m : by rewrite [*sub_sub] @@ -554,7 +565,7 @@ calc by rewrite [add.comm, (add_mul_div_self H4)] ... = n - k div m - 1 : by rewrite [div_eq_zero_of_lt H6, zero_add] - +end private lemma div_div_aux (a b c : nat) : b > 0 → c > 0 → (a div b) div c = a div (b * c) := suppose b > 0, suppose c > 0, diff --git a/library/data/nat/fact.lean b/library/data/nat/fact.lean index 8e5c4d43b9..17f116055d 100644 --- a/library/data/nat/fact.lean +++ b/library/data/nat/fact.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura Factorial -/ import data.nat.div +open - [notations] algebra namespace nat definition fact : nat → nat diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index f9f6de6d76..f6f3ad56b8 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -7,6 +7,7 @@ Definitions and properties of gcd, lcm, and coprime. -/ import .div open eq.ops well_founded decidable prod +open - [notations] algebra namespace nat @@ -341,7 +342,7 @@ theorem comprime_one_left : ∀ n, coprime 1 n := theorem comprime_one_right : ∀ n, coprime n 1 := λ n, !gcd_one_right -theorem exists_eq_prod_and_dvd_and_dvd {m n k} (H : k ∣ m * n) : +theorem exists_eq_prod_and_dvd_and_dvd {m n k : nat} (H : k ∣ m * n) : ∃ m' n', k = m' * n' ∧ m' ∣ m ∧ n' ∣ n := or.elim (eq_zero_or_pos (gcd k m)) (assume H1 : gcd k m = 0, diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 85595c613c..00f62ab2e1 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -135,92 +135,72 @@ else (eq_max_left h) ▸ !le.refl /- nat is an instance of a linearly ordered semiring and a lattice -/ -section migrate_algebra - open [classes] algebra - local attribute nat.comm_semiring [instance] +open -[notations] algebra - protected definition decidable_linear_ordered_semiring [reducible] : - algebra.decidable_linear_ordered_semiring nat := - ⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring, - add_left_cancel := @add.cancel_left, - add_right_cancel := @add.cancel_right, - lt := lt, - le := le, - le_refl := le.refl, - le_trans := @le.trans, - le_antisymm := @le.antisymm, - le_total := @le.total, - le_iff_lt_or_eq := @le_iff_lt_or_eq, - le_of_lt := @le_of_lt, - lt_irrefl := @lt.irrefl, - lt_of_lt_of_le := @lt_of_lt_of_le, - lt_of_le_of_lt := @lt_of_le_of_lt, - lt_of_add_lt_add_left := @lt_of_add_lt_add_left, - add_lt_add_left := @add_lt_add_left, - add_le_add_left := @add_le_add_left, - le_of_add_le_add_left := @le_of_add_le_add_left, - zero_lt_one := zero_lt_succ 0, - mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1), - mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1), - mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left, - mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right, - decidable_lt := nat.decidable_lt ⦄ +protected definition decidable_linear_ordered_semiring [reducible] [instance] : +algebra.decidable_linear_ordered_semiring nat := +⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring, + add_left_cancel := @add.cancel_left, + add_right_cancel := @add.cancel_right, + lt := nat.lt, + le := nat.le, + le_refl := le.refl, + le_trans := @le.trans, + le_antisymm := @le.antisymm, + le_total := @le.total, + le_iff_lt_or_eq := @le_iff_lt_or_eq, + le_of_lt := @le_of_lt, + lt_irrefl := @lt.irrefl, + lt_of_lt_of_le := @lt_of_lt_of_le, + lt_of_le_of_lt := @lt_of_le_of_lt, + lt_of_add_lt_add_left := @lt_of_add_lt_add_left, + add_lt_add_left := @add_lt_add_left, + add_le_add_left := @add_le_add_left, + le_of_add_le_add_left := @le_of_add_le_add_left, + zero_lt_one := zero_lt_succ 0, + mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left c H1), + mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right c H1), + mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left, + mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right, + decidable_lt := nat.decidable_lt ⦄ -/- - protected definition lattice [reducible] : algebra.lattice nat := - ⦃ algebra.lattice, nat.linear_ordered_semiring, - min := min, - max := max, - min_le_left := min_le_left, - min_le_right := min_le_right, - le_min := @le_min, - le_max_left := le_max_left, - le_max_right := le_max_right, - max_le := @max_le ⦄ - local attribute nat.linear_ordered_semiring [instance] - local attribute nat.lattice [instance] --/ - local attribute nat.decidable_linear_ordered_semiring [instance] +definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat := +has_dvd.mk algebra.dvd - definition min : ℕ → ℕ → ℕ := algebra.min - definition max : ℕ → ℕ → ℕ := algebra.max +theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b := +@algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le - migrate from algebra with nat - replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, min → min, max → max - hiding add_pos_of_pos_of_nonneg, add_pos_of_nonneg_of_pos, - add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le, - le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg, - lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right, - mul_lt_mul +theorem add_pos_right {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < b + a := +by rewrite add.comm; apply add_pos_left H b - attribute le.trans ge.trans lt.trans gt.trans [trans] - attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans] +theorem add_eq_zero_iff_eq_zero_and_eq_zero {a b : ℕ} : +a + b = 0 ↔ a = 0 ∧ b = 0 := +@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le - theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b := - @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le - theorem add_pos_right {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < b + a := - !add.comm ▸ add_pos_left H b - theorem add_eq_zero_iff_eq_zero_and_eq_zero {a b : ℕ} : - a + b = 0 ↔ a = 0 ∧ b = 0 := - @algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le - theorem le_add_of_le_left {a b c : ℕ} (H : b ≤ c) : b ≤ a + c := - @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H - theorem le_add_of_le_right {a b c : ℕ} (H : b ≤ c) : b ≤ c + a := - @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le - theorem lt_add_of_lt_left {b c : ℕ} (H : b < c) (a : ℕ) : b < a + c := - @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H - theorem lt_add_of_lt_right {b c : ℕ} (H : b < c) (a : ℕ) : b < c + a := - @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le - theorem lt_of_mul_lt_mul_left {a b c : ℕ} (H : c * a < c * b) : a < b := - @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le - theorem lt_of_mul_lt_mul_right {a b c : ℕ} (H : a * c < b * c) : a < b := - @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le - theorem pos_of_mul_pos_left {a b : ℕ} (H : 0 < a * b) : 0 < b := - @algebra.pos_of_mul_pos_left _ _ a b H !zero_le - theorem pos_of_mul_pos_right {a b : ℕ} (H : 0 < a * b) : 0 < a := - @algebra.pos_of_mul_pos_right _ _ a b H !zero_le -end migrate_algebra +theorem le_add_of_le_left {a b c : ℕ} (H : b ≤ c) : b ≤ a + c := +@algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H + +theorem le_add_of_le_right {a b c : ℕ} (H : b ≤ c) : b ≤ c + a := +@algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le + +theorem lt_add_of_lt_left {b c : ℕ} (H : b < c) (a : ℕ) : b < a + c := +@algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H + +theorem lt_add_of_lt_right {b c : ℕ} (H : b < c) (a : ℕ) : b < c + a := +@algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le + +theorem lt_of_mul_lt_mul_left {a b c : ℕ} (H : c * a < c * b) : a < b := +@algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le + +theorem lt_of_mul_lt_mul_right {a b c : ℕ} (H : a * c < b * c) : a < b := +@algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le + +theorem pos_of_mul_pos_left {a b : ℕ} (H : 0 < a * b) : 0 < b := +@algebra.pos_of_mul_pos_left _ _ a b H !zero_le + +theorem pos_of_mul_pos_right {a b : ℕ} (H : 0 < a * b) : 0 < a := +@algebra.pos_of_mul_pos_right _ _ a b H !zero_le theorem zero_le_one : 0 ≤ 1 := dec_trivial diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean index b2f6f40486..60a16db19e 100644 --- a/library/data/nat/pairing.lean +++ b/library/data/nat/pairing.lean @@ -7,6 +7,7 @@ Elegant pairing function. -/ import data.nat.sqrt data.nat.div open prod decidable +open - [notations] algebra namespace nat definition mkpair (a b : nat) : nat := diff --git a/library/data/nat/sqrt.lean b/library/data/nat/sqrt.lean index 3fdcde4a09..da33ab1f78 100644 --- a/library/data/nat/sqrt.lean +++ b/library/data/nat/sqrt.lean @@ -10,6 +10,7 @@ import data.nat.order data.nat.sub namespace nat open decidable +open - [notations] algebra -- This is the simplest possible function that just performs a linear search definition sqrt_aux : nat → nat → nat diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 36837dc92d..102eda8b48 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -50,7 +50,7 @@ theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m := theorem add_sub_cancel (n m : ℕ) : n + m - m = n := nat.induction_on m - (!add_zero⁻¹ ▸ !sub_zero) + (begin rewrite add_zero end) (take k : ℕ, assume IH : n + k - k = n, calc @@ -72,7 +72,7 @@ nat.induction_on k n - m - succ l = pred (n - m - l) : !sub_succ ... = pred (n - (m + l)) : IH ... = n - succ (m + l) : sub_succ - ... = n - (m + succ l) : {!add_succ⁻¹}) + ... = n - (m + succ l) : by rewrite add_succ) theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k := calc @@ -206,7 +206,7 @@ theorem exists_sub_eq_of_le {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n := obtain (k : ℕ) (Hk : n + k = m), from le.elim H, exists.intro k (calc - m - k = n + k - k : Hk⁻¹ + m - k = n + k - k : by rewrite Hk ... = n : add_sub_cancel) theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) := @@ -289,9 +289,11 @@ sub.cases ... = k - n + n : sub_add_cancel H3, le.intro (add.cancel_right H4)) +open -[notations] algebra + theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 := -have H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹, -have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H, +assert H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹, +have H2 : 0 + m < n - m + m, begin rewrite [zero_add, -H1], exact H end, !lt_of_add_lt_add_right H2 theorem lt_of_sub_pos {m n : ℕ} (H : n - m > 0) : m < n := @@ -319,9 +321,9 @@ sub.cases assume Hmn : m + mn = n, sub.cases (assume H : m ≤ k, - have H2 : n - k ≤ n - m, from sub_le_sub_left H n, - have H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2, - show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3) + have H2 : n - k ≤ n - m, from sub_le_sub_left H n, + assert H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2, + show n - k ≤ mn + 0, begin rewrite add_zero, assumption end) (take km : ℕ, assume Hkm : k + km = m, have H : k + (mn + km) = n, from @@ -444,7 +446,9 @@ theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) : theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k := have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)), -from (!add.comm ▸ !add.left_comm ▸ !add.assoc) ⬝ !add.assoc⁻¹, +begin rewrite [add.comm (k - m) (m - n), + {n - m + _ + _}add.assoc, + {m - k + _}add.left_comm, -add.assoc] end, this ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l := @@ -457,7 +461,7 @@ assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl, by rewrite [this, this n m, mul.right_distrib, *mul_sub_right_distrib] theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m := -!mul.comm ▸ !mul.comm ▸ !dist_mul_right ⬝ !mul.comm +begin rewrite [mul.comm k n, mul.comm k m, dist_mul_right, mul.comm] end theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) := have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean index 4122e004f4..ba25b02221 100644 --- a/library/data/quotient/util.lean +++ b/library/data/quotient/util.lean @@ -78,7 +78,7 @@ namespace quotient theorem map_pair2_comm {A B : Type} {f : A → A → B} (Hcomm : ∀a b : A, f a b = f b a) : Π (v w : A × A), map_pair2 f v w = map_pair2 f w v | (pair v₁ v₂) (pair w₁ w₂) := - !map_pair2_pair ⬝ by rewrite [Hcomm v₁ w₁, Hcomm v₂ w₂] ⬝ !map_pair2_pair⁻¹ + !map_pair2_pair ⬝ by rewrite [Hcomm v₁ w₁, Hcomm v₂ w₂] ⬝ (eq.symm !map_pair2_pair) theorem map_pair2_assoc {A : Type} {f : A → A → A} (Hassoc : ∀a b c : A, f (f a b) c = f a (f b c)) (u v w : A × A) : diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 4cf25c0f9a..a28979563b 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -6,7 +6,8 @@ Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn Sigma types, aka dependent sum. -/ import logic.cast -open inhabited eq.ops sigma.ops +open inhabited sigma.ops +override eq.ops namespace sigma universe variables u v diff --git a/library/init/nat.lean b/library/init/nat.lean index 584d251ade..eb9f51f325 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -16,29 +16,30 @@ namespace nat | refl : le a a | step : Π {b}, le a b → le a (succ b) - infix ≤ := le - attribute le.refl [refl] + definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le - definition lt [reducible] (n m : ℕ) := succ n ≤ m - definition ge [reducible] (n m : ℕ) := m ≤ n - definition gt [reducible] (n m : ℕ) := succ m ≤ n - infix < := lt - infix ≥ := ge - infix > := gt + lemma le_refl [refl] : ∀ a : nat, a ≤ a := + le.refl + + protected definition lt [reducible] (n m : ℕ) := succ n ≤ m + definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt definition pred [unfold 1] (a : nat) : nat := nat.cases_on a zero (λ a₁, a₁) -- add is defined in init.num - definition sub (a b : nat) : nat := + protected definition sub (a b : nat) : nat := nat.rec_on b a (λ b₁, pred) - definition mul (a b : nat) : nat := + protected definition mul (a b : nat) : nat := nat.rec_on b zero (λ b₁ r, r + a) - notation a - b := sub a b - notation a * b := mul a b + definition nat_has_sub [instance] [reducible] [priority nat.prio] : has_sub nat := + has_sub.mk nat.sub + + definition nat_has_mul [instance] [reducible] [priority nat.prio] : has_mul nat := + has_mul.mk nat.mul /- properties of ℕ -/ @@ -182,15 +183,14 @@ namespace nat theorem lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b := le_of_succ_le_succ - definition decidable_le [instance] : decidable_rel le := + definition decidable_le [instance] : ∀ a b : nat, decidable (a ≤ b) := nat.rec (λm, (decidable.inl !zero_le)) (λn IH m, !nat.cases_on (decidable.inr (not_succ_le_zero n)) (λm, decidable.rec (λH, inl (succ_le_succ H)) (λH, inr (λa, H (le_of_succ_le_succ a))) (IH m))) - definition decidable_lt [instance] : decidable_rel lt := _ - definition decidable_gt [instance] : decidable_rel gt := _ - definition decidable_ge [instance] : decidable_rel ge := _ + definition decidable_lt [instance] : ∀ a b : nat, decidable (a < b) := + λ a b, decidable_le (succ a) b theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b := nat.rec (inr !zero_le) (λn, or.rec @@ -220,7 +220,7 @@ namespace nat theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h theorem succ_sub_succ_eq_sub [simp] (a b : ℕ) : succ a - succ b = a - b := - nat.rec rfl (λ b, congr_arg pred) b + nat.rec (by esimp) (λ b, congr_arg pred) b theorem sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := eq.symm !succ_sub_succ_eq_sub @@ -248,9 +248,3 @@ namespace nat theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true := iff_true_intro !sub_lt_succ end nat - -namespace nat_esimp - open nat - attribute add mul sub [unfold 2] - attribute of_num [unfold 1] -end nat_esimp diff --git a/library/init/num.lean b/library/init/num.lean index 2884e7da22..7c4207aa5c 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude -import init.logic init.bool +import init.logic init.bool init.priority open bool definition pos_num.is_inhabited [instance] : inhabited pos_num := @@ -117,11 +117,12 @@ end num -- the coercion from num to nat is defined here, -- so that it can already be used in init.tactic namespace nat + protected definition prio := num.add std.priority.default 100 - definition add (a b : nat) : nat := + protected definition add (a b : nat) : nat := nat.rec_on b a (λ b₁ r, succ r) - notation a + b := add a b + definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat := has_add.mk nat.add definition of_num [coercion] (n : num) : nat := num.rec zero diff --git a/library/init/prod.lean b/library/init/prod.lean index 275505d16b..6085c43c73 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -12,12 +12,6 @@ notation A × B := prod A B notation `(` h `, ` t:(foldl `, ` (e r, prod.mk r e) h) `)` := t namespace prod - notation [parsing-only] A * B := prod A B - namespace low_precedence_times - reserve infixr [parsing-only] `*`:30 -- conflicts with notation for multiplication - infixr `*` := prod - end low_precedence_times - notation `pr₁` := pr1 notation `pr₂` := pr2 diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 41f4ea2020..899c930aa5 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -95,3 +95,43 @@ reserve infix ` ⊇ `:50 reserve infix ` ∣ `:50 reserve infixl ` ++ `:65 reserve infixr ` :: `:65 + +structure has_add [class] (A : Type) := (add : A → A → A) +structure has_mul [class] (A : Type) := (mul : A → A → A) +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_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) +structure has_lt [class] (A : Type) := (lt : A → A → Prop) + +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 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 +definition inv {A : Type} [s : has_inv A] : A → A := has_inv.inv +definition le {A : Type} [s : has_le A] : A → A → Prop := has_le.le +definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt +definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a +definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a + +infix + := add +infix * := mul +infix - := sub +infix / := division +infix div := divides +infix ∣ := dvd +infix mod := modulo +prefix - := neg +postfix ⁻¹ := inv +infix ≤ := le +infix ≥ := ge +infix < := lt +infix > := gt diff --git a/library/init/wf.lean b/library/init/wf.lean index 34b62313e1..979e586e84 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -131,8 +131,8 @@ section definition accessible {z} (ac: acc R z) : acc R⁺ z := begin induction ac with x acx ih, - constructor, intro y lt, - induction lt with a b rab a b c rab rbc ih₁ ih₂, + constructor, intro y rel, + induction rel with a b rab a b c rab rbc ih₁ ih₂, {exact ih a rab}, {exact acc.inv (ih₂ acx ih) rab} end diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f3bab8199a..a8224f395b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1551,10 +1551,10 @@ expr parser::parse_numeral_expr(bool user_notation) { "(solution: use 'import data.num', or define notation for the given numeral)", p); } buffer cs; - if (*m_has_num) - cs.push_back(save_pos(copy(from_num(n)), p)); for (expr const & c : vals) cs.push_back(copy_with_new_pos(c, p)); + if (*m_has_num) + cs.push_back(save_pos(copy(from_num(n)), p)); // Remark: choices are processed from right to left. // We want to process user provided notation before the default 'num'. lean_assert(!cs.empty());