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());