diff --git a/doc/lean/calc.org b/doc/lean/calc.org index cf3da91e6..3864ec4fe 100644 --- a/doc/lean/calc.org +++ b/doc/lean/calc.org @@ -37,7 +37,7 @@ Here is an example := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : add_comm + ... = 1 + d : add.comm d 1 ... = e : eq.symm Ax4. #+END_SRC @@ -47,8 +47,7 @@ We can use =by = or =by = to (try to) automatically construct th proof expression using the given tactic or solver. Even when tactics and solvers are not used, we can still use the elaboration engine to fill -gaps in our calculational proofs. In the previous examples, the arguments for the -=add_comm= theorem are implicit. The Lean elaboration engine infers them automatically for us. +gaps in our calculational proofs. The Lean elaboration engine infers them automatically for us. The =calc= command can be configured for any relation that supports some form of transitivity. It can even combine different relations. @@ -60,7 +59,7 @@ some form of transitivity. It can even combine different relations. theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 := calc a = b : H1 ... = c + 1 : H2 - ... = succ c : add_one + ... = succ c : add.one c ... ≠ 0 : succ_ne_zero #+END_SRC diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index c31aed13f..03bcd8da2 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -760,7 +760,7 @@ of two even numbers is an even number. exists_intro (w1 + w2) (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} - ... = 2*(w1 + w2) : eq.symm mul_distr_left))) + ... = 2*(w1 + w2) : eq.symm !mul.distr_left))) #+END_SRC @@ -780,5 +780,5 @@ With this macro we can write the example above in a more natural way exists_intro (w1 + w2) (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} - ... = 2*(w1 + w2) : eq.symm mul_distr_left) + ... = 2*(w1 + w2) : eq.symm !mul.distr_left) #+END_SRC diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index bf6955508..943a5770b 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -28,13 +28,13 @@ H -- add_rewrite rel_comp --local theorem rel_refl {a : ℕ × ℕ} : rel a a := -add_comm +!add.comm theorem rel_symm {a b : ℕ × ℕ} (H : rel a b) : rel b a := calc - pr1 b + pr2 a = pr2 a + pr1 b : add_comm + pr1 b + pr2 a = pr2 a + pr1 b : !add.comm ... = pr1 a + pr2 b : H⁻¹ - ... = pr2 b + pr1 a : add_comm + ... = pr2 b + pr1 a : !add.comm theorem rel_trans {a b c : ℕ × ℕ} (H1 : rel a b) (H2 : rel b c) : rel a c := have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from @@ -44,7 +44,7 @@ have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from ... = pr2 a + (pr1 b + pr2 c) : by simp ... = pr2 a + (pr2 b + pr1 c) : {H2} ... = pr2 a + pr1 c + pr2 b : by simp, -show pr1 a + pr2 c = pr2 a + pr1 c, from add_cancel_right H3 +show pr1 a + pr2 c = pr2 a + pr1 c, from add.cancel_right H3 theorem rel_equiv : is_equivalence rel := is_equivalence.mk @@ -133,14 +133,14 @@ or.elim le_total (assume H : pr2 a ≤ pr1 a, calc pr1 a + pr2 (proj a) = pr1 a + 0 : {proj_ge_pr2 H} - ... = pr1 a : add_zero_right + ... = pr1 a : !add.zero_right ... = pr2 a + (pr1 a - pr2 a) : (add_sub_le H)⁻¹ ... = pr2 a + pr1 (proj a) : {(proj_ge_pr1 H)⁻¹}) (assume H : pr1 a ≤ pr2 a, calc pr1 a + pr2 (proj a) = pr1 a + (pr2 a - pr1 a) : {proj_le_pr2 H} ... = pr2 a : add_sub_le H - ... = pr2 a + 0 : add_zero_right⁻¹ + ... = pr2 a + 0 : !add.zero_right⁻¹ ... = pr2 a + pr1 (proj a) : {(proj_le_pr1 H)⁻¹}) theorem proj_congr {a b : ℕ × ℕ} (H : rel a b) : proj a = proj b := @@ -296,7 +296,7 @@ have H5 : n + m = 0, from n + m = pr1 (pair n 0) + pr2 (pair 0 m) : by simp ... = pr2 (pair n 0) + pr1 (pair 0 m) : H4 ... = 0 : by simp, - add_eq_zero H5 + add.eq_zero H5 -- add_rewrite to_nat_neg @@ -591,7 +591,7 @@ have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * x : by simp ... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)) : by simp, -nat.add_cancel_right H3 +nat.add.cancel_right H3 theorem rel_mul {u u' v v' : ℕ × ℕ} (H1 : rel u u') (H2 : rel v v') : rel (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v)) @@ -713,7 +713,7 @@ have H2 : (to_nat a) * (to_nat b) = 0, from (to_nat a) * (to_nat b) = (to_nat (a * b)) : (mul_to_nat a b)⁻¹ ... = (to_nat 0) : {H} ... = 0 : to_nat_of_nat 0, -have H3 : (to_nat a) = 0 ∨ (to_nat b) = 0, from mul_eq_zero H2, +have H3 : (to_nat a) = 0 ∨ (to_nat b) = 0, from mul.eq_zero H2, or.imp_or H3 (assume H : (to_nat a) = 0, to_nat_eq_zero H) (assume H : (to_nat b) = 0, to_nat_eq_zero H) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index b6a9aa8fe..ab2a39c3e 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -66,7 +66,7 @@ have H3 : a + of_nat (n + m) = a + 0, from ... = a + 0 : (add_zero_right a)⁻¹, have H4 : of_nat (n + m) = of_nat 0, from add_cancel_left H3, have H5 : n + m = 0, from of_nat_inj H4, -have H6 : n = 0, from nat.add_eq_zero_left H5, +have H6 : n = 0, from nat.add.eq_zero_left H5, show a = b, from calc a = a + of_nat 0 : (add_zero_right a)⁻¹ diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index dda560970..bbcd056b1 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -73,7 +73,7 @@ theorem length_nil : length (@nil T) = 0 theorem length_cons {x : T} {t : list T} : length (x::t) = succ (length t) theorem length_append {s t : list T} : length (s ++ t) = length s + length t := -induction_on s (add_zero_left⁻¹) (λx s H, add_succ_left⁻¹ ▸ H ▸ rfl) +induction_on s (!add.zero_left⁻¹) (λx s H, !add.succ_left⁻¹ ▸ H ▸ rfl) -- add_rewrite length_nil length_cons diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 01d4e1af3..7cd93bb43 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -68,9 +68,9 @@ absurd H2 true_ne_false definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n -theorem pred_zero : pred 0 = 0 +theorem pred.zero : pred 0 = 0 -theorem pred_succ {n : ℕ} : pred (succ n) = n +theorem pred.succ (n : ℕ) : pred (succ n) = n irreducible pred @@ -78,7 +78,7 @@ theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n (or.inl rfl) (take m IH, or.inr - (show succ m = succ (pred (succ m)), from congr_arg succ pred_succ⁻¹)) + (show succ m = succ (pred (succ m)), from congr_arg succ !pred.succ⁻¹)) theorem zero_or_exists_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k := or.imp_or (zero_or_succ_pred n) (assume H, H) @@ -92,18 +92,18 @@ or.elim (zero_or_succ_pred n) (take H3 : n = 0, H1 H3) (take H3 : n = succ (pred n), H2 (pred n) H3) -theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m := +theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m := calc - n = pred (succ n) : pred_succ⁻¹ + n = pred (succ n) : !pred.succ⁻¹ ... = pred (succ m) : {H} - ... = m : pred_succ + ... = m : !pred.succ -theorem succ_ne_self {n : ℕ} : succ n ≠ n := +theorem succ.ne_self {n : ℕ} : succ n ≠ n := induction_on n (take H : 1 = 0, have ne : 1 ≠ 0, from succ_ne_zero, absurd H ne) - (take k IH H, IH (succ_inj H)) + (take k IH H, IH (succ.inj H)) protected definition has_decidable_eq [instance] : decidable_eq ℕ := take n m : ℕ, @@ -121,7 +121,7 @@ have general : ∀n, decidable (n = m), from (assume Heq : n' = m', inl (congr_arg succ Heq)) (assume Hne : n' ≠ m', have H1 : succ n' ≠ succ m', from - assume Heq, absurd (succ_inj Heq) Hne, + assume Heq, absurd (succ.inj Heq) Hne, inr H1))), general n @@ -150,110 +150,106 @@ general m -- Addition -- -------- -theorem add_zero_right {n : ℕ} : n + 0 = n +theorem add.zero_right (n : ℕ) : n + 0 = n -theorem add_succ_right {n m : ℕ} : n + succ m = succ (n + m) +theorem add.succ_right (n m : ℕ) : n + succ m = succ (n + m) irreducible add -theorem add_zero_left {n : ℕ} : 0 + n = n := +theorem add.zero_left (n : ℕ) : 0 + n = n := induction_on n - add_zero_right + !add.zero_right (take m IH, show 0 + succ m = succ m, from calc - 0 + succ m = succ (0 + m) : add_succ_right + 0 + succ m = succ (0 + m) : !add.succ_right ... = succ m : {IH}) -theorem add_succ_left {n m : ℕ} : (succ n) + m = succ (n + m) := +theorem add.succ_left (n m : ℕ) : (succ n) + m = succ (n + m) := induction_on m - (add_zero_right ▸ add_zero_right) + (!add.zero_right ▸ !add.zero_right) (take k IH, calc - succ n + succ k = succ (succ n + k) : add_succ_right + succ n + succ k = succ (succ n + k) : !add.succ_right ... = succ (succ (n + k)) : {IH} - ... = succ (n + succ k) : {add_succ_right⁻¹}) + ... = succ (n + succ k) : {!add.succ_right⁻¹}) -theorem add_comm {n m : ℕ} : n + m = m + n := +theorem add.comm (n m : ℕ) : n + m = m + n := induction_on m - (add_zero_right ⬝ add_zero_left⁻¹) + (!add.zero_right ⬝ !add.zero_left⁻¹) (take k IH, calc - n + succ k = succ (n+k) : add_succ_right + n + succ k = succ (n+k) : !add.succ_right ... = succ (k + n) : {IH} - ... = succ k + n : add_succ_left⁻¹) + ... = succ k + n : !add.succ_left⁻¹) -theorem add_move_succ {n m : ℕ} : succ n + m = n + succ m := -add_succ_left ⬝ add_succ_right⁻¹ +theorem add.move_succ (n m : ℕ) : succ n + m = n + succ m := +!add.succ_left ⬝ !add.succ_right⁻¹ -theorem add_comm_succ {n m : ℕ} : n + succ m = m + succ n := -add_move_succ⁻¹ ⬝ add_comm +theorem add.comm_succ (n m : ℕ) : n + succ m = m + succ n := +!add.move_succ⁻¹ ⬝ !add.comm -theorem add_assoc {n m k : ℕ} : (n + m) + k = n + (m + k) := +theorem add.assoc (n m k : ℕ) : (n + m) + k = n + (m + k) := induction_on k - (add_zero_right ▸ add_zero_right) + (!add.zero_right ▸ !add.zero_right) (take l IH, calc - (n + m) + succ l = succ ((n + m) + l) : add_succ_right + (n + m) + succ l = succ ((n + m) + l) : !add.succ_right ... = succ (n + (m + l)) : {IH} - ... = n + succ (m + l) : add_succ_right⁻¹ - ... = n + (m + succ l) : {add_succ_right⁻¹}) + ... = n + succ (m + l) : !add.succ_right⁻¹ + ... = n + (m + succ l) : {!add.succ_right⁻¹}) -theorem add_left_comm {n m k : ℕ} : n + (m + k) = m + (n + k) := -left_comm @add_comm @add_assoc n m k +theorem add.left_comm (n m k : ℕ) : n + (m + k) = m + (n + k) := +left_comm @add.comm @add.assoc n m k -theorem add_right_comm {n m k : ℕ} : n + m + k = n + k + m := -right_comm @add_comm @add_assoc n m k - --- add_rewrite add_zero_left add_zero_right --- add_rewrite add_succ_left add_succ_right --- add_rewrite add_comm add_assoc add_left_comm +theorem add.right_comm (n m k : ℕ) : n + m + k = n + k + m := +right_comm @add.comm @add.assoc n m k -- ### cancelation -theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k := +theorem add.cancel_left {n m k : ℕ} : n + m = n + k → m = k := induction_on n (take H : 0 + m = 0 + k, - add_zero_left⁻¹ ⬝ H ⬝ add_zero_left) + !add.zero_left⁻¹ ⬝ H ⬝ !add.zero_left) (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k), have H2 : succ (n + m) = succ (n + k), from calc - succ (n + m) = succ n + m : add_succ_left⁻¹ + succ (n + m) = succ n + m : !add.succ_left⁻¹ ... = succ n + k : H - ... = succ (n + k) : add_succ_left, - have H3 : n + m = n + k, from succ_inj H2, + ... = succ (n + k) : !add.succ_left, + have H3 : n + m = n + k, from succ.inj H2, IH H3) -theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k := -have H2 : m + n = m + k, from add_comm ⬝ H ⬝ add_comm, - add_cancel_left H2 +theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k := +have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm, + add.cancel_left H2 -theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0 := +theorem add.eq_zero_left {n m : ℕ} : n + m = 0 → n = 0 := induction_on n (take (H : 0 + m = 0), rfl) (take k IH, assume H : succ k + m = 0, absurd (show succ (k + m) = 0, from calc - succ (k + m) = succ k + m : add_succ_left⁻¹ + succ (k + m) = succ k + m : !add.succ_left⁻¹ ... = 0 : H) succ_ne_zero) -theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 := -add_eq_zero_left (add_comm ⬝ H) +theorem add.eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 := +add.eq_zero_left (!add.comm ⬝ H) -theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := -and.intro (add_eq_zero_left H) (add_eq_zero_right H) +theorem add.eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := +and.intro (add.eq_zero_left H) (add.eq_zero_right H) -- ### misc -theorem add_one {n : ℕ} : n + 1 = succ n := -add_zero_right ▸ add_succ_right +theorem add.one (n : ℕ) : n + 1 = succ n := +!add.zero_right ▸ !add.succ_right -theorem add_one_left {n : ℕ} : 1 + n = succ n := -add_zero_left ▸ add_succ_left +theorem add.one_left (n : ℕ) : 1 + n = succ n := +!add.zero_left ▸ !add.succ_left -- TODO: rename? remove? theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a := -nat.rec H1 (take n IH, add_one ▸ (H2 n IH)) a +nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a -- Multiplication -- -------------- @@ -261,92 +257,92 @@ nat.rec H1 (take n IH, add_one ▸ (H2 n IH)) a definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m infixl `*` := mul -theorem mul_zero_right {n : ℕ} : n * 0 = 0 +theorem mul.zero_right (n : ℕ) : n * 0 = 0 -theorem mul_succ_right {n m : ℕ} : n * succ m = n * m + n +theorem mul.succ_right (n m : ℕ) : n * succ m = n * m + n irreducible mul -- ### commutativity, distributivity, associativity, identity -theorem mul_zero_left {n : ℕ} : 0 * n = 0 := +theorem mul.zero_left (n : ℕ) : 0 * n = 0 := induction_on n - mul_zero_right - (take m IH, mul_succ_right ⬝ add_zero_right ⬝ IH) + !mul.zero_right + (take m IH, !mul.succ_right ⬝ !add.zero_right ⬝ IH) -theorem mul_succ_left {n m : ℕ} : (succ n) * m = (n * m) + m := +theorem mul.succ_left (n m : ℕ) : (succ n) * m = (n * m) + m := induction_on m - (mul_zero_right ⬝ mul_zero_right⁻¹ ⬝ add_zero_right⁻¹) + (!mul.zero_right ⬝ !mul.zero_right⁻¹ ⬝ !add.zero_right⁻¹) (take k IH, calc - succ n * succ k = (succ n * k) + succ n : mul_succ_right + succ n * succ k = (succ n * k) + succ n : !mul.succ_right ... = (n * k) + k + succ n : {IH} - ... = (n * k) + (k + succ n) : add_assoc - ... = (n * k) + (n + succ k) : {add_comm_succ} - ... = (n * k) + n + succ k : add_assoc⁻¹ - ... = (n * succ k) + succ k : {mul_succ_right⁻¹}) + ... = (n * k) + (k + succ n) : !add.assoc + ... = (n * k) + (n + succ k) : {!add.comm_succ} + ... = (n * k) + n + succ k : !add.assoc⁻¹ + ... = (n * succ k) + succ k : {!mul.succ_right⁻¹}) -theorem mul_comm {n m : ℕ} : n * m = m * n := +theorem mul.comm (n m : ℕ) : n * m = m * n := induction_on m - (mul_zero_right ⬝ mul_zero_left⁻¹) + (!mul.zero_right ⬝ !mul.zero_left⁻¹) (take k IH, calc - n * succ k = n * k + n : mul_succ_right + n * succ k = n * k + n : !mul.succ_right ... = k * n + n : {IH} - ... = (succ k) * n : mul_succ_left⁻¹) + ... = (succ k) * n : !mul.succ_left⁻¹) -theorem mul_distr_right {n m k : ℕ} : (n + m) * k = n * k + m * k := +theorem mul.distr_right (n m k : ℕ) : (n + m) * k = n * k + m * k := induction_on k (calc - (n + m) * 0 = 0 : mul_zero_right - ... = 0 + 0 : add_zero_right⁻¹ - ... = n * 0 + 0 : {mul_zero_right⁻¹} - ... = n * 0 + m * 0 : {mul_zero_right⁻¹}) + (n + m) * 0 = 0 : !mul.zero_right + ... = 0 + 0 : !add.zero_right⁻¹ + ... = n * 0 + 0 : {!mul.zero_right⁻¹} + ... = n * 0 + m * 0 : {!mul.zero_right⁻¹}) (take l IH, calc - (n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right + (n + m) * succ l = (n + m) * l + (n + m) : !mul.succ_right ... = n * l + m * l + (n + m) : {IH} - ... = n * l + m * l + n + m : add_assoc⁻¹ - ... = n * l + n + m * l + m : {add_right_comm} - ... = n * l + n + (m * l + m) : add_assoc - ... = n * succ l + (m * l + m) : {mul_succ_right⁻¹} - ... = n * succ l + m * succ l : {mul_succ_right⁻¹}) + ... = n * l + m * l + n + m : !add.assoc⁻¹ + ... = n * l + n + m * l + m : {!add.right_comm} + ... = n * l + n + (m * l + m) : !add.assoc + ... = n * succ l + (m * l + m) : {!mul.succ_right⁻¹} + ... = n * succ l + m * succ l : {!mul.succ_right⁻¹}) -theorem mul_distr_left {n m k : ℕ} : n * (m + k) = n * m + n * k := +theorem mul.distr_left (n m k : ℕ) : n * (m + k) = n * m + n * k := calc - n * (m + k) = (m + k) * n : mul_comm - ... = m * n + k * n : mul_distr_right - ... = n * m + k * n : {mul_comm} - ... = n * m + n * k : {mul_comm} + n * (m + k) = (m + k) * n : !mul.comm + ... = m * n + k * n : !mul.distr_right + ... = n * m + k * n : {!mul.comm} + ... = n * m + n * k : {!mul.comm} -theorem mul_assoc {n m k : ℕ} : (n * m) * k = n * (m * k) := +theorem mul.assoc (n m k : ℕ) : (n * m) * k = n * (m * k) := induction_on k (calc - (n * m) * 0 = 0 : mul_zero_right - ... = n * 0 : mul_zero_right⁻¹ - ... = n * (m * 0) : {mul_zero_right⁻¹}) + (n * m) * 0 = 0 : !mul.zero_right + ... = n * 0 : !mul.zero_right⁻¹ + ... = n * (m * 0) : {!mul.zero_right⁻¹}) (take l IH, calc - (n * m) * succ l = (n * m) * l + n * m : mul_succ_right + (n * m) * succ l = (n * m) * l + n * m : !mul.succ_right ... = n * (m * l) + n * m : {IH} - ... = n * (m * l + m) : mul_distr_left⁻¹ - ... = n * (m * succ l) : {mul_succ_right⁻¹}) + ... = n * (m * l + m) : !mul.distr_left⁻¹ + ... = n * (m * succ l) : {!mul.succ_right⁻¹}) -theorem mul_left_comm {n m k : ℕ} : n * (m * k) = m * (n * k) := -left_comm @mul_comm @mul_assoc n m k +theorem mul.left_comm (n m k : ℕ) : n * (m * k) = m * (n * k) := +left_comm mul.comm mul.assoc n m k -theorem mul_right_comm {n m k : ℕ} : n * m * k = n * k * m := -right_comm @mul_comm @mul_assoc n m k +theorem mul.right_comm (n m k : ℕ) : n * m * k = n * k * m := +right_comm mul.comm mul.assoc n m k -theorem mul_one_right {n : ℕ} : n * 1 = n := +theorem mul.one_right (n : ℕ) : n * 1 = n := calc - n * 1 = n * 0 + n : mul_succ_right - ... = 0 + n : {mul_zero_right} - ... = n : add_zero_left + n * 1 = n * 0 + n : !mul.succ_right + ... = 0 + n : {!mul.zero_right} + ... = n : !add.zero_left -theorem mul_one_left {n : ℕ} : 1 * n = n := +theorem mul.one_left (n : ℕ) : 1 * n = n := calc - 1 * n = n * 1 : mul_comm - ... = n : mul_one_right + 1 * n = n * 1 : !mul.comm + ... = n : !mul.one_right -theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 := +theorem mul.eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 := discriminate (take Hn : n = 0, or.inl Hn) (take (k : ℕ), @@ -359,15 +355,8 @@ discriminate (calc n * m = n * succ l : {Hl} ... = succ k * succ l : {Hk} - ... = k * succ l + succ l : mul_succ_left - ... = succ (k * succ l + l) : add_succ_right)⁻¹, + ... = k * succ l + succ l : !mul.succ_left + ... = succ (k * succ l + l) : !add.succ_right)⁻¹, absurd (Heq ⬝ H) succ_ne_zero)) ----other inversion theorems appear below - --- add_rewrite mul_zero_left mul_zero_right mul_one_right mul_one_left --- add_rewrite mul_succ_left mul_succ_right --- add_rewrite mul_comm mul_assoc mul_left_comm --- add_rewrite mul_distr_right mul_distr_left - end nat diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index ef5970fbb..1f5f2e615 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -306,7 +306,7 @@ case_zero_pos n (by simp) -- add_rewrite mod_mul_self_right theorem mod_mul_self_left {m n : ℕ} : (m * n) mod m = 0 := -mul_comm ▸ mod_mul_self_right +!mul.comm ▸ mod_mul_self_right -- add_rewrite mod_mul_self_left @@ -333,8 +333,8 @@ theorem div_mod_eq {x y : ℕ} : x = x div y * y + x mod y := case_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_right} - ... = x mod 0 : add_zero_left + x div 0 * 0 + x mod 0 = 0 + x mod 0 : {!mul.zero_right} + ... = x mod 0 : !add.zero_left ... = x : mod_zero)⁻¹) (take y, assume H : y > 0, @@ -358,9 +358,9 @@ case_zero_pos y (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 : {mul_succ_left} + ... = ((succ x - y) div y) * y + y + succ x mod y : {!mul.succ_left} ... = ((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) div y) * y + (succ x - y) mod y + y : !add.right_comm ... = succ x - y + y : {(IH _ H6)⁻¹} ... = succ x : add_sub_ge_left H2)⁻¹))) @@ -373,7 +373,7 @@ theorem remainder_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) calc r1 = r1 mod y : by simp ... = (r1 + q1 * y) mod y : (mod_add_mul_self_right H)⁻¹ - ... = (q1 * y + r1) mod y : {add_comm} + ... = (q1 * y + r1) mod y : {!add.comm} ... = (r2 + q2 * y) mod y : by simp ... = r2 mod y : mod_add_mul_self_right H ... = r2 : by simp @@ -381,7 +381,7 @@ calc theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y) (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 := have H4 : q1 * y + r2 = q2 * y + r2, from (remainder_unique H H1 H2 H3) ▸ H3, -have H5 : q1 * y = q2 * y, from add_cancel_right H4, +have H5 : q1 * y = q2 * y, from add.cancel_right H4, have H6 : y > 0, from le_lt_trans zero_le H1, show q1 = q2, from mul_cancel_right H6 H5 @@ -397,8 +397,8 @@ by_cases -- (y = 0) (calc ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq⁻¹ ... = z * (x div y * y + x mod y) : {div_mod_eq} - ... = z * (x div y * y) + z * (x mod y) : mul_distr_left - ... = (x div y) * (z * y) + z * (x mod y) : {mul_left_comm})) + ... = z * (x div y * y) + z * (x mod y) : !mul.distr_left + ... = (x div y) * (z * y) + z * (x mod y) : {!mul.left_comm})) --- something wrong with the term order --- ... = (x div y) * (z * y) + z * (x mod y) : by simp)) @@ -414,8 +414,8 @@ by_cases -- (y = 0) (calc ((z * x) div (z * y)) * (z * y) + (z * x) mod (z * y) = z * x : div_mod_eq⁻¹ ... = z * (x div y * y + x mod y) : {div_mod_eq} - ... = z * (x div y * y) + z * (x mod y) : mul_distr_left - ... = (x div y) * (z * y) + z * (x mod y) : {mul_left_comm})) + ... = z * (x div y * y) + z * (x mod y) : !mul.distr_left + ... = (x div y) * (z * y) + z * (x mod y) : {!mul.left_comm})) theorem mod_one {x : ℕ} : x mod 1 = 0 := have H1 : x mod 1 < 1, from mod_lt succ_pos, @@ -458,13 +458,13 @@ theorem dvd_imp_div_mul_eq {x y : ℕ} (H : y | x) : x div y * y = x := (calc x = x div y * y + x mod y : div_mod_eq ... = x div y * y + 0 : {mp dvd_iff_mod_eq_zero H} - ... = x div y * y : add_zero_right)⁻¹ + ... = x div y * y : !add.zero_right)⁻¹ -- add_rewrite dvd_imp_div_mul_eq theorem mul_eq_imp_dvd {z x y : ℕ} (H : z * y = x) : y | x := have H1 : z * y = x mod y + x div y * y, from - H ⬝ div_mod_eq ⬝ add_comm, + H ⬝ div_mod_eq ⬝ !add.comm, have H2 : (z - x div y) * y = x mod y, from calc (z - x div y) * y = z * y - x div y * y : mul_sub_distr_right @@ -477,7 +477,7 @@ show x mod y = 0, from calc x = z * y : H⁻¹ ... = z * 0 : {yz} - ... = 0 : mul_zero_right, + ... = 0 : !mul.zero_right, calc x mod y = x mod 0 : {yz} ... = x : mod_zero @@ -485,13 +485,13 @@ show x mod y = 0, from (assume ynz : y ≠ 0, have ypos : y > 0, from ne_zero_imp_pos ynz, have H3 : (z - x div y) * y < y, from H2⁻¹ ▸ mod_lt ypos, - have H4 : (z - x div y) * y < 1 * y, from mul_one_left⁻¹ ▸ H3, + have H4 : (z - x div y) * y < 1 * y, from !mul.one_left⁻¹ ▸ H3, have H5 : z - x div y < 1, from mul_lt_cancel_right H4, have H6 : z - x div y = 0, from le_zero (lt_succ_imp_le H5), calc x mod y = (z - x div y) * y : H2⁻¹ ... = 0 * y : {H6} - ... = 0 : mul_zero_left) + ... = 0 : !mul.zero_left) theorem dvd_iff_exists_mul {x y : ℕ} : x | y ↔ ∃z, z * x = y := iff.intro @@ -537,7 +537,7 @@ have H4 : k = k div n * (n div m) * m, from calc k = k div n * n : by simp ... = k div n * (n div m * m) : {H3} - ... = k div n * (n div m) * m : mul_assoc⁻¹, + ... = k div n * (n div m) * m : !mul.assoc⁻¹, mp (dvd_iff_exists_mul⁻¹) (exists_intro (k div n * (n div m)) (H4⁻¹)) theorem dvd_add {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 + n2) := @@ -560,16 +560,16 @@ case_zero_pos m calc n1 + n2 = (n1 + n2) div m * m : by simp ... = (n1 div m * m + n2) div m * m : by simp - ... = (n2 + n1 div m * m) div m * m : {add_comm} + ... = (n2 + n1 div m * m) div m * m : {!add.comm} ... = (n2 div m + n1 div m) * m : {div_add_mul_self_right mpos} - ... = n2 div m * m + n1 div m * m : mul_distr_right - ... = n1 div m * m + n2 div m * m : add_comm + ... = n2 div m * m + n1 div m * m : !mul.distr_right + ... = n1 div m * m + n2 div m * m : !add.comm ... = n1 + n2 div m * m : by simp, - have H4 : n2 = n2 div m * m, from add_cancel_left H3, + have H4 : n2 = n2 div m * m, from add.cancel_left H3, mp (dvd_iff_exists_mul⁻¹) (exists_intro _ (H4⁻¹))) theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m | n1 := -dvd_add_cancel_left (add_comm ▸ H) +dvd_add_cancel_left (!add.comm ▸ H) theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) := by_cases diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 355fd3fbf..67ec3c66c 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -35,14 +35,14 @@ irreducible le -- ### partial order (totality is part of less than) theorem le_refl {n : ℕ} : n ≤ n := -le_intro add_zero_right +le_intro !add.zero_right theorem zero_le {n : ℕ} : 0 ≤ n := -le_intro add_zero_left +le_intro !add.zero_left theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 := obtain (k : ℕ) (Hk : n + k = 0), from le_elim H, -add_eq_zero_left Hk +add.eq_zero_left Hk theorem not_succ_zero_le {n : ℕ} : ¬ succ n ≤ 0 := not_intro @@ -55,7 +55,7 @@ obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1, obtain (l2 : ℕ) (Hl2 : m + l2 = k), from le_elim H2, le_intro (calc - n + (l1 + l2) = n + l1 + l2 : add_assoc⁻¹ + n + (l1 + l2) = n + l1 + l2 : !add.assoc⁻¹ ... = m + l2 : {Hl1} ... = k : Hl2) @@ -63,15 +63,15 @@ theorem le_antisym {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := obtain (k : ℕ) (Hk : n + k = m), from (le_elim H1), obtain (l : ℕ) (Hl : m + l = n), from (le_elim H2), have L1 : k + l = 0, from - add_cancel_left + add.cancel_left (calc - n + (k + l) = n + k + l : add_assoc⁻¹ + n + (k + l) = n + k + l : !add.assoc⁻¹ ... = m + l : {Hk} ... = n : Hl - ... = n + 0 : add_zero_right⁻¹), -have L2 : k = 0, from add_eq_zero_left L1, + ... = n + 0 : !add.zero_right⁻¹), +have L2 : k = 0, from add.eq_zero_left L1, calc - n = n + 0 : add_zero_right⁻¹ + n = n + 0 : !add.zero_right⁻¹ ... = n + k : {L2⁻¹} ... = m : Hk @@ -81,17 +81,17 @@ theorem le_add_right {n m : ℕ} : n ≤ n + m := le_intro rfl theorem le_add_left {n m : ℕ} : n ≤ m + n := -le_intro add_comm +le_intro !add.comm theorem add_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m := obtain (l : ℕ) (Hl : n + l = m), from (le_elim H), le_intro (calc - k + n + l = k + (n + l) : add_assoc + k + n + l = k + (n + l) : !add.assoc ... = k + m : {Hl}) theorem add_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k := -add_comm ▸ add_comm ▸ add_le_left H k +!add.comm ▸ !add.comm ▸ add_le_left H k theorem add_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n + m ≤ k + l := le_trans (add_le_right H1 m) (add_le_left H2 k) @@ -99,17 +99,17 @@ le_trans (add_le_right H1 m) (add_le_left H2 k) theorem add_le_cancel_left {n m k : ℕ} (H : k + n ≤ k + m) : n ≤ m := obtain (l : ℕ) (Hl : k + n + l = k + m), from (le_elim H), -le_intro (add_cancel_left +le_intro (add.cancel_left (calc - k + (n + l) = k + n + l : add_assoc⁻¹ + k + (n + l) = k + n + l : !add.assoc⁻¹ ... = k + m : Hl)) theorem add_le_cancel_right {n m k : ℕ} (H : n + k ≤ m + k) : n ≤ m := -add_le_cancel_left (add_comm ▸ add_comm ▸ H) +add_le_cancel_left (!add.comm ▸ !add.comm ▸ H) theorem add_le_inv {n m k l : ℕ} (H1 : n + m ≤ k + l) (H2 : k ≤ n) : m ≤ l := obtain (a : ℕ) (Ha : k + a = n), from le_elim H2, -have H3 : k + (a + m) ≤ k + l, from add_assoc ▸ Ha⁻¹ ▸ H1, +have H3 : k + (a + m) ≤ k + l, from !add.assoc ▸ Ha⁻¹ ▸ H1, have H4 : a + m ≤ l, from add_le_cancel_left H3, show m ≤ l, from le_trans le_add_left H4 @@ -118,13 +118,13 @@ show m ≤ l, from le_trans le_add_left H4 -- ### interaction with successor and predecessor theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := -add_one ▸ add_one ▸ add_le_right H 1 +!add.one ▸ !add.one ▸ add_le_right H 1 theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := -add_le_cancel_right (add_one⁻¹ ▸ add_one⁻¹ ▸ H) +add_le_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H) theorem self_le_succ {n : ℕ} : n ≤ succ n := -le_intro add_one +le_intro !add.one theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le_trans H self_le_succ @@ -135,7 +135,7 @@ discriminate (assume H3 : k = 0, have Heq : n = m, from calc - n = n + 0 : add_zero_right⁻¹ + n = n + 0 : !add.zero_right⁻¹ ... = n + k : {H3⁻¹} ... = m : Hk, or.inr Heq) @@ -144,7 +144,7 @@ discriminate have Hlt : succ n ≤ m, from (le_intro (calc - succ n + l = n + succ l : add_move_succ + succ n + l = n + succ l : !add.move_succ ... = n + k : {H3⁻¹} ... = m : Hk)), or.inl Hlt) @@ -161,18 +161,18 @@ obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H), and.intro (have H3 : n + succ k = m, from calc - n + succ k = succ n + k : add_move_succ⁻¹ + n + succ k = succ n + k : !add.move_succ⁻¹ ... = m : H2, show n ≤ m, from le_intro H3) (assume H3 : n = m, have H4 : succ n ≤ n, from H3⁻¹ ▸ H, have H5 : succ n = n, from le_antisym H4 self_le_succ, - show false, from absurd H5 succ_ne_self) + show false, from absurd H5 succ.ne_self) theorem le_pred_self {n : ℕ} : pred n ≤ n := case n - (pred_zero⁻¹ ▸ le_refl) - (take k : ℕ, pred_succ⁻¹ ▸ self_le_succ) + (pred.zero⁻¹ ▸ le_refl) + (take k : ℕ, !pred.succ⁻¹ ▸ self_le_succ) theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := discriminate @@ -180,7 +180,7 @@ discriminate have H2 : pred n = 0, from calc pred n = pred 0 : {Hn} - ... = 0 : pred_zero, + ... = 0 : pred.zero, H2⁻¹ ▸ zero_le) (take k : ℕ, assume Hn : n = succ k, @@ -188,9 +188,9 @@ discriminate have H2 : pred n + l = pred m, from calc pred n + l = pred (succ k) + l : {Hn} - ... = k + l : {pred_succ} - ... = pred (succ (k + l)) : pred_succ⁻¹ - ... = pred (succ k + l) : {add_succ_left⁻¹} + ... = k + l : {!pred.succ} + ... = pred (succ (k + l)) : !pred.succ⁻¹ + ... = pred (succ k + l) : {!add.succ_left⁻¹} ... = pred (n + l) : {Hn⁻¹} ... = pred m : {Hl}, le_intro H2) @@ -204,7 +204,7 @@ discriminate have H2 : pred n = k, from calc pred n = pred (succ k) : {Hn} - ... = k : pred_succ, + ... = k : !pred.succ, have H3 : k ≤ m, from H2 ▸ H, have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, show n ≤ m ∨ n = succ m, from @@ -223,7 +223,7 @@ have H2 : k * n + k * l = k * m, from le_intro H2 theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k := -mul_comm ▸ mul_comm ▸ (mul_le_left H k) +!mul.comm ▸ !mul.comm ▸ (mul_le_left H k) theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l := le_trans (mul_le_right H1 m) (mul_le_left H2 k) @@ -276,7 +276,7 @@ theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m := le_elim H theorem lt_add_succ (n m : ℕ) : n < n + succ m := -lt_intro add_move_succ +lt_intro !add.move_succ -- ### basic facts @@ -346,10 +346,10 @@ le_imp_not_gt (lt_imp_le H) -- ### interaction with addition theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m := -add_succ_right ▸ add_le_left H k +!add.succ_right ▸ add_le_left H k theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k := -add_comm ▸ add_comm ▸ add_lt_left H k +!add.comm ▸ !add.comm ▸ add_lt_left H k theorem add_le_lt {n m k l : ℕ} (H1 : n ≤ k) (H2 : m < l) : n + m < k + l := le_lt_trans (add_le_right H1 m) (add_lt_left H2 k) @@ -361,18 +361,18 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l := add_lt_le H1 (lt_imp_le H2) theorem add_lt_cancel_left {n m k : ℕ} (H : k + n < k + m) : n < m := -add_le_cancel_left (add_succ_right⁻¹ ▸ H) +add_le_cancel_left (!add.succ_right⁻¹ ▸ H) theorem add_lt_cancel_right {n m k : ℕ} (H : n + k < m + k) : n < m := -add_lt_cancel_left (add_comm ▸ add_comm ▸ H) +add_lt_cancel_left (!add.comm ▸ !add.comm ▸ H) -- ### interaction with successor (see also the interaction with le) theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m := -add_one ▸ add_one ▸ add_lt_right H 1 +!add.one ▸ !add.one ▸ add_lt_right H 1 theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) : n < m := -add_lt_cancel_right (add_one⁻¹ ▸ add_one⁻¹ ▸ H) +add_lt_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H) theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m := lt_trans H self_lt_succ @@ -393,14 +393,14 @@ induction_on n from calc m = k + l : Hl⁻¹ ... = k + 0 : {H2} - ... = k : add_zero_right, + ... = k : !add.zero_right, have H4 : m < succ k, from H3 ▸ self_lt_succ, or.inr H4) (take l2 : ℕ, assume H2 : l = succ l2, have H3 : succ k + l2 = m, from calc - succ k + l2 = k + succ l2 : add_move_succ + succ k + l2 = k + succ l2 : !add.move_succ ... = k + l : {H2⁻¹} ... = m : Hl, or.inl (le_intro H3))) @@ -486,10 +486,10 @@ theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l := lt_imp_eq_succ H theorem add_pos_right {n k : ℕ} (H : k > 0) : n + k > n := -add_zero_right ▸ add_lt_left H n +!add.zero_right ▸ add_lt_left H n theorem add_pos_left {n : ℕ} {k : ℕ} (H : k > 0) : k + n > n := -add_comm ▸ add_pos_right H +!add.comm ▸ add_pos_right H -- ### multiplication @@ -499,8 +499,8 @@ obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm, succ_imp_pos (calc n * m = succ k * m : {Hk} ... = succ k * succ l : {Hl} - ... = succ k * l + succ k : mul_succ_right - ... = succ (succ k * l + k) : add_succ_right) + ... = succ k * l + succ k : !mul.succ_right + ... = succ (succ k * l + k) : !add.succ_right) theorem mul_pos_imp_pos_left {n m : ℕ} (H : n * m > 0) : n > 0 := discriminate @@ -508,7 +508,7 @@ discriminate have H3 : n * m = 0, from calc n * m = 0 * m : {H2} - ... = 0 : mul_zero_left, + ... = 0 : !mul.zero_left, have H4 : 0 > 0, from H3 ▸ H, absurd H4 lt_irrefl) (take l : nat, @@ -516,17 +516,17 @@ discriminate Hl⁻¹ ▸ succ_pos) theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0 := -mul_pos_imp_pos_left (mul_comm ▸ H) +mul_pos_imp_pos_left (!mul.comm ▸ H) -- ### interaction of mul with le and lt theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m := have H2 : k * n < k * n + k, from add_pos_right Hk, -have H3 : k * n + k ≤ k * m, from mul_succ_right ▸ mul_le_left H k, +have H3 : k * n + k ≤ k * m, from !mul.succ_right ▸ mul_le_left H k, lt_le_trans H2 H3 theorem mul_lt_right {n m k : ℕ} (Hk : k > 0) (H : n < m) : n * k < m * k := -mul_comm ▸ mul_comm ▸ mul_lt_left Hk H +!mul.comm ▸ !mul.comm ▸ mul_lt_left Hk H theorem mul_le_lt {n m k l : ℕ} (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) : n * m < k * l := le_lt_trans (mul_le_right H1 m) (mul_lt_left Hk H2) @@ -547,16 +547,16 @@ or.elim le_or_gt (assume H2 : n < m, H2) theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m := -mul_lt_cancel_left (mul_comm ▸ mul_comm ▸ H) +mul_lt_cancel_left (!mul.comm ▸ !mul.comm ▸ H) theorem mul_le_cancel_left {n m k : ℕ} (Hk : k > 0) (H : k * n ≤ k * m) : n ≤ m := have H2 : k * n < k * m + k, from le_lt_trans H (add_pos_right Hk), -have H3 : k * n < k * succ m, from mul_succ_right⁻¹ ▸ H2, +have H3 : k * n < k * succ m, from !mul.succ_right⁻¹ ▸ H2, have H4 : n < succ m, from mul_lt_cancel_left H3, show n ≤ m, from lt_succ_imp_le H4 theorem mul_le_cancel_right {n k m : ℕ} (Hm : m > 0) (H : n * m ≤ k * m) : n ≤ k := -mul_le_cancel_left Hm (mul_comm ▸ mul_comm ▸ H) +mul_le_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H) theorem mul_cancel_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k := have H2 : n * m ≤ n * k, from H ▸ le_refl, @@ -570,10 +570,10 @@ or.imp_or_right zero_or_pos (assume Hn : n > 0, mul_cancel_left Hn H) theorem mul_cancel_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k := -mul_cancel_left Hm (mul_comm ▸ mul_comm ▸ H) +mul_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H) theorem mul_cancel_right_or {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k := -mul_cancel_left_or (mul_comm ▸ mul_comm ▸ H) +mul_cancel_left_or (!mul.comm ▸ !mul.comm ▸ H) theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 := have H2 : n * m > 0, from H⁻¹ ▸ succ_pos, @@ -584,10 +584,10 @@ or.elim le_or_gt show n = 1, from le_antisym H5 H3) (assume H5 : n > 1, have H6 : n * m ≥ 2 * 1, from mul_le H5 H4, - have H7 : 1 ≥ 2, from mul_one_right ▸ H ▸ H6, + have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6, absurd self_lt_succ (le_imp_not_gt H7)) theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 := -mul_eq_one_left (mul_comm ▸ H) +mul_eq_one_left (!mul.comm ▸ H) end nat diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index c4504e3b0..2cb65c98e 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -35,14 +35,14 @@ induction_on n sub_zero_right calc 0 - succ k = pred (0 - k) : sub_succ_right ... = pred 0 : {IH} - ... = 0 : pred_zero) + ... = 0 : pred.zero) theorem sub_succ_succ {n m : ℕ} : succ n - succ m = n - m := induction_on m (calc succ n - 1 = pred (succ n - 0) : sub_succ_right ... = pred (succ n) : {sub_zero_right} - ... = n : pred_succ + ... = n : !pred.succ ... = n - 0 : sub_zero_right⁻¹) (take k : nat, assume IH : succ n - succ k = n - k, @@ -57,50 +57,50 @@ induction_on n sub_zero_right (take k IH, sub_succ_succ ⬝ IH) theorem sub_add_add_right {n k m : ℕ} : (n + k) - (m + k) = n - m := induction_on k (calc - (n + 0) - (m + 0) = n - (m + 0) : {add_zero_right} - ... = n - m : {add_zero_right}) + (n + 0) - (m + 0) = n - (m + 0) : {!add.zero_right} + ... = n - m : {!add.zero_right}) (take l : nat, assume IH : (n + l) - (m + l) = n - m, calc - (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ_right} - ... = succ (n + l) - succ (m + l) : {add_succ_right} + (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add.succ_right} + ... = succ (n + l) - succ (m + l) : {!add.succ_right} ... = (n + l) - (m + l) : sub_succ_succ ... = n - m : IH) theorem sub_add_add_left {k n m : ℕ} : (k + n) - (k + m) = n - m := -add_comm ▸ add_comm ▸ sub_add_add_right +!add.comm ▸ !add.comm ▸ sub_add_add_right theorem sub_add_left {n m : ℕ} : n + m - m = n := induction_on m - (add_zero_right⁻¹ ▸ sub_zero_right) + (!add.zero_right⁻¹ ▸ sub_zero_right) (take k : ℕ, assume IH : n + k - k = n, calc - n + succ k - succ k = succ (n + k) - succ k : {add_succ_right} + n + succ k - succ k = succ (n + k) - succ k : {!add.succ_right} ... = n + k - k : sub_succ_succ ... = n : IH) -- TODO: add_sub_inv' theorem sub_add_left2 {n m : ℕ} : n + m - n = m := -add_comm ▸ sub_add_left +!add.comm ▸ sub_add_left theorem sub_sub {n m k : ℕ} : n - m - k = n - (m + k) := induction_on k (calc n - m - 0 = n - m : sub_zero_right - ... = n - (m + 0) : {add_zero_right⁻¹}) + ... = n - (m + 0) : {!add.zero_right⁻¹}) (take l : nat, assume IH : n - m - l = n - (m + l), calc n - m - succ l = pred (n - m - l) : sub_succ_right ... = pred (n - (m + l)) : {IH} ... = n - succ (m + l) : sub_succ_right⁻¹ - ... = n - (m + succ l) : {add_succ_right⁻¹}) + ... = n - (m + succ l) : {!add.succ_right⁻¹}) theorem succ_sub_sub {n m k : ℕ} : succ n - m - succ k = n - m - k := calc succ n - m - succ k = succ n - (m + succ k) : sub_sub - ... = succ n - succ (m + k) : {add_succ_right} + ... = succ n - succ (m + k) : {!add.succ_right} ... = n - (m + k) : sub_succ_succ ... = n - m - k : sub_sub⁻¹ @@ -113,7 +113,7 @@ calc theorem sub_comm {m n k : ℕ} : m - n - k = m - k - n := calc m - n - k = m - (n + k) : sub_sub - ... = m - (k + n) : {add_comm} + ... = m - (k + n) : {!add.comm} ... = m - k - n : sub_sub⁻¹ theorem sub_one {n : ℕ} : n - 1 = pred n := @@ -131,28 +131,28 @@ sub_succ_succ ⬝ sub_zero_right theorem mul_pred_left {n m : ℕ} : pred n * m = n * m - m := induction_on n (calc - pred 0 * m = 0 * m : {pred_zero} - ... = 0 : mul_zero_left + pred 0 * m = 0 * m : {pred.zero} + ... = 0 : !mul.zero_left ... = 0 - m : sub_zero_left⁻¹ - ... = 0 * m - m : {mul_zero_left⁻¹}) + ... = 0 * m - m : {!mul.zero_left⁻¹}) (take k : nat, assume IH : pred k * m = k * m - m, calc - pred (succ k) * m = k * m : {pred_succ} + pred (succ k) * m = k * m : {!pred.succ} ... = k * m + m - m : sub_add_left⁻¹ - ... = succ k * m - m : {mul_succ_left⁻¹}) + ... = succ k * m - m : {!mul.succ_left⁻¹}) theorem mul_pred_right {n m : ℕ} : n * pred m = n * m - n := -calc n * pred m = pred m * n : mul_comm +calc n * pred m = pred m * n : !mul.comm ... = m * n - n : mul_pred_left - ... = n * m - n : {mul_comm} + ... = n * m - n : {!mul.comm} theorem mul_sub_distr_right {n m k : ℕ} : (n - m) * k = n * k - m * k := induction_on m (calc (n - 0) * k = n * k : {sub_zero_right} ... = n * k - 0 : sub_zero_right⁻¹ - ... = n * k - 0 * k : {mul_zero_left⁻¹}) + ... = n * k - 0 * k : {!mul.zero_left⁻¹}) (take l : nat, assume IH : (n - l) * k = n * k - l * k, calc @@ -160,14 +160,14 @@ induction_on m ... = (n - l) * k - k : mul_pred_left ... = n * k - l * k - k : {IH} ... = n * k - (l * k + k) : sub_sub - ... = n * k - (succ l * k) : {mul_succ_left⁻¹}) + ... = n * k - (succ l * k) : {!mul.succ_left⁻¹}) theorem mul_sub_distr_left {n m k : ℕ} : n * (m - k) = n * m - n * k := calc - n * (m - k) = (m - k) * n : mul_comm + n * (m - k) = (m - k) * n : !mul.comm ... = m * n - k * n : mul_sub_distr_right - ... = n * m - k * n : {mul_comm} - ... = n * m - n * k : {mul_comm} + ... = n * m - k * n : {!mul.comm} + ... = n * m - n * k : {!mul.comm} -- ### interaction with inequalities @@ -197,7 +197,7 @@ sub_induction n m (take k, assume H : 0 ≤ k, calc - 0 + (k - 0) = k - 0 : add_zero_left + 0 + (k - 0) = k - 0 : !add.zero_left ... = k : sub_zero_right) (take k, assume H : succ k ≤ 0, absurd H not_succ_zero_le) (take k l, @@ -205,19 +205,19 @@ sub_induction n m take H : succ k ≤ succ l, calc succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ} - ... = succ (k + (l - k)) : add_succ_left + ... = succ (k + (l - k)) : !add.succ_left ... = succ l : {IH (succ_le_cancel H)}) theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n := -add_comm ▸ add_sub_le +!add.comm ▸ add_sub_le theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n := calc n + (m - n) = n + 0 : {le_imp_sub_eq_zero H} - ... = n : add_zero_right + ... = n : !add.zero_right theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m := -add_comm ▸ add_sub_ge +!add.comm ▸ add_sub_ge theorem le_add_sub_left {n m : ℕ} : n ≤ n + (m - n) := or.elim le_total @@ -238,7 +238,7 @@ or.elim le_total theorem sub_le_self {n m : ℕ} : n - m ≤ n := sub_split (assume H : n ≤ m, zero_le) - (take k : ℕ, assume H : m + k = n, le_intro (add_comm ▸ H)) + (take k : ℕ, assume H : m + k = n, le_intro (!add.comm ▸ H)) theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n := obtain (k : ℕ) (Hk : n + k = m), from le_elim H, @@ -260,7 +260,7 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from assume IH : k ≤ m → n + m - k = n + (m - k), take H : succ k ≤ succ m, calc - n + succ m - succ k = succ (n + m) - succ k : {add_succ_right} + n + succ m - succ k = succ (n + m) - succ k : {!add.succ_right} ... = n + m - k : sub_succ_succ ... = n + (m - k) : IH (succ_le_cancel H) ... = n + (succ m - succ k) : {sub_succ_succ⁻¹}), @@ -272,7 +272,7 @@ sub_split (take k : ℕ, assume H1 : m + k = n, assume H2 : k = 0, - have H3 : n = m, from add_zero_right ▸ H2 ▸ H1⁻¹, + have H3 : n = m, from !add.zero_right ▸ H2 ▸ H1⁻¹, H3 ▸ le_refl) theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) @@ -288,8 +288,8 @@ have H2 : k - n + n = m + n, from calc k - n + n = k : add_sub_ge_left (le_intro H) ... = n + m : H⁻¹ - ... = m + n : add_comm, -add_cancel_right H2 + ... = m + n : !add.comm, +add.cancel_right H2 theorem sub_lt {x y : ℕ} (xpos : x > 0) (ypos : y > 0) : x - y < x := obtain (x' : ℕ) (xeq : x = succ x'), from pos_imp_eq_succ xpos, @@ -312,7 +312,7 @@ or.elim le_total calc n - k + l = l + (n - k) : by simp ... = l + n - k : (add_sub_assoc H2 l)⁻¹ - ... = n + l - k : {add_comm} + ... = n + l - k : {!add.comm} ... = m - k : {Hl}, le_intro H3) @@ -329,7 +329,7 @@ sub_split ... = m + m' : {Hl} ... = k : Hm ... = k - n + n : (add_sub_ge_left H3)⁻¹, - le_intro (add_cancel_right H4)) + le_intro (add.cancel_right H4)) -- theorem sub_lt_cancel_right {n m k : ℕ) (H : n - k < m - k) : n < m -- := @@ -341,14 +341,14 @@ sub_split theorem sub_triangle_inequality {n m k : ℕ} : n - k ≤ (n - m) + (m - k) := sub_split - (assume H : n ≤ m, add_zero_left⁻¹ ▸ sub_le_right H k) + (assume H : n ≤ m, !add.zero_left⁻¹ ▸ sub_le_right H k) (take mn : ℕ, assume Hmn : m + mn = n, sub_split (assume H : m ≤ k, have H2 : n - k ≤ n - m, from sub_le_left H n, have H3 : n - k ≤ mn, from sub_intro Hmn ▸ H2, - show n - k ≤ mn + 0, from add_zero_right⁻¹ ▸ H3) + show n - k ≤ mn + 0, from !add.zero_right⁻¹ ▸ H3) (take km : ℕ, assume Hkm : k + km = m, have H : k + (mn + km) = n, from @@ -384,7 +384,7 @@ theorem right_le_max {n m : ℕ} : m ≤ max n m := le_add_sub_right definition dist (n m : ℕ) := (n - m) + (m - n) theorem dist_comm {n m : ℕ} : dist n m = dist m n := -add_comm +!add.comm theorem dist_self {n : ℕ} : dist n n = 0 := calc @@ -392,16 +392,16 @@ calc ... = 0 : by simp theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m := -have H2 : n - m = 0, from add_eq_zero_left H, +have H2 : n - m = 0, from add.eq_zero_left H, have H3 : n ≤ m, from sub_eq_zero_imp_le H2, -have H4 : m - n = 0, from add_eq_zero_right H, +have H4 : m - n = 0, from add.eq_zero_right H, have H5 : m ≤ n, from sub_eq_zero_imp_le H4, le_antisym H3 H5 theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n := calc dist n m = 0 + (m - n) : {le_imp_sub_eq_zero H} - ... = m - n : add_zero_left + ... = m - n : !add.zero_left theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m := dist_comm ▸ dist_le H @@ -424,7 +424,7 @@ calc ... = (n - m) + (m - n) : {sub_add_add_right} theorem dist_add_left {k n m : ℕ} : dist (k + n) (k + m) = dist n m := -add_comm ▸ add_comm ▸ dist_add_right +!add.comm ▸ !add.comm ▸ dist_add_right -- add_rewrite dist_self dist_add_right dist_add_left dist_zero_left dist_zero_right @@ -485,7 +485,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l ... = dist (n * (k - l)) (m * (k - l)) : dist_mul_right⁻¹ ... = dist (n * k - n * l) (m * k - m * l) : by simp ... = dist (n * k) (m * k - m * l + n * l) : dist_sub_move_add (mul_le_left H n) _ - ... = dist (n * k) (n * l + (m * k - m * l)) : {add_comm} + ... = dist (n * k) (n * l + (m * k - m * l)) : {!add.comm} ... = dist (n * k) (n * l + m * k - m * l) : {(add_sub_assoc H2 (n * l))⁻¹} ... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _, or.elim le_total diff --git a/library/data/vector.lean b/library/data/vector.lean index b9d2ffedc..361a789a0 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -81,14 +81,14 @@ namespace vector cast (congr_arg P H) B definition concat {n m : ℕ} (v : vector T n) (w : vector T m) : vector T (n + m) := - vector.rec (cast_subst (add_zero_left⁻¹) w) (λx n w' u, cast_subst (add_succ_left⁻¹) (x::u)) v + vector.rec (cast_subst (!add.zero_left⁻¹) w) (λx n w' u, cast_subst (!add.succ_left⁻¹) (x::u)) v infixl `++`:65 := concat - theorem nil_concat {n : ℕ} (v : vector T n) : nil ++ v = cast_subst (add_zero_left⁻¹) v := rfl + theorem nil_concat {n : ℕ} (v : vector T n) : nil ++ v = cast_subst (!add.zero_left⁻¹) v := rfl theorem cons_concat {n m : ℕ} (x : T) (v : vector T n) (w : vector T m) - : (x :: v) ++ w = cast_subst (add_succ_left⁻¹) (x::(v++w)) := rfl + : (x :: v) ++ w = cast_subst (!add.succ_left⁻¹) (x::(v++w)) := rfl /- theorem cons_concat (x : T) (s t : list T) : (x :: s) ++ t = x :: (s ++ t) := refl _ diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index fb766a123..1fe7674f0 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -42,7 +42,6 @@ opaque definition exact {B : Type} (b : B) : tactic := builtin opaque definition trace (s : string) : tactic := builtin precedence `;`:200 infixl ; := and_then -notation `!` t:max := repeat t -- [ t_1 | ... | t_n ] notation notation `[` h:100 `|` r:(foldl 100 `|` (e r, or_else r e) h) `]` := r -- [ t_1 || ... || t_n ] notation diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean index da314e652..ae8152331 100644 --- a/tests/lean/run/tactic7.lean +++ b/tests/lean/run/tactic7.lean @@ -6,6 +6,6 @@ theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A check tst theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by !([apply @and.intro | assumption] ; trace "STEP"; state; trace "----------") +:= by repeat ([apply @and.intro | assumption] ; trace "STEP"; state; trace "----------") check tst2 diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean index ceccc793b..905d1c675 100644 --- a/tests/lean/slow/list_elab2.lean +++ b/tests/lean/slow/list_elab2.lean @@ -110,14 +110,14 @@ theorem length_concat (s t : list T) : length (s ++ t) = length s + length t := list_induction_on s (calc length (concat nil t) = length t : refl _ - ... = 0 + length t : {symm add_zero_left} + ... = 0 + length t : {symm !add.zero_left} ... = length (@nil T) + length t : refl _) (take x s, assume H : length (concat s t) = length s + length t, calc length (concat (cons x s) t ) = succ (length (concat s t)) : refl _ ... = succ (length s + length t) : { H } - ... = succ (length s) + length t : {symm add_succ_left} + ... = succ (length s) + length t : {symm !add.succ_left} ... = length (cons x s) + length t : refl _) -- Reverse