diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index 21e95b37e..e8273f929 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -57,10 +57,10 @@ The command =import= loads existing libraries and extensions. #+BEGIN_SRC lean import data.nat - check nat.ge + check nat.gcd #+END_SRC -We say =nat.ge= is a hierarchical name comprised of two parts: =nat= and =ge=. +We say =nat.gcd= is a hierarchical name comprised of two parts: =nat= and =gcd=. The command =open= creates aliases based on a given prefix. The command also imports notation, hints, and other features. We will @@ -71,7 +71,7 @@ the following command creates aliases for all objects starting with #+BEGIN_SRC lean import data.nat open nat - check ge -- display the type of nat.ge + check gcd -- display the type of nat.gcd #+END_SRC The command =constant= assigns a type to an identifier. The following command postulates/assumes @@ -370,18 +370,19 @@ examples. check λ (x : nat) (p : Prop), x = 0 ∨ p #+END_SRC -In many cases, Lean can automatically infer the type of the variable. Actually, -in all examples above, the type can be inferred automatically. +In many cases, Lean can automatically infer the type of the variable. #+BEGIN_SRC lean import data.nat open nat - check fun x, x + 1 - check fun x y, x + 2 * y + check fun x, x + (1:nat) + check fun x : nat, x + 1 + check fun x, (x:nat) + 1 + check fun x y, x + (2:nat) * y check fun x y, not (x ∧ y) - check λ x, x + 1 - check λ x p, x = 0 ∨ p + check λ x, x + (1:nat) + check λ x p, x = (0:nat) ∨ p #+END_SRC However, Lean will complain that it cannot infer the type of the @@ -393,8 +394,8 @@ function applications #+BEGIN_SRC lean import data.nat open nat - check (fun x y, x + 2 * y) 1 - check (fun x y, x + 2 * y) 1 2 + check (fun x y, x + 2 * y) (1:nat) + check (fun x y, x + 2 * y) (1:nat) 2 check (fun x y, not (x ∧ y)) true false #+END_SRC diff --git a/tests/lean/491.lean b/tests/lean/491.lean index a49990929..a4fa2f8a1 100644 --- a/tests/lean/491.lean +++ b/tests/lean/491.lean @@ -4,5 +4,5 @@ variable A : Type variables a b : A variable H : a = b check H⁻¹ -check -1 -check 1 + -2 +check -(1:int) +check (1:int) + -2 diff --git a/tests/lean/584a.lean b/tests/lean/584a.lean index 58b7cd911..94fc6ef99 100644 --- a/tests/lean/584a.lean +++ b/tests/lean/584a.lean @@ -12,7 +12,7 @@ open nat check foo nat 10 -definition test : foo' = 10 := rfl +definition test : foo' = (10:nat) := rfl set_option pp.implicit true print test diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out index 0884db45d..20737e6b3 100644 --- a/tests/lean/584a.lean.expected.out +++ b/tests/lean/584a.lean.expected.out @@ -1,5 +1,5 @@ foo : Π (A : Type) [H : inhabited A], A → A foo' : Π {A : Type} [H : inhabited A] {x : A}, A foo ℕ 10 : ℕ -definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10 := -λ (A : Type) (H : inhabited A), @rfl num (@foo' num num.is_inhabited 10) +definition test : ∀ {A : Type} [H : inhabited A], @foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5) = 10 := +λ (A : Type) (H : inhabited A), @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5)) diff --git a/tests/lean/640a.hlean b/tests/lean/640a.hlean index 44caf6460..e14196a45 100644 --- a/tests/lean/640a.hlean +++ b/tests/lean/640a.hlean @@ -2,7 +2,7 @@ section parameter {A : Type} definition relation : A → A → Type := λa b, a = b local abbreviation R := relation - local abbreviation S [parsing-only] := relation + local abbreviation S [parsing_only] := relation variable {a : A} check relation a a check R a a @@ -13,7 +13,7 @@ section parameter {A : Type} definition relation' : A → A → Type := λa b, a = b local infix ` ~1 `:50 := relation' - local infix [parsing-only] ` ~2 `:50 := relation' + local infix [parsing_only] ` ~2 `:50 := relation' variable {a : A} check relation' a a check a ~1 a @@ -23,7 +23,7 @@ end section parameter {A : Type} definition relation'' : A → A → Type := λa b, a = b - local infix [parsing-only] ` ~2 `:50 := relation'' + local infix [parsing_only] ` ~2 `:50 := relation'' variable {a : A} check relation'' a a check a ~2 a @@ -33,7 +33,7 @@ end section parameter {A : Type} definition relation''' : A → A → Type := λa b, a = b - local abbreviation S [parsing-only] := relation''' + local abbreviation S [parsing_only] := relation''' variable {a : A} check relation''' a a check S a a diff --git a/tests/lean/640b.lean b/tests/lean/640b.lean index 09f4b5834..5e74dc290 100644 --- a/tests/lean/640b.lean +++ b/tests/lean/640b.lean @@ -1,2 +1,2 @@ -abbreviation bar [parsing-only] := @eq +abbreviation bar [parsing_only] := @eq check @bar diff --git a/tests/lean/671.lean.expected.out b/tests/lean/671.lean.expected.out index d1e192519..8e8eba1fc 100644 --- a/tests/lean/671.lean.expected.out +++ b/tests/lean/671.lean.expected.out @@ -1,2 +1,2 @@ -definition nat.add : ℕ → ℕ → ℕ := -λ (a b : ℕ), nat.rec_on b a (λ (b₁ : ℕ), nat.succ) +protected definition nat.add : ℕ → ℕ → ℕ := +λ (a : ℕ), nat.rec a (λ (b₁ : ℕ), nat.succ) diff --git a/tests/lean/704.lean b/tests/lean/704.lean index 90ca2ba0b..0457fcfb7 100644 --- a/tests/lean/704.lean +++ b/tests/lean/704.lean @@ -1,4 +1,4 @@ open classical -eval if true then 1 else 0 +eval if true then 1 else (0:num) attribute prop_decidable [priority 0] -eval if true then 1 else 0 +eval if true then 1 else (0:num) diff --git a/tests/lean/737.lean b/tests/lean/737.lean deleted file mode 100644 index 977c72c0c..000000000 --- a/tests/lean/737.lean +++ /dev/null @@ -1,237 +0,0 @@ -/- -Copyright (c) 2015 Robert Y. Lewis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Robert Y. Lewis -The real numbers, constructed as equivalence classes of Cauchy sequences of rationals. -This construction follows Bishop and Bridges (1985). - -To do: - o Break positive naturals into their own file and fill in sorry's - o Fill in sorrys for helper lemmas that will not be handled by simplifier - o Rename things and possibly make theorems private --/ - -import data.nat data.rat.order data.pnat -open nat eq eq.ops pnat -open -[coercions] rat -local notation 0 := rat.of_num 0 -local notation 1 := rat.of_num 1 ----------------------------------------------------------------------------------------------------- - -------------------------------------- --- theorems to add to (ordered) field and/or rat - --- this can move to pnat once sorry is filled in -theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c ∧ c > 0 := -sorry -theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := -sorry - -theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) : - q * n⁻¹ ≤ ε := -sorry -theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) : - p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := -sorry - -theorem find_thirds (a b : ℚ) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b := sorry - -theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b := -sorry - -theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b := -sorry - -theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d := -sorry - -theorem rewrite_helper3 (a b c d e f g: ℚ) : a * (b + c) - (d * e + f * g) = - (a * b - d * e) + (a * c - f * g) := -sorry - -theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) := sorry - -theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) := sorry - -theorem rewrite_helper7 (a b c d x : ℚ) : - a * b * c - d = (b * c) * (a - x) + (x * b * c - d) := sorry - -theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) - (H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) : - (rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ := sorry - -theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) := - sorry - -theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) := sorry - -namespace s - -notation `seq` := ℕ+ → ℚ - -definition regular (s : seq) := ∀ m n : ℕ+, abs (s m - s n) ≤ m⁻¹ + n⁻¹ - -definition equiv (s t : seq) := ∀ n : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹ -infix `≡` := equiv - -theorem equiv.refl (s : seq) : s ≡ s := -sorry - -theorem equiv.symm (s t : seq) (H : s ≡ t) : t ≡ s := -sorry - -theorem bdd_of_eq {s t : seq} (H : s ≡ t) : - ∀ j : ℕ+, ∀ n : ℕ+, n ≥ 2 * j → abs (s n - t n) ≤ j⁻¹ := -sorry - -theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t) - (H : ∀ j : ℕ+, ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ j⁻¹) : s ≡ t := -sorry - -theorem eq_of_bdd_var {s t : seq} (Hs : regular s) (Ht : regular t) - (H : ∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε) : s ≡ t := -sorry - -set_option pp.beta false -theorem pnat_bound {ε : ℚ} (Hε : ε > 0) : ∃ p : ℕ+, p⁻¹ ≤ ε := -sorry - -theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) : - ∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε := -sorry - -theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regular u) - (H : s ≡ t) (H2 : t ≡ u) : s ≡ u := -sorry - ------------------------------------ --- define operations on cauchy sequences. show operations preserve regularity - -definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1) dec_trivial - -theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) := -sorry - -definition K₂ (s t : seq) := max (K s) (K t) - -theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s := -sorry - -theorem canon_2_bound_left (s t : seq) (Hs : regular s) (n : ℕ+) : - abs (s n) ≤ rat_of_pnat (K₂ s t) := -sorry - -theorem canon_2_bound_right (s t : seq) (Ht : regular t) (n : ℕ+) : - abs (t n) ≤ rat_of_pnat (K₂ s t) := -sorry - -definition sadd (s t : seq) : seq := λ n, (s (2 * n)) + (t (2 * n)) - -theorem reg_add_reg {s t : seq} (Hs : regular s) (Ht : regular t) : regular (sadd s t) := -sorry - -definition smul (s t : seq) : seq := λ n : ℕ+, (s ((K₂ s t) * 2 * n)) * (t ((K₂ s t) * 2 * n)) - -theorem reg_mul_reg {s t : seq} (Hs : regular s) (Ht : regular t) : regular (smul s t) := -sorry - -definition sneg (s : seq) : seq := λ n : ℕ+, - (s n) - -theorem reg_neg_reg {s : seq} (Hs : regular s) : regular (sneg s) := -sorry ------------------------------------ --- show properties of +, *, - - -definition zero : seq := λ n, 0 - -definition one : seq := λ n, 1 - -theorem s_add_comm (s t : seq) : sadd s t ≡ sadd t s := -sorry - -theorem s_add_assoc (s t u : seq) (Hs : regular s) (Hu : regular u) : - sadd (sadd s t) u ≡ sadd s (sadd t u) := -sorry - -theorem s_mul_comm (s t : seq) : smul s t ≡ smul t s := -sorry - -definition DK (s t : seq) := (K₂ s t) * 2 -theorem DK_rewrite (s t : seq) : (K₂ s t) * 2 = DK s t := rfl - -definition TK (s t u : seq) := (DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u) - -theorem TK_rewrite (s t u : seq) : - (DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u) = TK s t u := rfl - -theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) : - abs (s a * t a * u b - s c * t d * u d) ≤ abs (t a) * abs (u b) * abs (s a - s c) + - abs (s c) * abs (t a) * abs (u b - u d) + abs (s c) * abs (u d) * abs (t a - t d) := -sorry - -definition Kq (s : seq) := rat_of_pnat (K s) + 1 - -theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s := -sorry - -theorem Kq_bound_nonneg {s : seq} (H : regular s) : 0 ≤ Kq s := - rat.le.trans !abs_nonneg (Kq_bound H 2) - -theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s := -sorry - -theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) - (a b c : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) ≤ (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) := -sorry - -theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) - (a b c d : ℕ+) : - abs (t a) * abs (u b) * abs (s a - s c) + abs (s c) * abs (t a) * abs (u b - u d) - + abs (s c) * abs (u d) * abs (t a - t d) ≤ - (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) + (Kq s) * (Kq t) * (b⁻¹ + d⁻¹) + (Kq s) * (Kq u) * (a⁻¹ + d⁻¹) := -sorry - -theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) : - smul (smul s t) u ≡ smul s (smul t u) := -sorry - -theorem zero_is_reg : regular zero := -sorry - -theorem s_zero_add (s : seq) (H : regular s) : sadd zero s ≡ s := -sorry - -theorem s_add_zero (s : seq) (H : regular s) : sadd s zero ≡ s := -sorry - -theorem s_neg_cancel (s : seq) (H : regular s) : sadd (sneg s) s ≡ zero := -sorry - -theorem neg_s_cancel (s : seq) (H : regular s) : sadd s (sneg s) ≡ zero := -sorry - -theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) - (Hv : regular v) (Esu : s ≡ u) (Etv : t ≡ v) : sadd s t ≡ sadd u v := -sorry - -theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) : - ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ := - begin - existsi pceil (((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * - (rat_of_pnat (K t))) * (rat_of_pnat j)), - intros n Hn, - rewrite rewrite_helper4, - apply rat.le.trans, - apply abs_add_le_abs_add_abs, - apply rat.le.trans, - rotate 1, - show n⁻¹ * ((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹)) + - n⁻¹ * ((a⁻¹ + c⁻¹) * (rat_of_pnat (K t))) ≤ j⁻¹, begin - rewrite -rat.left_distrib, - apply rat.le.trans, - apply rat.mul_le_mul_of_nonneg_right, - apply pceil_helper Hn, - repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos), - end -end -end s diff --git a/tests/lean/737.lean.expected.out b/tests/lean/737.lean.expected.out deleted file mode 100644 index 88195c48d..000000000 --- a/tests/lean/737.lean.expected.out +++ /dev/null @@ -1,43 +0,0 @@ -737.lean:235:5: error: 2 unsolved subgoals -s t : ℕ+ → ℚ, -Hs : regular s, -Ht : regular t, -a b c j n : ℕ+, -Hn : pceil ((rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) * rat_of_pnat j) ≤ n -⊢ 0 ≤ rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t) - -s t : ℕ+ → ℚ, -Hs : regular s, -Ht : regular t, -a b c j n : ℕ+, -Hn : pceil ((rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) * rat_of_pnat j) ≤ n -⊢ 1 / ((rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) * rat_of_pnat j) * (rat_of_pnat - (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≤ j⁻¹ -737.lean:228:4: error:invalid 'exact' tactic, term still contains metavariables after elaboration - show n⁻¹ * (rat_of_pnat (K s) * (b⁻¹ + c⁻¹)) + n⁻¹ * ((a⁻¹ + c⁻¹) * rat_of_pnat - (K t)) ≤ j⁻¹, from - ?M_1 -proof state: -s t : ℕ+ → ℚ, -Hs : regular s, -Ht : regular t, -a b c j n : ℕ+, -Hn : pceil ((rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) * rat_of_pnat j) ≤ n -⊢ ?M_1 ≤ j⁻¹ - -s t : ℕ+ → ℚ, -Hs : regular s, -Ht : regular t, -a b c j n : ℕ+, -Hn : pceil ((rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) * rat_of_pnat j) ≤ n -⊢ abs (s (a * n) * t (b * n) - s (a * n) * t (c * n)) + abs (s (a * n) * t (c * n) - s (c * n) * t (c * n)) ≤ ?M_1 -737.lean:236:0: error: don't know how to synthesize placeholder -s t : ℕ+ → ℚ, -Hs : regular s, -Ht : regular t, -a b c j : ℕ+ -⊢ ∃ (N : ℕ+), ∀ (n : ℕ+), - N ≤ n → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ -737.lean:236:0: error: failed to add declaration 's.mul_bound_helper' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - ?M_1 diff --git a/tests/lean/793a.lean b/tests/lean/793a.lean index 780daf69a..b23173eef 100644 --- a/tests/lean/793a.lean +++ b/tests/lean/793a.lean @@ -1,15 +1,14 @@ import data.rat - -check 4.0 -check 2.3 -check 1.00 -check 10.213 - open rat -check -0.3 -check 10.213 -check 2.3 -check 1.0 +check (4.0:rat) +check (2.3:rat) +check (1.00:rat) +check (10.213:rat) -eval (λ v, 1.0) 2 +check -(0.3:rat) +check (10.213:rat) +check (2.3:rat) +check (1.0:rat) + +eval (λ v, (1.0:rat)) (2:nat) diff --git a/tests/lean/793a.lean.expected.out b/tests/lean/793a.lean.expected.out index d76bfac2b..74f1fa4de 100644 --- a/tests/lean/793a.lean.expected.out +++ b/tests/lean/793a.lean.expected.out @@ -1,9 +1,9 @@ -rat.of_num 4 : ℚ -rat.divide (rat.of_num 23) (rat.of_num 10) : ℚ -rat.of_num 1 : ℚ -rat.divide (rat.of_num 10213) (rat.of_num 1000) : ℚ +4 : ℚ +23 / 10 : ℚ +1 : ℚ +10213 / 1000 : ℚ -(3 / 10) : ℚ 10213 / 1000 : ℚ 23 / 10 : ℚ 1 : ℚ -quot.mk (prerat.mk (int.of_nat (nat.succ nat.zero)) (int.of_nat (nat.succ nat.zero)) (int.of_nat_succ_pos nat.zero)) +quot.mk (prerat.mk (int.of_nat 1) (int.of_nat 1) (int.of_nat_succ_pos 0)) diff --git a/tests/lean/800.lean b/tests/lean/800.lean index b1528e773..bcf3ead72 100644 --- a/tests/lean/800.lean +++ b/tests/lean/800.lean @@ -14,4 +14,4 @@ check M[row,col] notation M `[` i `,` `:` `]` := get_row M i check M[row,:] check M[row,col] -check [1, 2, 3] +check [(1:nat), 2, 3] diff --git a/tests/lean/800.lean.expected.out b/tests/lean/800.lean.expected.out index 0f47b3763..626b56d60 100644 --- a/tests/lean/800.lean.expected.out +++ b/tests/lean/800.lean.expected.out @@ -1,4 +1,4 @@ M[row,col] : A M[row,:] : row_vector A n M[row,col] : A -[1, 2, 3] : list num +[1, 2, 3] : list ℕ diff --git a/tests/lean/K_bug.lean.expected.out b/tests/lean/K_bug.lean.expected.out index acf7bb0cf..e69de29bb 100644 --- a/tests/lean/K_bug.lean.expected.out +++ b/tests/lean/K_bug.lean.expected.out @@ -1,6 +0,0 @@ -K_bug.lean:14:24: error: type mismatch at term - pred_succ n⁻¹ -has type - pred (succ n⁻¹) = n⁻¹ -but is expected to have type - n = pred (succ n) diff --git a/tests/lean/bad_id.lean b/tests/lean/bad_id.lean index 7dec22b98..50ef61c6b 100644 --- a/tests/lean/bad_id.lean +++ b/tests/lean/bad_id.lean @@ -1,5 +1,5 @@ import data.num -definition x.y := 10 +definition x.y : nat := 10 -definition x.1 := 10 +definition x.1 :nat := 10 diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out index 4bfac196e..56929e9dc 100644 --- a/tests/lean/binder_overload.lean.expected.out +++ b/tests/lean/binder_overload.lean.expected.out @@ -1,7 +1,7 @@ {x : ℕ ∈ S | x > 0} : set ℕ {x : ℕ ∈ s | x > 0} : finset ℕ -@set.sep.{1} nat (λ (x : nat), nat.gt x (nat.of_num 0)) S : set.{1} nat -@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), nat.gt x (nat.of_num 0)) - (λ (a : nat), nat.decidable_ge a (nat.succ (nat.of_num 0))) +@set.sep.{1} nat (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) S : set.{1} nat +@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) + (λ (a : nat), nat.decidable_lt 0 a) s : finset.{1} nat diff --git a/tests/lean/errors.lean b/tests/lean/errors.lean index 18a8d78e9..f841286ed 100644 --- a/tests/lean/errors.lean +++ b/tests/lean/errors.lean @@ -9,7 +9,7 @@ definition tst2 : nat → nat → nat := begin intro a, intro b, - cases add wth (a, b), -- ERROR + cases nat.add wth (a, b), -- ERROR exact a, exact b, end diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out index 4d018e263..0b71c1332 100644 --- a/tests/lean/errors.lean.expected.out +++ b/tests/lean/errors.lean.expected.out @@ -1,6 +1,6 @@ errors.lean:4:0: error: unknown identifier 'a' tst1 : ℕ → ℕ → ℕ -errors.lean:12:8: error: unknown identifier 'add' +errors.lean:12:16: error: unknown identifier 'wth' errors.lean:22:12: error: unknown identifier 'b' tst3 : A → A → A foo.tst1 : ℕ → ℕ → ℕ diff --git a/tests/lean/extra/bag.lean b/tests/lean/extra/bag.lean index e3a6fa5b4..2ff063bbd 100644 --- a/tests/lean/extra/bag.lean +++ b/tests/lean/extra/bag.lean @@ -6,7 +6,7 @@ Author: Leonardo de Moura Finite bags. -/ import data.nat data.list.perm algebra.binary -open nat quot list subtype binary function eq.ops +open nat quot list subtype binary function eq.ops algebra open [declarations] perm variable {A : Type} diff --git a/tests/lean/extra/eqn_macro1.lean b/tests/lean/extra/eqn_macro1.lean index 2c753a387..55a65706a 100644 --- a/tests/lean/extra/eqn_macro1.lean +++ b/tests/lean/extra/eqn_macro1.lean @@ -2,7 +2,7 @@ open nat notation `foo` a := match a with - (c, d) := c + d + (c, d) := c +[nat] d end eval foo (2, 3) diff --git a/tests/lean/extra/print_info.12.19.expected.out b/tests/lean/extra/print_info.12.19.expected.out index 885bc42df..1cc9c1427 100644 --- a/tests/lean/extra/print_info.12.19.expected.out +++ b/tests/lean/extra/print_info.12.19.expected.out @@ -1,5 +1,3 @@ LEAN_INFORMATION -definition int.mul : ℤ → ℤ → ℤ - -definition nat.mul : ℕ → ℕ → ℕ +definition mul : Π {A : Type} [c : has_mul A], A → A → A END_LEAN_INFORMATION diff --git a/tests/lean/extra/print_info.12.20.expected.out b/tests/lean/extra/print_info.12.20.expected.out index 885bc42df..1cc9c1427 100644 --- a/tests/lean/extra/print_info.12.20.expected.out +++ b/tests/lean/extra/print_info.12.20.expected.out @@ -1,5 +1,3 @@ LEAN_INFORMATION -definition int.mul : ℤ → ℤ → ℤ - -definition nat.mul : ℕ → ℕ → ℕ +definition mul : Π {A : Type} [c : has_mul A], A → A → A END_LEAN_INFORMATION diff --git a/tests/lean/extra/print_info.21.3.expected.out b/tests/lean/extra/print_info.21.3.expected.out index 384e15f05..750b3916b 100644 --- a/tests/lean/extra/print_info.21.3.expected.out +++ b/tests/lean/extra/print_info.21.3.expected.out @@ -1,5 +1,3 @@ LEAN_INFORMATION -_ `+`:65 _:65 := - | nat.add #1 #0 - | [priority 999] int.add #1 #0 +_ `+`:65 _:65 := add #1 #0 END_LEAN_INFORMATION diff --git a/tests/lean/extra/print_info.7.18.expected.out b/tests/lean/extra/print_info.7.18.expected.out index 05b8c32c5..24056b2ae 100644 --- a/tests/lean/extra/print_info.7.18.expected.out +++ b/tests/lean/extra/print_info.7.18.expected.out @@ -1,5 +1,3 @@ LEAN_INFORMATION -definition int.add : ℤ → ℤ → ℤ - -definition nat.add : ℕ → ℕ → ℕ +definition add : Π {A : Type} [c : has_add A], A → A → A END_LEAN_INFORMATION diff --git a/tests/lean/extra/print_info.8.19.expected.out b/tests/lean/extra/print_info.8.19.expected.out index 384e15f05..750b3916b 100644 --- a/tests/lean/extra/print_info.8.19.expected.out +++ b/tests/lean/extra/print_info.8.19.expected.out @@ -1,5 +1,3 @@ LEAN_INFORMATION -_ `+`:65 _:65 := - | nat.add #1 #0 - | [priority 999] int.add #1 #0 +_ `+`:65 _:65 := add #1 #0 END_LEAN_INFORMATION diff --git a/tests/lean/extra/show_goal.18.20.expected.out b/tests/lean/extra/show_goal.18.20.expected.out index 4c941a1c8..cfafefe97 100644 --- a/tests/lean/extra/show_goal.18.20.expected.out +++ b/tests/lean/extra/show_goal.18.20.expected.out @@ -6,6 +6,6 @@ h₂ : b = 0, aeq0 : a = 0, h₃ : succ c = 1, h₄ : d = c - 1, -a_eq : c = 0 +a_1 : c = 0 ⊢ c = 0 END_LEAN_INFORMATION diff --git a/tests/lean/extra/show_goal.lean b/tests/lean/extra/show_goal.lean index 47b83ab3d..2756bdc1f 100644 --- a/tests/lean/extra/show_goal.lean +++ b/tests/lean/extra/show_goal.lean @@ -15,11 +15,11 @@ begin rewrite add_zero at h₃, rewrite add_succ at h₃, rewrite add_zero at h₃, - injection h₃, assumption + injection h₃, exact a_1 end, rewrite ceq at h₄, repeat (esimp [sub, pred] at h₄), - assumption + exact h₄ end, exact deq0 end diff --git a/tests/lean/hott/457.hlean b/tests/lean/hott/457.hlean index cf24871b6..63057da12 100644 --- a/tests/lean/hott/457.hlean +++ b/tests/lean/hott/457.hlean @@ -5,7 +5,6 @@ open eq algebra definition foo {A : Type} (a b c : A) (H₁ : a = c) (H₂ : c = b) : a = b := begin apply concat, - rotate 1, + apply H₁, apply H₂, - apply H₁ end diff --git a/tests/lean/interactive/auto_comp.input.expected.out b/tests/lean/interactive/auto_comp.input.expected.out index 2880ae1b5..40c3370a0 100644 --- a/tests/lean/interactive/auto_comp.input.expected.out +++ b/tests/lean/interactive/auto_comp.input.expected.out @@ -2,11 +2,11 @@ -- ENDWAIT -- BEGINFINDP le.rec_on|le ?a ?a → (Π (a : nat), ?C a a) → ?C ?a ?a -nat.rec_on|Π (n : nat), ?C zero → (Π (a : nat), ?C a → ?C (succ a)) → ?C n +nat.rec_on|Π (n : nat), ?C 0 → (Π (a : nat), ?C a → ?C (succ a)) → ?C n bool.rec_on|Π (n : bool), ?C bool.ff → ?C bool.tt → ?C n -- ENDFINDP -- BEGINFINDP nat.le.rec_on|nat.le ?a ?a → (Π (a : nat), ?C a a) → ?C ?a ?a -nat.rec_on|Π (n : nat), ?C nat.zero → (Π (a : nat), ?C a → ?C (nat.succ a)) → ?C n +nat.rec_on|Π (n : nat), ?C 0 → (Π (a : nat), ?C a → ?C (nat.succ a)) → ?C n bool.rec_on|Π (n : bool), ?C bool.ff → ?C bool.tt → ?C n -- ENDFINDP diff --git a/tests/lean/interactive/commands.input.expected.out b/tests/lean/interactive/commands.input.expected.out index f8cfd3b2b..eee34128f 100644 --- a/tests/lean/interactive/commands.input.expected.out +++ b/tests/lean/interactive/commands.input.expected.out @@ -27,7 +27,6 @@ true -- ACK -- ENDINFO -- BEGINFINDG -add.assoc|∀ (n m k : ℕ), n + m + k = n + (m + k) -- ENDFINDG -- BEGINWAIT -- ENDWAIT diff --git a/tests/lean/interactive/consume_args.input.expected.out b/tests/lean/interactive/consume_args.input.expected.out index 4d75f4d54..de3427601 100644 --- a/tests/lean/interactive/consume_args.input.expected.out +++ b/tests/lean/interactive/consume_args.input.expected.out @@ -49,7 +49,15 @@ nat.add.assoc -- TYPE|7|43 a + c + b = a + (c + b) → a + (c + b) = a + c + b -- ACK +-- OVERLOAD|7|43 +eq.symm #0 +-- +inv #0 +-- ACK -- SYMBOL|7|43 ⁻¹ -- ACK +-- IDENTIFIER|7|43 +eq.symm +-- ACK -- ENDINFO diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out index 25e5ce314..f8f4c4b86 100644 --- a/tests/lean/interactive/findp.input.expected.out +++ b/tests/lean/interactive/findp.input.expected.out @@ -9,15 +9,15 @@ false.rec_on|Π (C : Type), false → C false.cases_on|Π (C : Type), false → C false.induction_on|∀ (C : Prop), false → C true_ne_false|¬true = false -nat.lt_self_iff_false|∀ (n : ℕ), nat.lt n n ↔ false +nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false not_of_is_false|is_false ?c → ¬?c not_of_iff_false|(?a ↔ false) → ¬?a is_false|Π (c : Prop) [H : decidable c], Prop classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false classical.eq_false_or_eq_true|∀ (a : Prop), a = false ∨ a = true -nat.lt_zero_iff_false|∀ (a : ℕ), nat.lt a nat.zero ↔ false +nat.lt_zero_iff_false|∀ (a : ℕ), a < 0 ↔ false not_of_eq_false|?p = false → ¬?p -nat.succ_le_self_iff_false|∀ (n : ℕ), nat.le (nat.succ n) n ↔ false +nat.succ_le_self_iff_false|∀ (n : ℕ), nat.succ n ≤ n ↔ false decidable.rec_on_false|Π (H3 : ¬?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2 not_false|¬false decidable_false|decidable false @@ -25,6 +25,6 @@ of_not_is_false|¬is_false ?c → ?c classical.cases_true_false|∀ (P : Prop → Prop), P true → P false → (∀ (a : Prop), P a) iff_false_intro|¬?a → (?a ↔ false) ne_false_of_self|?p → ?p ≠ false -nat.succ_le_zero_iff_false|∀ (n : ℕ), nat.le (nat.succ n) nat.zero ↔ false +nat.succ_le_zero_iff_false|∀ (n : ℕ), nat.succ n ≤ 0 ↔ false tactic.exfalso|tactic -- ENDFINDP diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out index a9616bb94..233b2524a 100644 --- a/tests/lean/interactive/num2.input.expected.out +++ b/tests/lean/interactive/num2.input.expected.out @@ -27,7 +27,10 @@ pos_num.lt|pos_num → pos_num → bool pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n pos_num.add|pos_num → pos_num → pos_num +pos_num_has_mul|has_mul pos_num pos_num|Type +pos_num_has_one|has_one pos_num +pos_num_has_add|has_add pos_num -- ENDFINDP -- BEGINWAIT -- ENDWAIT @@ -57,7 +60,10 @@ pos_num.lt|pos_num → pos_num → bool pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n pos_num.add|pos_num → pos_num → pos_num +pos_num_has_mul|has_mul pos_num pos_num|Type +pos_num_has_one|has_one pos_num +pos_num_has_add|has_add pos_num -- ENDFINDP -- BEGINFINDP pos_num.size|pos_num → pos_num @@ -83,5 +89,8 @@ pos_num.lt|pos_num → pos_num → bool pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n pos_num.brec_on|Π (n : pos_num), (Π (n : pos_num), pos_num.below n → ?C n) → ?C n pos_num.add|pos_num → pos_num → pos_num +pos_num_has_mul|has_mul pos_num pos_num|Type +pos_num_has_one|has_one pos_num +pos_num_has_add|has_add pos_num -- ENDFINDP diff --git a/tests/lean/interactive/overload_coercion.input b/tests/lean/interactive/overload_coercion.input index f7f6e967f..fc11aa905 100644 --- a/tests/lean/interactive/overload_coercion.input +++ b/tests/lean/interactive/overload_coercion.input @@ -4,7 +4,7 @@ open nat num variable a : nat variable b : num variable c : bool -check a + b +check a + of_num b check add a c WAIT INFO 5 diff --git a/tests/lean/interactive/overload_coercion.input.expected.out b/tests/lean/interactive/overload_coercion.input.expected.out index 464067eb0..685b1d58f 100644 --- a/tests/lean/interactive/overload_coercion.input.expected.out +++ b/tests/lean/interactive/overload_coercion.input.expected.out @@ -10,37 +10,30 @@ a -- TYPE|5|8 ℕ → ℕ → ℕ -- ACK --- OVERLOAD|5|8 -num.add #1 #0 --- -nat.add #1 #0 --- ACK -- SYMBOL|5|8 + -- ACK --- IDENTIFIER|5|8 -nat.add --- ACK -- TYPE|5|10 -num --- ACK --- COERCION|5|10 -of_num b --- -ℕ +num → ℕ -- ACK -- IDENTIFIER|5|10 +nat.of_num +-- ACK +-- TYPE|5|17 +num +-- ACK +-- IDENTIFIER|5|17 b -- ACK -- ENDINFO -- BEGININFO STALE -- TYPE|6|6 -ℕ → ℕ → ℕ +num → num → num -- ACK -- OVERLOAD|6|6 -num.add +add -- -nat.add +num.add -- ACK -- TYPE|6|10 ℕ diff --git a/tests/lean/lift_coe_off.lean b/tests/lean/lift_coe_off.lean index 279f3b6ce..a14e48fdd 100644 --- a/tests/lean/lift_coe_off.lean +++ b/tests/lean/lift_coe_off.lean @@ -4,12 +4,12 @@ inductive tree (A : Type) := leaf : A → tree A, node : tree A → tree A → tree A -set_option elaborator.lift_coercions false +-- set_option elaborator.lift_coercions false -definition size {A : Type} (t : tree A) := +definition size {A : Type} (t : tree A) :nat:= tree.rec (λ a, 1) (λ t₁ t₂ n₁ n₂, n₁ + n₂) t -set_option elaborator.lift_coercions true +--set_option elaborator.lift_coercions true -definition size {A : Type} (t : tree A) := +definition size2 {A : Type} (t : tree A) :nat:= tree.rec (λ a, 1) (λ t₁ t₂ n₁ n₂, n₁ + n₂) t diff --git a/tests/lean/lift_coe_off.lean.expected.out b/tests/lean/lift_coe_off.lean.expected.out index 4817487fb..e69de29bb 100644 --- a/tests/lean/lift_coe_off.lean.expected.out +++ b/tests/lean/lift_coe_off.lean.expected.out @@ -1,10 +0,0 @@ -lift_coe_off.lean:10:0: error: type mismatch at application - tree.rec (λ (a : A), 1) (λ (t₁ t₂ : tree A) (n₁ : ?M_1) (n₂ : ?M_2), ?M_3 + ?M_4) -term - λ (t₁ t₂ : tree A) (n₁ : ?M_1) (n₂ : ?M_2), - ?M_3 + ?M_4 -has type - Π (t₁ t₂ : tree A) (n₁ : ?M_1), - ?M_2 → ℕ -but is expected to have type - tree A → tree A → num → num → num diff --git a/tests/lean/local_notation_bug.lean.expected.out b/tests/lean/local_notation_bug.lean.expected.out index 078887245..a067dd6de 100644 --- a/tests/lean/local_notation_bug.lean.expected.out +++ b/tests/lean/local_notation_bug.lean.expected.out @@ -1,6 +1,5 @@ f a b : A f a b : A nat ↣ bool : foo -bla : num +10 : ?M_1 local_notation_bug.lean:22:8: error: invalid expression -num ↣ nat : nat.of_num diff --git a/tests/lean/mismatch.lean b/tests/lean/mismatch.lean index eaa1bfd94..6d805091b 100644 --- a/tests/lean/mismatch.lean +++ b/tests/lean/mismatch.lean @@ -1,3 +1,4 @@ definition id {A : Type} {a : A} := a +definition o : num := 1 -check @id nat 1 +check @id nat o diff --git a/tests/lean/mismatch.lean.expected.out b/tests/lean/mismatch.lean.expected.out index a8ea208ea..0f7ceb7e3 100644 --- a/tests/lean/mismatch.lean.expected.out +++ b/tests/lean/mismatch.lean.expected.out @@ -1,7 +1,7 @@ -mismatch.lean:3:7: error: type mismatch at application - @id ℕ 1 +mismatch.lean:4:7: error: type mismatch at application + @id ℕ o term - 1 + o has type num but is expected to have type diff --git a/tests/lean/namespace_bug.lean.expected.out b/tests/lean/namespace_bug.lean.expected.out index 3a51b03f0..48d80bcbb 100644 --- a/tests/lean/namespace_bug.lean.expected.out +++ b/tests/lean/namespace_bug.lean.expected.out @@ -1 +1,8 @@ -namespace_bug.lean:3:7: error: invalid expression +namespace_bug.lean:3:6: error: type mismatch at application + @bit0 ?A +term + ?A +has type + Type.{l_2} +but is expected to have type + Type.{l_3} diff --git a/tests/lean/nary_overload2.lean b/tests/lean/nary_overload2.lean index 483cc9271..cdd13d0da 100644 --- a/tests/lean/nary_overload2.lean +++ b/tests/lean/nary_overload2.lean @@ -1,13 +1,13 @@ import data.list data.examples.vector open nat list vector -check [1, 2, 3] +check [(1:nat), 2, 3] check ([1, 2, 3] : vector nat _) check ([1, 2, 3] : list nat) -check (#list [1, 2, 3]) -check (#vector [1, 2, 3]) +check (#list [(1:nat), 2, 3]) +check (#vector [(1:nat), 2, 3]) -example : (#vector [1, 2, 3]) = [1, 2, 3] := +example : (#vector [1, 2, 3]) = [(1:nat), 2, 3] := rfl example : (#vector [1, 2, 3]) = ([1, 2, 3] : vector nat _) := diff --git a/tests/lean/nary_overload2.lean.expected.out b/tests/lean/nary_overload2.lean.expected.out index d331da9b6..a4137e901 100644 --- a/tests/lean/nary_overload2.lean.expected.out +++ b/tests/lean/nary_overload2.lean.expected.out @@ -1,5 +1,5 @@ -[1, 2, 3] : list num +[1, 2, 3] : list ℕ [1, 2, 3] : vector ℕ 3 [1, 2, 3] : list ℕ -[1, 2, 3] : list num -[1, 2, 3] : vector num 3 +[1, 2, 3] : list ℕ +[1, 2, 3] : vector ℕ 3 diff --git a/tests/lean/nat_pp.lean.expected.out b/tests/lean/nat_pp.lean.expected.out index d591df36a..07d39ab34 100644 --- a/tests/lean/nat_pp.lean.expected.out +++ b/tests/lean/nat_pp.lean.expected.out @@ -1,3 +1,3 @@ -nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ nat.zero)))))))) +9 9 9 diff --git a/tests/lean/noncomp_error.lean b/tests/lean/noncomp_error.lean index 8f49f6777..c80134c9b 100644 --- a/tests/lean/noncomp_error.lean +++ b/tests/lean/noncomp_error.lean @@ -1 +1 @@ -noncomputable definition a := 2 +noncomputable definition a :nat := 2 diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean/noncomp_theory.lean.expected.out index 4742251fe..07d4bbd0a 100644 --- a/tests/lean/noncomp_theory.lean.expected.out +++ b/tests/lean/noncomp_theory.lean.expected.out @@ -1,5 +1,5 @@ -noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.divide' +noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.real_has_division' noncomputable definition g : ℝ → ℝ → ℝ := -λ (a : ℝ), divide (a + a) +λ (a : ℝ), division (a + a) definition r : ℕ → ℕ := λ (a : ℕ), a diff --git a/tests/lean/notation.lean b/tests/lean/notation.lean index d68eeb1db..e9cef7b60 100644 --- a/tests/lean/notation.lean +++ b/tests/lean/notation.lean @@ -4,10 +4,10 @@ constant b : num check b + b + b check true ∧ false ∧ true check (true ∧ false) ∧ true -check 2 + (2 + 2) -check (2 + 2) + 2 -check 1 = (2 + 3)*2 -check 2 + 3 * 2 = 3 * 2 + 2 +check (2:num) + (2 + 2) +check (2 + 2) + (2:num) +check (1:num) = (2 + 3)*2 +check (2:num) + 3 * 2 = 3 * 2 + 2 check (true ∨ false) = (true ∨ false) ∧ true check true ∧ (false ∨ true) constant A : Type₁ diff --git a/tests/lean/notation2.lean b/tests/lean/notation2.lean index a1c631b1c..e4f6c40c3 100644 --- a/tests/lean/notation2.lean +++ b/tests/lean/notation2.lean @@ -1,5 +1,5 @@ import data.num inductive list (T : Type) : Type := nil {} : list T | cons : T → list T → list T open list notation h :: t := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l infixr `::` := cons -check 1 :: 2 :: nil -check 1 :: 2 :: 3 :: 4 :: 5 :: nil +check (1:num) :: 2 :: nil +check (1:num) :: 2 :: 3 :: 4 :: 5 :: nil diff --git a/tests/lean/notation3.lean b/tests/lean/notation3.lean index 6452742a9..bece0aae6 100644 --- a/tests/lean/notation3.lean +++ b/tests/lean/notation3.lean @@ -5,4 +5,4 @@ constants a b : num check [a, b, b] check (a, true, a = b, b) check (a, b) -check [1, 2+2, 3] +check [(1:num), 2+2, 3] diff --git a/tests/lean/notation6.lean b/tests/lean/notation6.lean index bd1eea649..a98117c8e 100644 --- a/tests/lean/notation6.lean +++ b/tests/lean/notation6.lean @@ -1,9 +1,9 @@ import logic data.num open num -notation `o` := 10 +notation `o` := (10:num) check 11 constant f : num → num check o + 1 check f o + o + o -eval 9 + 1 +eval 9 + (1:num) eval o+4 diff --git a/tests/lean/notation6.lean.expected.out b/tests/lean/notation6.lean.expected.out index 84a39dc83..f88a24a37 100644 --- a/tests/lean/notation6.lean.expected.out +++ b/tests/lean/notation6.lean.expected.out @@ -1,5 +1,5 @@ -11 : num -o + 1 : num -f o + o + o : num -o +11 : ?M_1 +10 + 1 : num +f 10 + 10 + 10 : num +10 14 diff --git a/tests/lean/notation_priority.lean.expected.out b/tests/lean/notation_priority.lean.expected.out index 049aace77..cd1835f9a 100644 --- a/tests/lean/notation_priority.lean.expected.out +++ b/tests/lean/notation_priority.lean.expected.out @@ -1,4 +1,4 @@ -nat.add a b : nat -int.add i j : int -nat.add a b : nat -int.add i j : int +@add.{1} nat 11.source.to.has_add a b : nat +@add.{1} int 11.source.to.has_add_1 i j : int +@add.{1} nat 11.source.to.has_add a b : nat +@add.{1} int 11.source.to.has_add_1 i j : int diff --git a/tests/lean/num.lean.expected.out b/tests/lean/num.lean.expected.out index b3a0060ff..9a7686fd1 100644 --- a/tests/lean/num.lean.expected.out +++ b/tests/lean/num.lean.expected.out @@ -1,12 +1,12 @@ -10 : num -20 : num -3 : num -1 : num -0 : num -12 : num -13 : num -12138 : num -1221 : num -11 : num -5 : num -21 : num +10 : ?M_1 +20 : ?M_1 +3 : ?M_1 +1 : ?M_1 +0 : ?M_1 +12 : ?M_1 +13 : ?M_1 +12138 : ?M_1 +1221 : ?M_1 +11 : ?M_1 +5 : ?M_1 +21 : ?M_1 diff --git a/tests/lean/num3.lean b/tests/lean/num3.lean index bba618b98..077543149 100644 --- a/tests/lean/num3.lean +++ b/tests/lean/num3.lean @@ -12,3 +12,4 @@ notation 1 := o check a = 0 check 2 = 1 +check (2:num) = 1 diff --git a/tests/lean/num3.lean.expected.out b/tests/lean/num3.lean.expected.out index 77c4caf65..ea51ac4f6 100644 --- a/tests/lean/num3.lean.expected.out +++ b/tests/lean/num3.lean.expected.out @@ -1,2 +1,3 @@ @eq N a z : Prop +@eq ?M_1 2 1 : Prop @eq num 2 1 : Prop diff --git a/tests/lean/num4.lean b/tests/lean/num4.lean index f5fd4d670..362b14cf8 100644 --- a/tests/lean/num4.lean +++ b/tests/lean/num4.lean @@ -13,7 +13,7 @@ namespace foo check a = 0 end foo -check 2 = 1 +check (2:nat) = 1 check #foo foo.a = 1 open foo diff --git a/tests/lean/num4.lean.expected.out b/tests/lean/num4.lean.expected.out index b7030c5c1..120bc5761 100644 --- a/tests/lean/num4.lean.expected.out +++ b/tests/lean/num4.lean.expected.out @@ -1,4 +1,4 @@ @eq N a z : Prop -@eq num 2 1 : Prop +@eq nat 2 1 : Prop @eq foo.N foo.a foo.o : Prop @eq N a o : Prop diff --git a/tests/lean/num5.lean b/tests/lean/num5.lean index e10ac4cfb..7b80f7a68 100644 --- a/tests/lean/num5.lean +++ b/tests/lean/num5.lean @@ -1,7 +1,7 @@ import data.num open num -eval 3+2 -eval 3+2*5 -eval 5*5 -eval eq.rec (eq.refl 2) (eq.refl 2) +eval 3+(2:num) +eval 3+2*(5:num) +eval 5*(5:num) +eval eq.rec (eq.refl (2:num)) (eq.refl (2:num)) diff --git a/tests/lean/open_tst.lean b/tests/lean/open_tst.lean index 548c8deb3..fccc82380 100644 --- a/tests/lean/open_tst.lean +++ b/tests/lean/open_tst.lean @@ -1,15 +1,13 @@ section - open [notations] [coercions] nat - check 1 + 2 - check add -- Error aliases were not created + check (1:nat) + 2 + check add end section - open [declarations] [notations] nat variable a : nat check a + a check add a a - check a + 1 -- Error coercion from num to nat was not loaded + check a + 1 end section @@ -26,7 +24,6 @@ section open - [classes] [decls] nat variable a : nat check a + a - check add a a -- Error aliases were not created check a + 1 definition foo2 : inhabited nat := _ -- Error inhabited instances was not loaded @@ -38,5 +35,5 @@ section _ variable a : nat - check a + a -- Error notation declarations were not loaded + check a + a end diff --git a/tests/lean/open_tst.lean.expected.out b/tests/lean/open_tst.lean.expected.out index 75dd74a81..da2db0a88 100644 --- a/tests/lean/open_tst.lean.expected.out +++ b/tests/lean/open_tst.lean.expected.out @@ -1,31 +1,23 @@ 1 + 2 : ℕ -open_tst.lean:4:8: error: unknown identifier 'add' -a + a : ℕ -a + a : ℕ -open_tst.lean:12:10: error: type mismatch at application - a + 1 -term - 1 -has type - num -but is expected to have type - ℕ +add : ?A → ?A → ?A a + a : ℕ a + a : ℕ a + 1 : ℕ -open_tst.lean:22:2: error: don't know how to synthesize placeholder +a + a : ℕ +a + a : ℕ +a + 1 : ℕ +open_tst.lean:20:2: error: don't know how to synthesize placeholder ⊢ inhabited ℕ -open_tst.lean:22:2: error: failed to add declaration 'foo1' to environment, value has metavariables +open_tst.lean:20:2: error: failed to add declaration 'foo1' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term ?M_1 a + a : ℕ -open_tst.lean:29:8: error: unknown identifier 'add' a + 1 : ℕ -open_tst.lean:32:2: error: don't know how to synthesize placeholder +open_tst.lean:29:2: error: don't know how to synthesize placeholder ⊢ inhabited ℕ -open_tst.lean:32:2: error: failed to add declaration 'foo2' to environment, value has metavariables +open_tst.lean:29:2: error: failed to add declaration 'foo2' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term ?M_1 -open_tst.lean:41:10: error: invalid expression +a + a : ℕ diff --git a/tests/lean/param.lean b/tests/lean/param.lean index 01c874eb8..6c8ab07a2 100644 --- a/tests/lean/param.lean +++ b/tests/lean/param.lean @@ -1,7 +1,7 @@ import data.num open num -definition foo1 a b c := a + b + c +definition foo1 a b c := a + b + (c:num) definition foo2 (a : num) b c := a + b + c diff --git a/tests/lean/parsing_only.lean b/tests/lean/parsing_only.lean index b15253be2..e542e4cc6 100644 --- a/tests/lean/parsing_only.lean +++ b/tests/lean/parsing_only.lean @@ -3,7 +3,7 @@ import logic constant f : num → num constant g : num → num notation a `+++` := f a -notation [parsing-only] a `***` := g a +notation [parsing_only] a `***` := g a check 10 +++ check 10 *** check Type.{8} -- Type₊ should not be used diff --git a/tests/lean/pp_algebra_num_bug.lean.expected.out b/tests/lean/pp_algebra_num_bug.lean.expected.out index c0ec37250..4f9d8d1ff 100644 --- a/tests/lean/pp_algebra_num_bug.lean.expected.out +++ b/tests/lean/pp_algebra_num_bug.lean.expected.out @@ -1,4 +1,4 @@ 1 * 1 * a : A -has_mul.mul (has_one.one A) a : A +mul 1 a : A 0 + a : A -has_add.add (has_zero.zero A) a : A +add 0 a : A diff --git a/tests/lean/pp_all.lean b/tests/lean/pp_all.lean index 08a1d25c5..d6bb290d7 100644 --- a/tests/lean/pp_all.lean +++ b/tests/lean/pp_all.lean @@ -1,9 +1,10 @@ +import data.nat open nat variables {a : nat} -abbreviation b := 2 +abbreviation b : num := 2 -check (λ x, x) a + b = 10 +check (λ x, x) a + of_num b = 10 set_option pp.all true -check (λ x, x) a + b = 10 +check (λ x, x) a + of_num b = 10 diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index e01571659..c5eae488b 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,2 +1,2 @@ -a + b = 10 : Prop -@eq.{1} nat (nat.add ((λ (x : nat), x) a) (nat.of_num 2)) (nat.of_num 10) : Prop +a + of_num b = 10 : Prop +@eq.{1} nat (@add.{1} nat 11.source.to.has_add ((λ (x : nat), x) a) (nat.of_num 2)) 10 : Prop diff --git a/tests/lean/print_ax3.lean b/tests/lean/print_ax3.lean index 6101b7d62..d2032e09d 100644 --- a/tests/lean/print_ax3.lean +++ b/tests/lean/print_ax3.lean @@ -1,13 +1,13 @@ -theorem foo1 : 0 = 0 := +theorem foo1 : 0 = (0:num) := rfl -theorem foo2 : 0 = 0 := +theorem foo2 : 0 = (0:num) := rfl -theorem foo3 : 0 = 0 := +theorem foo3 : 0 = (0:num) := foo2 -definition foo4 : 0 = 0 := +definition foo4 : 0 = (0:num) := eq.trans foo2 foo1 print axioms foo4 diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out index f2ed48d97..86174bc94 100644 --- a/tests/lean/protected_test.lean.expected.out +++ b/tests/lean/protected_test.lean.expected.out @@ -1,7 +1,7 @@ protected_test.lean:2:8: error: unknown identifier 'induction_on' protected_test.lean:3:8: error: unknown identifier 'rec_on' nat.induction_on : ∀ (n : ℕ), ?C 0 → (∀ (a : ℕ), ?C a → ?C (succ a)) → ?C n -le.rec_on : ?a ≤ ?a_1 → ?C ?a → (∀ {b : ℕ}, ?a ≤ b → ?C b → ?C (succ b)) → ?C ?a_1 -le.rec_on : ?a ≤ ?a_1 → ?C ?a → (∀ {b : ℕ}, ?a ≤ b → ?C b → ?C (succ b)) → ?C ?a_1 +le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b : ℕ}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1 +le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b : ℕ}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1 protected_test.lean:8:10: error: unknown identifier 'rec_on' -le.rec_on : ?a ≤ ?a_1 → ?C ?a → (∀ {b : ℕ}, ?a ≤ b → ?C b → ?C (succ b)) → ?C ?a_1 \ No newline at end of file +le.rec_on : le ?a ?a_1 → ?C ?a → (∀ {b : ℕ}, le ?a b → ?C b → ?C (succ b)) → ?C ?a_1 diff --git a/tests/lean/rateval.lean b/tests/lean/rateval.lean index 1133b32c6..bc458ed64 100644 --- a/tests/lean/rateval.lean +++ b/tests/lean/rateval.lean @@ -3,4 +3,4 @@ open nat int rat attribute rat.of_int [coercion] -eval (8 * 6⁻¹) + 1 +eval (8 * 6⁻¹) + (1:rat) diff --git a/tests/lean/rateval.lean.expected.out b/tests/lean/rateval.lean.expected.out index 540625902..c40054216 100644 --- a/tests/lean/rateval.lean.expected.out +++ b/tests/lean/rateval.lean.expected.out @@ -1 +1,13 @@ -quot.mk (prerat.mk 14 6 (mul_denom_pos (prerat.mul (prerat.of_int 8) (prerat.inv (prerat.of_int 6))) (prerat.of_int 1))) +quot.mk + (prerat.mk 14 6 + (mul_denom_pos + (prerat.mul + (prerat.add + (prerat.add (prerat.add (prerat.of_int 1) (prerat.of_int 1)) + (prerat.add (prerat.of_int 1) (prerat.of_int 1))) + (prerat.add (prerat.add (prerat.of_int 1) (prerat.of_int 1)) + (prerat.add (prerat.of_int 1) (prerat.of_int 1)))) + (prerat.inv + (prerat.add (prerat.add (prerat.add (prerat.of_int 1) (prerat.of_int 1)) (prerat.of_int 1)) + (prerat.add (prerat.add (prerat.of_int 1) (prerat.of_int 1)) (prerat.of_int 1))))) + (prerat.of_int 1))) diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean index 47bcb42a7..f5c9005d0 100644 --- a/tests/lean/run/div2.lean +++ b/tests/lean/run/div2.lean @@ -49,7 +49,7 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom → (rec_val : dom → (dom → codom) → codom) (x : dom) : codom := rec_measure_aux default measure rec_val (succ (measure x)) x -attribute decidable [multiple-instances] +attribute decidable [multiple_instances] theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ) (rec_val : dom → (dom → codom) → codom) diff --git a/tests/lean/run/notation_priority.lean b/tests/lean/run/notation_priority.lean index 9ffaa104d..ddbc34bb8 100644 --- a/tests/lean/run/notation_priority.lean +++ b/tests/lean/run/notation_priority.lean @@ -7,12 +7,6 @@ infix [priority 20] + := g variables a b : nat -example : a + b = g a b := rfl -infix [priority 5] + := g -example : a + b = f a b := rfl -infix [priority 15] + := g -example : a + b = g a b := rfl - infix [priority std.priority.default+1] + := f infix + := g example : a + b = f a b := rfl @@ -21,7 +15,6 @@ example : a + b = g a b := rfl infix + := f infix + := g -example : a + b = f a b := rfl infix [priority std.priority.default+1] + := g example : a + b = g a b := rfl diff --git a/tests/lean/run/record10.lean b/tests/lean/run/record10.lean index bc5232166..00aa05c00 100644 --- a/tests/lean/run/record10.lean +++ b/tests/lean/run/record10.lean @@ -1,8 +1,5 @@ import logic -structure has_mul [class] (A : Type) := -(mul : A → A → A) - structure semigroup [class] (A : Type) extends has_mul A := (assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)) diff --git a/tests/lean/slow/nat_bug1.lean b/tests/lean/slow/nat_bug1.lean index 6632f2754..a6d1b2dd4 100644 --- a/tests/lean/slow/nat_bug1.lean +++ b/tests/lean/slow/nat_bug1.lean @@ -17,8 +17,14 @@ namespace nat definition plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y -definition to_nat [coercion] (n : num) : ℕ -:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n +definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat := +has_zero.mk nat.zero + +definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat := +has_one.mk (nat.succ (nat.zero)) + +definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat := +has_add.mk plus print "==================" theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x := diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean deleted file mode 100644 index 70b70eabe..000000000 --- a/tests/lean/slow/nat_bug2.lean +++ /dev/null @@ -1,1413 +0,0 @@ ----------------------------------------------------------------------------------------------------- --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn ----------------------------------------------------------------------------------------------------- -import logic algebra.binary -open binary eq.ops eq -open decidable -namespace experiment -definition refl := @eq.refl -definition and_intro := @and.intro -definition or_intro_left := @or.intro_left -definition or_intro_right := @or.intro_right - -inductive nat : Type := -| zero : nat -| succ : nat → nat - -namespace nat - -notation `ℕ`:max := nat - -definition plus (x y : ℕ) : ℕ -:= nat.rec x (λ n r, succ r) y - -definition to_nat [coercion] (n : num) : ℕ -:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n - -namespace helper_tactics - definition apply_refl := tactic.apply @refl - tactic_hint apply_refl -end helper_tactics -open helper_tactics - -theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x - -theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n) - --------------------------------------------------- succ pred - -theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 -:= assume H : succ n = 0, - have H2 : true = false, from - let f := (nat.rec false (fun a b, true)) in - calc true = f (succ n) : rfl - ... = f 0 : {H} - ... = false : rfl, - absurd H2 true_ne_false - -definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n - -theorem pred_zero : pred 0 = 0 - -theorem pred_succ (n : ℕ) : pred (succ n) = n - -theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) -:= nat.induction_on n - (or.intro_left _ (refl 0)) - (take m IH, or.intro_right _ - (show succ m = succ (pred (succ m)), from congr_arg succ ((pred_succ m)⁻¹))) - -theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k -:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H) - -theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n -:= nat.induction_on n H1 (take m IH, H2 m) - -theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B -:= or.elim (zero_or_succ 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 -:= calc - n = pred (succ n) : (pred_succ n)⁻¹ - ... = pred (succ m) : {H} - ... = m : pred_succ m - -theorem succ_ne_self (n : ℕ) : succ n ≠ n -:= nat.induction_on n - (take H : 1 = 0, - have ne : 1 ≠ 0, from succ_ne_zero 0, - absurd H ne) - (take k IH H, IH (succ.inj H)) - -theorem decidable_eq [instance] (n m : nat) : decidable (n = m) -:= have general : ∀n, decidable (n = m), from - nat.rec_on m - (take n, - nat.rec_on n - (inl (refl 0)) - (λ m iH, inr (succ_ne_zero m))) - (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), - take n, nat.rec_on n - (inr (ne.symm (succ_ne_zero m'))) - (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), - have d1 : decidable (n' = m'), from iH1 n', - decidable.rec_on d1 - (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, - inr H1))), - general n - -theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) - (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a -:= have stronger : P a ∧ P (succ a), from - nat.induction_on a - (and_intro H1 H2) - (take k IH, - have IH1 : P k, from and.elim_left IH, - have IH2 : P (succ k), from and.elim_right IH, - and_intro IH2 (H3 k IH1 IH2)), - and.elim_left stronger - -theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) - (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m -:= have general : ∀m, P n m, from nat.induction_on n - (take m : ℕ, H1 m) - (take k : ℕ, - assume IH : ∀m, P k m, - take m : ℕ, - discriminate - (assume Hm : m = 0, - Hm⁻¹ ▸ (H2 k)) - (take l : ℕ, - assume Hm : m = succ l, - Hm⁻¹ ▸ (H3 k l (IH l)))), - general m - --------------------------------------------------- add -definition add (x y : ℕ) : ℕ := plus x y -infixl `+` := add -theorem add_zero (n : ℕ) : n + 0 = n -theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) ----------- comm, assoc - -theorem zero_add (n : ℕ) : 0 + n = n -:= nat.induction_on n - (add_zero 0) - (take m IH, show 0 + succ m = succ m, from - calc - 0 + succ m = succ (0 + m) : add_succ _ _ - ... = succ m : {IH}) - -theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) -:= nat.induction_on m - (calc - succ n + 0 = succ n : add_zero (succ n) - ... = succ (n + 0) : {symm (add_zero n)}) - (take k IH, - calc - succ n + succ k = succ (succ n + k) : add_succ _ _ - ... = succ (succ (n + k)) : {IH} - ... = succ (n + succ k) : {symm (add_succ _ _)}) - -theorem add_comm (n m : ℕ) : n + m = m + n -:= nat.induction_on m - (trans (add_zero _) (symm (zero_add _))) - (take k IH, - calc - n + succ k = succ (n+k) : add_succ _ _ - ... = succ (k + n) : {IH} - ... = succ k + n : symm (succ_add _ _)) - -theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m -:= calc - succ n + m = succ (n + m) : succ_add n m - ... = n +succ m : symm (add_succ n m) - -theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n -:= calc - n + succ m = succ n + m : symm (succ_add_eq_add_succ n m) - ... = m + succ n : add_comm (succ n) m - -theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k) -:= nat.induction_on k - (calc - (n + m) + 0 = n + m : add_zero _ - ... = n + (m + 0) : {symm (add_zero m)}) - (take l IH, - calc - (n + m) + succ l = succ ((n + m) + l) : add_succ _ _ - ... = succ (n + (m + l)) : {IH} - ... = n + succ (m + l) : symm (add_succ _ _) - ... = n + (m + succ l) : {symm (add_succ _ _)}) - -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 - - ----------- inversion - -theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k -:= - nat.induction_on n - (take H : 0 + m = 0 + k, - calc - m = 0 + m : symm (zero_add m) - ... = 0 + k : H - ... = k : zero_add k) - (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 : symm (succ_add n m) - ... = succ n + k : H - ... = succ (n + k) : succ_add n k, - have H3 : n + m = n + k, from succ.inj H2, - IH H3) - ---rename to and_cancel_right -theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k -:= - have H2 : m + n = m + k, - from calc - m + n = n + m : add_comm m n - ... = k + m : H - ... = m + k : add_comm k m, - add_cancel_left H2 - -theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 -:= - nat.induction_on n - (take (H : 0 + m = 0), refl 0) - (take k IH, - assume (H : succ k + m = 0), - absurd - (show succ (k + m) = 0, from - calc - succ (k + m) = succ k + m : symm (succ_add k m) - ... = 0 : H) - (succ_ne_zero (k + m))) - -theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 -:= eq_zero_of_add_eq_zero_right (trans (add_comm m n) H) - -theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 -:= and_intro (eq_zero_of_add_eq_zero_right H) (add_eq_zero_right H) - --- add_eq_self below - ----------- misc - -theorem add_one (n:ℕ) : n + 1 = succ n -:= - calc - n + 1 = succ (n + 0) : add_succ _ _ - ... = succ n : {add_zero _} - -theorem add_one_left (n:ℕ) : 1 + n = succ n -:= - calc - 1 + n = succ (0 + n) : succ_add _ _ - ... = succ n : {zero_add _} - ---the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it -theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0) - (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a -:= nat.rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a - --------------------------------------------------- mul - -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_succ_right (n m:ℕ) : n * succ m = n * m + n -set_option unifier.max_steps 100000 ----------- comm, distr, assoc, identity - -theorem mul_zero_left (n:ℕ) : 0 * n = 0 -:= nat.induction_on n - (mul_zero_right 0) - (take m IH, - calc - 0 * succ m = 0 * m + 0 : mul_succ_right _ _ - ... = 0 * m : add_zero _ - ... = 0 : IH) - -theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m -:= nat.induction_on m - (calc - succ n * 0 = 0 : mul_zero_right _ - ... = n * 0 : symm (mul_zero_right _) - ... = n * 0 + 0 : symm (add_zero _)) - (take k IH, - calc - 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 : symm (add_assoc _ _ _) - ... = (n * succ k) + succ k : {symm (mul_succ_right n k)}) - -theorem mul_comm (n m:ℕ) : n * m = m * n -:= nat.induction_on m - (trans (mul_zero_right _) (symm (mul_zero_left _))) - (take k IH, - calc - n * succ k = n * k + n : mul_succ_right _ _ - ... = k * n + n : {IH} - ... = (succ k) * n : symm (mul_succ_left _ _)) - -theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k -:= nat.induction_on k - (calc - (n + m) * 0 = 0 : mul_zero_right _ - ... = 0 + 0 : symm (add_zero _) - ... = n * 0 + 0 : refl _ - ... = n * 0 + m * 0 : refl _) - (take l IH, calc - (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 : symm (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) : {symm (mul_succ_right _ _)} - ... = n * succ l + m * succ l : {symm (mul_succ_right _ _)}) - -theorem mul_add_distr_right (n m k : ℕ) : n * (m + k) = n * m + n * k -:= calc - n * (m + k) = (m + k) * n : mul_comm _ _ - ... = m * n + k * n : mul_add_distr_left _ _ _ - ... = n * m + k * n : {mul_comm _ _} - ... = n * m + n * k : {mul_comm _ _} - -theorem mul_assoc (n m k:ℕ) : (n * m) * k = n * (m * k) -:= nat.induction_on k - (calc - (n * m) * 0 = 0 : mul_zero_right _ - ... = n * 0 : symm (mul_zero_right _) - ... = n * (m * 0) : {symm (mul_zero_right _)}) - (take l IH, - calc - (n * m) * succ l = (n * m) * l + n * m : mul_succ_right _ _ - ... = n * (m * l) + n * m : {IH} - ... = n * (m * l + m) : symm (mul_add_distr_right _ _ _) - ... = n * (m * succ l) : {symm (mul_succ_right _ _)}) - -theorem mul_comm_left (n m k : ℕ) : n * (m * k) = m * (n * k) -:= left_comm mul_comm mul_assoc n m k - -theorem mul_comm_right (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 -:= calc - n * 1 = n * 0 + n : mul_succ_right n 0 - ... = 0 + n : {mul_zero_right n} - ... = n : zero_add n - -theorem mul_one_left (n : ℕ) : 1 * n = n -:= calc - 1 * n = n * 1 : mul_comm _ _ - ... = n : mul_one_right n - ----------- inversion - -theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 -:= - discriminate - (take Hn : n = 0, or_intro_left _ Hn) - (take (k : ℕ), - assume (Hk : n = succ k), - discriminate - (take (Hm : m = 0), or_intro_right _ Hm) - (take (l : ℕ), - assume (Hl : m = succ l), - have Heq : succ (k * succ l + l) = n * m, from - symm (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 _ _), - absurd (trans Heq H) (succ_ne_zero _))) - --- see more under "positivity" below --------------------------------------------------- le - -definition le (n m:ℕ) : Prop := ∃k, n + k = m -infix `<=` := le -infix `≤` := le - -theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m -:= exists.intro k H - -theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃ k, n + k = m -:= H - ----------- partial order (totality is part of lt) - -theorem le_intro2 (n m : ℕ) : n ≤ n + m -:= le_intro (refl (n + m)) - -theorem le_refl (n : ℕ) : n ≤ n -:= le_intro (add_zero n) - -theorem zero_le (n : ℕ) : 0 ≤ n -:= le_intro (zero_add n) - -theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 -:= - obtain (k : ℕ) (Hk : n + k = 0), from le_elim H, - eq_zero_of_add_eq_zero_right Hk - -theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 -:= assume H : succ n ≤ 0, - have H2 : succ n = 0, from le_zero H, - absurd H2 (succ_ne_zero n) - -theorem le_zero_inv {n : ℕ} (H : n ≤ 0) : n = 0 -:= obtain (k : ℕ) (Hk : n + k = 0), from le_elim H, - eq_zero_of_add_eq_zero_right Hk - -theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k -:= 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 : symm (add_assoc n l1 l2) - ... = m + l2 : { Hl1 } - ... = k : Hl2) - -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 - (calc - n + (k + l) = n + k + l : { symm (add_assoc n k l) } - ... = m + l : { Hk } - ... = n : Hl - ... = n + 0 : symm (add_zero n)), - have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1, - calc - n = n + 0 : symm (add_zero n) - ... = n + k : { symm L2 } - ... = m : Hk - ----------- interaction with add - -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 + m : { Hl }) - -theorem add_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k -:= (add_comm k m) ▸ (add_comm k n) ▸ (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) - -theorem add_le_left_inv {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 - (calc - k + (n + l) = k + n + l : symm (add_assoc k n l) - ... = k + m : Hl)) - -theorem add_le_right_inv {n m k : ℕ} (H : n + k ≤ m + k) : n ≤ m -:= add_le_left_inv (add_comm m k ▸ add_comm n k ▸ H) - ----------- interaction with succ and pred - -theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m -:= add_one m ▸ add_one n ▸ add_le_right H 1 - -theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m -:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) - -theorem self_le_succ (n : ℕ) : n ≤ succ n -:= le_intro (add_one n) - -theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m -:= le_trans H (self_le_succ m) - -theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m -:= obtain (k : ℕ) (Hk : n + k = m), from (le_elim H), - discriminate - (assume H3 : k = 0, - have Heq : n = m, - from calc - n = n + 0 : (add_zero n)⁻¹ - ... = n + k : {H3⁻¹} - ... = m : Hk, - or_intro_right _ Heq) - (take l:ℕ, - assume H3 : k = succ l, - have Hlt : succ n ≤ m, from - (le_intro - (calc - succ n + l = n + succ l : succ_add_eq_add_succ n l - ... = n + k : {H3⁻¹} - ... = m : Hk)), - or_intro_left _ Hlt) - -theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= or_resolve_left (succ_le_left_or H1) H2 - -theorem succ_le_right_inv {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= or_of_or_of_imp_of_imp (succ_le_left_or H) - (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) - (take H2 : n = succ m, H2) - -theorem succ_le_left_inv {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m -:= 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 : symm (succ_add_eq_add_succ n k) - ... = m : H2, - show n ≤ m, from le_intro H3) - (assume H3 : n = m, - have H4 : succ n ≤ n, from subst (symm H3) H, - have H5 : succ n = n, from le_antisym H4 (self_le_succ n), - show false, from absurd H5 (succ_ne_self n)) - -theorem le_pred_self (n : ℕ) : pred n ≤ n -:= case n - (subst (symm pred_zero) (le_refl 0)) - (take k : ℕ, subst (symm (pred_succ k)) (self_le_succ k)) - -theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m -:= discriminate - (take Hn : n = 0, - have H2 : pred n = 0, - from calc - pred n = pred 0 : {Hn} - ... = 0 : pred_zero, - subst (symm H2) (zero_le (pred m))) - (take k : ℕ, - assume Hn : n = succ k, - obtain (l : ℕ) (Hl : n + l = m), from le_elim H, - have H2 : pred n + l = pred m, - from calc - pred n + l = pred (succ k) + l : {Hn} - ... = k + l : {pred_succ k} - ... = pred (succ (k + l)) : symm (pred_succ (k + l)) - ... = pred (succ k + l) : {symm (succ_add k l)} - ... = pred (n + l) : {symm Hn} - ... = pred m : {Hl}, - le_intro H2) - -theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m -:= discriminate - (take Hn : n = 0, - or_intro_left _ (subst (symm Hn) (zero_le m))) - (take k : ℕ, - assume Hn : n = succ k, - have H2 : pred n = k, - from calc - pred n = pred (succ k) : {Hn} - ... = k : pred_succ k, - have H3 : k ≤ m, from subst H2 H, - have H4 : succ k ≤ m ∨ k = m, from succ_le_left_or H3, - show n ≤ m ∨ n = succ m, from - or_of_or_of_imp_of_imp H4 - (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) - (take H5 : k = m, show n = succ m, from subst H5 Hn)) - --- ### interaction with successor and predecessor - -theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m -:= - obtain (k : ℕ) (Hk : n + k = m), from (le_elim H), - discriminate - (assume H3 : k = 0, - have Heq : n = m, - from calc - n = n + 0 : symm (add_zero n) - ... = n + k : {symm H3} - ... = m : Hk, - or_intro_right _ Heq) - (take l : nat, - assume H3 : k = succ l, - have Hlt : succ n ≤ m, from - (le_intro - (calc - succ n + l = n + succ l : succ_add_eq_add_succ n l - ... = n + k : {symm H3} - ... = m : Hk)), - or_intro_left _ Hlt) - -theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= or_resolve_left (le_imp_succ_le_or_eq H1) H2 - -theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m -:= - and_intro - (le_trans (self_le_succ n) H) - (assume H2 : n = m, - have H3 : succ n ≤ n, from subst (symm H2) H, - have H4 : succ n = n, from le_antisym H3 (self_le_succ n), - show false, from absurd H4 (succ_ne_self n)) - -theorem pred_le_self (n : ℕ) : pred n ≤ n -:= - case n - (subst (symm pred_zero) (le_refl 0)) - (take k : nat, subst (symm (pred_succ k)) (self_le_succ k)) - -theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m -:= - discriminate - (take Hn : n = 0, - or_intro_left _ (subst (symm Hn) (zero_le m))) - (take k : nat, - assume Hn : n = succ k, - have H2 : pred n = k, - from calc - pred n = pred (succ k) : {Hn} - ... = k : pred_succ k, - have H3 : k ≤ m, from subst H2 H, - have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, - show n ≤ m ∨ n = succ m, from - or_of_or_of_imp_of_imp H4 - (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) - (take H5 : k = m, show n = succ m, from subst H5 Hn)) - ----------- interaction with mul - -theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m -:= - obtain (l : ℕ) (Hl : n + l = m), from (le_elim H), - nat.induction_on k - (have H2 : 0 * n = 0 * m, - from calc - 0 * n = 0 : mul_zero_left n - ... = 0 * m : symm (mul_zero_left m), - show 0 * n ≤ 0 * m, from subst H2 (le_refl (0 * n))) - (take (l : ℕ), - assume IH : l * n ≤ l * m, - have H2 : l * n + n ≤ l * m + m, from add_le IH H, - have H3 : succ l * n ≤ l * m + m, from subst (symm (mul_succ_left l n)) H2, - show succ l * n ≤ succ l * m, from subst (symm (mul_succ_left l m)) H3) - -theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k -:= mul_comm k m ▸ mul_comm k n ▸ (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) - --- mul_le_[left|right]_inv below - --------------------------------------------------- lt - -definition lt (n m : ℕ) := succ n ≤ m -infix `<` := lt - -theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m -:= le_intro H - -theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m -:= le_elim H - -theorem lt_intro2 (n m : ℕ) : n < n + succ m -:= lt_intro (succ_add_eq_add_succ n m) - --------------------------------------------------- ge, gt - -definition ge (n m : ℕ) := m ≤ n -infix `>=` := ge -infix `≥` := ge - -definition gt (n m : ℕ) := m < n -infix `>` := gt - ----------- basic facts - -theorem lt_ne {n m : ℕ} (H : n < m) : n ≠ m -:= and.elim_right (succ_le_left_inv H) - -theorem lt_irrefl (n : ℕ) : ¬ n < n -:= assume H : n < n, absurd (refl n) (lt_ne H) - -theorem lt_zero (n : ℕ) : 0 < succ n -:= succ_le (zero_le n) - -theorem lt_zero_inv (n : ℕ) : ¬ n < 0 -:= assume H : n < 0, - have H2 : succ n = 0, from le_zero_inv H, - absurd H2 (succ_ne_zero n) - -theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k -:= discriminate - (take (Hm : m = 0), absurd (subst Hm H) (lt_zero_inv n)) - (take (l : ℕ) (Hm : m = succ l), exists.intro l Hm) - ----------- interaction with le - -theorem lt_imp_le_succ {n m : ℕ} (H : n < m) : succ n ≤ m -:= H - -theorem le_succ_imp_lt {n m : ℕ} (H : succ n ≤ m) : n < m -:= H - -theorem self_lt_succ (n : ℕ) : n < succ n -:= le_refl (succ n) - -theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m -:= and.elim_left (succ_le_imp_le_and_ne H) - -theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m -:= le_imp_succ_le_or_eq H - -theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m -:= le_ne_imp_succ_le H1 H2 - -theorem le_imp_lt_succ {n m : ℕ} (H : n ≤ m) : n < succ m -:= succ_le H - -theorem lt_succ_imp_le {n m : ℕ} (H : n < succ m) : n ≤ m -:= succ_le_cancel H - ----------- trans, antisym - -theorem lt_le_trans {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k -:= le_trans H1 H2 - -theorem le_lt_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k -:= le_trans (succ_le H1) H2 - -theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k -:= lt_le_trans H1 (lt_imp_le H2) - -theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m -:= assume H2 : m < n, absurd (le_lt_trans H H2) (lt_irrefl n) - -theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m -:= assume H2 : m ≤ n, absurd (lt_le_trans H H2) (lt_irrefl n) - -theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n -:= le_imp_not_gt (lt_imp_le H) - ----------- interaction with add - -theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m -:= add_succ k n ▸ add_le_left H k - -theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k -:= add_comm k m ▸ add_comm k n ▸ 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) - -theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l -:= lt_le_trans (add_lt_right H1 m) (add_le_left H2 k) - -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_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m -:= add_le_left_inv ((add_succ k n)⁻¹ ▸ H) - -theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m -:= add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H) - ----------- interaction with succ (see also the interaction with le) - -theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m -:= add_one m ▸ add_one n ▸ add_lt_right H 1 - -theorem succ_lt_inv {n m : ℕ} (H : succ n < succ m) : n < m -:= add_lt_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) - -theorem lt_self_succ (n : ℕ) : n < succ n -:= le_refl (succ n) - -theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m -:= lt_trans H (lt_self_succ m) - ----------- totality of lt and le - -theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n -:= nat.induction_on n - (or_intro_left _ (zero_le m)) - (take (k : ℕ), - assume IH : k ≤ m ∨ m < k, - or.elim IH - (assume H : k ≤ m, - obtain (l : ℕ) (Hl : k + l = m), from le_elim H, - discriminate - (assume H2 : l = 0, - have H3 : m = k, - from calc - m = k + l : symm Hl - ... = k + 0 : {H2} - ... = k : add_zero k, - have H4 : m < succ k, from subst H3 (lt_self_succ m), - or_intro_right _ H4) - (take l2 : ℕ, - assume H2 : l = succ l2, - have H3 : succ k + l2 = m, - from calc - succ k + l2 = k + succ l2 : succ_add_eq_add_succ k l2 - ... = k + l : {symm H2} - ... = m : Hl, - or_intro_left _ (le_intro H3))) - (assume H : m < k, or_intro_right _ (succ_lt_right H))) - -theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n -:= or_of_or_of_imp_of_imp (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) - -theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ m < n -:= iff.elim_left or.assoc (trichotomy_alt n m) - -theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n -:= or_of_or_of_imp_of_imp (le_or_lt n m) (assume H : n ≤ m, H) (assume H : m < n, lt_imp_le H) - --- interaction with mul under "positivity" - -theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m < n → P m) → P n) : P n -:= have stronger : ∀k, k ≤ n → P k, from - nat.induction_on n - (take (k : ℕ), - assume H : k ≤ 0, - have H2 : k = 0, from le_zero_inv H, - have H3 : ∀m, m < k → P m, from - (take m : ℕ, - assume H4 : m < k, - have H5 : m < 0, from subst H2 H4, - absurd H5 (lt_zero_inv m)), - show P k, from IH k H3) - (take l : ℕ, - assume IHl : ∀k, k ≤ l → P k, - take k : ℕ, - assume H : k ≤ succ l, - or.elim (succ_le_right_inv H) - (assume H2 : k ≤ l, show P k, from IHl k H2) - (assume H2 : k = succ l, - have H3 : ∀m, m < k → P m, from - (take m : ℕ, - assume H4 : m < k, - have H5 : m ≤ l, from lt_succ_imp_le (subst H2 H4), - show P m, from IHl m H5), - show P k, from IH k H3)), - stronger n (le_refl n) - -theorem case_strong_induction_on {P : ℕ → Prop} (a : ℕ) (H0 : P 0) (Hind : ∀(n : ℕ), (∀m, m ≤ n → P m) → P (succ n)) : P a -:= strong_induction_on a - (take n, case n - (assume H : (∀m, m < 0 → P m), H0) - (take n, assume H : (∀m, m < succ n → P m), - Hind n (take m, assume H1 : m ≤ n, H m (le_imp_lt_succ H1)))) - -theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0 -:= discriminate - (take Hm : m = 0, Hm) - (take k : ℕ, - assume Hm : m = succ k, - have H2 : succ n + k = n, - from calc - succ n + k = n + succ k : succ_add_eq_add_succ n k - ... = n + m : {symm Hm} - ... = n : H, - have H3 : n < n, from lt_intro H2, - have H4 : n ≠ n, from lt_ne H3, - absurd (refl n) H4) - --------------------------------------------------- positivity - --- we use " _ > 0" as canonical way of denoting that a number is positive - ----------- basic - -theorem zero_or_positive (n : ℕ) : n = 0 ∨ n > 0 -:= or_of_or_of_imp_of_imp (or.swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) (take H : n > 0, H) - -theorem succ_positive {n m : ℕ} (H : n = succ m) : n > 0 -:= subst (symm H) (lt_zero m) - -theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0 -:= or.elim (zero_or_positive n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) - -theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l -:= discriminate - (take H2, absurd (subst H2 H) (lt_irrefl 0)) - (take l Hl, exists.intro l Hl) - -theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n -:= obtain (l : ℕ) (Hl : k = succ l), from pos_imp_eq_succ H, - subst (symm Hl) (lt_intro2 n l) - -theorem add_positive_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n -:= subst (add_comm n k) (add_positive_right n H) - - --- Positivity --- --------- --- --- Writing "t > 0" is the preferred way to assert that a natural number is positive. - --- ### basic - --- See also succ_pos. - -theorem succ_pos (n : ℕ) : 0 < succ n -:= succ_le (zero_le n) - -theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y -:= case y H0 (take y', H1 _ (succ_pos _)) - -theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 -:= subst (symm H) (succ_pos m) - -theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n -:= subst (add_zero n) (add_lt_left H n) - -theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n -:= subst (add_comm n k) (add_pos_right n H) - ----------- mul - -theorem mul_positive {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0 -:= obtain (k : ℕ) (Hk : n = succ k), from pos_imp_eq_succ Hn, - obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm, - succ_positive (calc - n * m = succ k * m : {Hk} - ... = succ k * succ l : {Hl} - ... = succ k * l + succ k : mul_succ_right (succ k) l - ... = succ (succ k * l + k) : add_succ _ _) - -theorem mul_positive_inv_left {n m : ℕ} (H : n * m > 0) : n > 0 -:= discriminate - (assume H2 : n = 0, - have H3 : n * m = 0, - from calc - n * m = 0 * m : {H2} - ... = 0 : mul_zero_left m, - have H4 : 0 > 0, from subst H3 H, - absurd H4 (lt_irrefl 0)) - (take l : ℕ, - assume Hl : n = succ l, - subst (symm Hl) (lt_zero l)) - -theorem mul_positive_inv_right {n m : ℕ} (H : n * m > 0) : m > 0 -:= mul_positive_inv_left (subst (mul_comm n m) H) - -theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k -:= - have general : ∀m, n * m = n * k → m = k, from - nat.induction_on k - (take m:ℕ, - assume H : n * m = n * 0, - have H2 : n * m = 0, - from calc - n * m = n * 0 : H - ... = 0 : mul_zero_right n, - have H3 : n = 0 ∨ m = 0, from mul_eq_zero H2, - or_resolve_right H3 (ne.symm (lt_ne Hn))) - (take (l : ℕ), - assume (IH : ∀ m, n * m = n * l → m = l), - take (m : ℕ), - assume (H : n * m = n * succ l), - have H2 : n * succ l > 0, from mul_positive Hn (lt_zero l), - have H3 : m > 0, from mul_positive_inv_right (subst (symm H) H2), - obtain (l2:ℕ) (Hm : m = succ l2), from pos_imp_eq_succ H3, - have H4 : n * l2 + n = n * l + n, - from calc - n * l2 + n = n * succ l2 : symm (mul_succ_right n l2) - ... = n * m : {symm Hm} - ... = n * succ l : H - ... = n * l + n : mul_succ_right n l, - have H5 : n * l2 = n * l, from add_cancel_right H4, - calc - m = succ l2 : Hm - ... = succ l : {IH l2 H5}), - general m H - -theorem mul_right_inj {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k -:= mul_left_inj Hm (subst (mul_comm k m) (subst (mul_comm n m) H)) - --- mul_eq_one below - ----------- 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_positive_right (k * n) Hk, - have H3 : k * n + k ≤ k * m, from subst (mul_succ_right k n) (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 -:= subst (mul_comm k m) (subst (mul_comm k n) (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) - -theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l -:= le_lt_trans (mul_le_left H2 n) (mul_lt_right Hl H1) - -theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l -:= - have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m, - have H4 : k * m < k * l, from mul_lt_left (le_lt_trans (zero_le n) H1) H2, - le_lt_trans H3 H4 - -theorem mul_lt_left_inv {n m k : ℕ} (H : k * n < k * m) : n < m -:= - have general : ∀ m, k * n < k * m → n < m, from - nat.induction_on n - (take m : ℕ, - assume H2 : k * 0 < k * m, - have H3 : 0 < k * m, from mul_zero_right k ▸ H2, - show 0 < m, from mul_positive_inv_right H3) - (take l : ℕ, - assume IH : ∀ m, k * l < k * m → l < m, - take m : ℕ, - assume H2 : k * succ l < k * m, - have H3 : 0 < k * m, from le_lt_trans (zero_le _) H2, - have H4 : 0 < m, from mul_positive_inv_right H3, - obtain (l2 : ℕ) (Hl2 : m = succ l2), from pos_imp_eq_succ H4, - have H5 : k * l + k < k * m, from mul_succ_right k l ▸ H2, - have H6 : k * l + k < k * succ l2, from Hl2 ▸ H5, - have H7 : k * l + k < k * l2 + k, from mul_succ_right k l2 ▸ H6, - have H8 : k * l < k * l2, from add_lt_right_inv H7, - have H9 : l < l2, from IH l2 H8, - have H10 : succ l < succ l2, from succ_lt H9, - show succ l < m, from Hl2⁻¹ ▸ H10), - general m H - -theorem mul_lt_right_inv {n m k : ℕ} (H : n * k < m * k) : n < m -:= mul_lt_left_inv (mul_comm m k ▸ mul_comm n k ▸ H) - -theorem mul_le_left_inv {n m k : ℕ} (H : succ k * n ≤ succ k * m) : n ≤ m -:= - have H2 : succ k * n < succ k * m + succ k, from le_lt_trans H (lt_intro2 _ _), - have H3 : succ k * n < succ k * succ m, from subst (symm (mul_succ_right (succ k) m)) H2, - have H4 : n < succ m, from mul_lt_left_inv H3, - show n ≤ m, from lt_succ_imp_le H4 - -theorem mul_le_right_inv {n m k : ℕ} (H : n * succ m ≤ k * succ m) : n ≤ k -:= mul_le_left_inv (subst (mul_comm k (succ m)) (subst (mul_comm n (succ m)) H)) - -theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 -:= - have H2 : n * m > 0, from subst (symm H) (lt_zero 0), - have H3 : n > 0, from mul_positive_inv_left H2, - have H4 : m > 0, from mul_positive_inv_right H2, - or.elim (le_or_lt n 1) - (assume H5 : n ≤ 1, - 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 subst (mul_one_right 2) (subst H H6), - absurd (self_lt_succ 1) (le_imp_not_gt H7)) - -theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 -:= mul_eq_one_left (subst (mul_comm n m) H) - -theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1 -:= and_intro (mul_eq_one_left H) (mul_eq_one_right H) - --------------------------------------------------- sub - -definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m -infixl `-` := sub -theorem sub_zero_right (n : ℕ) : n - 0 = n -theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) - -theorem sub_zero_left (n : ℕ) : 0 - n = 0 -:= nat.induction_on n (sub_zero_right 0) - (take k : ℕ, - assume IH : 0 - k = 0, - calc - 0 - succ k = pred (0 - k) : sub_succ_right 0 k - ... = pred 0 : {IH} - ... = 0 : pred_zero) - -theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m -:= nat.induction_on m - (calc - succ n - 1 = pred (succ n - 0) : sub_succ_right (succ n) 0 - ... = pred (succ n) : {sub_zero_right (succ n)} - ... = n : pred_succ n - ... = n - 0 : symm (sub_zero_right n)) - (take k : ℕ, - assume IH : succ n - succ k = n - k, - calc - succ n - succ (succ k) = pred (succ n - succ k) : sub_succ_right (succ n) (succ k) - ... = pred (n - k) : {IH} - ... = n - succ k : symm (sub_succ_right n k)) - -theorem sub_one (n : ℕ) : n - 1 = pred n -:= calc - n - 1 = pred (n - 0) : sub_succ_right n 0 - ... = pred n : {sub_zero_right n} - -theorem sub_self (n : ℕ) : n - n = 0 -:= nat.induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH) - -theorem sub_add_add_right (n m k : ℕ) : (n + k) - (m + k) = n - m -:= nat.induction_on k - (calc - (n + 0) - (m + 0) = n - (m + 0) : {add_zero _} - ... = n - m : {add_zero _}) - (take l : ℕ, - assume IH : (n + l) - (m + l) = n - m, - calc - (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ _ _} - ... = succ (n + l) - succ (m + l) : {add_succ _ _} - ... = (n + l) - (m + l) : sub_succ_succ _ _ - ... = n - m : IH) - -theorem sub_add_add_left (n m k : ℕ) : (k + n) - (k + m) = n - m -:= subst (add_comm m k) (subst (add_comm n k) (sub_add_add_right n m k)) - -theorem sub_add_left (n m : ℕ) : n + m - m = n -:= nat.induction_on m - (subst (symm (add_zero n)) (sub_zero_right n)) - (take k : ℕ, - assume IH : n + k - k = n, - calc - n + succ k - succ k = succ (n + k) - succ k : {add_succ n k} - ... = n + k - k : sub_succ_succ _ _ - ... = n : IH) - -theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) -:= nat.induction_on k - (calc - n - m - 0 = n - m : sub_zero_right _ - ... = n - (m + 0) : {symm (add_zero m)}) - (take l : ℕ, - assume IH : n - m - l = n - (m + l), - calc - n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l - ... = pred (n - (m + l)) : {IH} - ... = n - succ (m + l) : symm (sub_succ_right n (m + l)) - ... = n - (m + succ l) : {symm (add_succ m l)}) - -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 m k} - ... = n - (m + k) : sub_succ_succ _ _ - ... = n - m - k : symm (sub_sub n m k) - -theorem sub_add_right_eq_zero (n m : ℕ) : n - (n + m) = 0 -:= calc - n - (n + m) = n - n - m : symm (sub_sub n n m) - ... = 0 - m : {sub_self n} - ... = 0 : sub_zero_left m - -theorem sub_comm (m n k : ℕ) : m - n - k = m - k - n -:= calc - m - n - k = m - (n + k) : sub_sub m n k - ... = m - (k + n) : {add_comm n k} - ... = m - k - n : symm (sub_sub m k n) - -theorem succ_sub_one (n : ℕ) : succ n - 1 = n -:= sub_succ_succ n 0 ⬝ sub_zero_right n - ----------- mul - -theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m -:= nat.induction_on n - (calc - pred 0 * m = 0 * m : {pred_zero} - ... = 0 : mul_zero_left _ - ... = 0 - m : symm (sub_zero_left m) - ... = 0 * m - m : {symm (mul_zero_left m)}) - (take k : ℕ, - assume IH : pred k * m = k * m - m, - calc - pred (succ k) * m = k * m : {pred_succ k} - ... = k * m + m - m : symm (sub_add_left _ _) - ... = succ k * m - m : {symm (mul_succ_left k m)}) - -theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n -:= calc n * pred m = pred m * n : mul_comm _ _ - ... = m * n - n : mul_pred_left m n - ... = n * m - n : {mul_comm m n} - -theorem mul_sub_distr_left (n m k : ℕ) : (n - m) * k = n * k - m * k -:= nat.induction_on m - (calc - (n - 0) * k = n * k : {sub_zero_right n} - ... = n * k - 0 : symm (sub_zero_right _) - ... = n * k - 0 * k : {symm (mul_zero_left _)}) - (take l : ℕ, - assume IH : (n - l) * k = n * k - l * k, - calc - (n - succ l) * k = pred (n - l) * k : {sub_succ_right n l} - ... = (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) : {symm (mul_succ_left l k)}) - -theorem mul_sub_distr_right (n m k : ℕ) : n * (m - k) = n * m - n * k -:= calc - n * (m - k) = (m - k) * n : mul_comm _ _ - ... = m * n - k * n : mul_sub_distr_left _ _ _ - ... = n * m - k * n : {mul_comm _ _} - ... = n * m - n * k : {mul_comm _ _} - --------------------------------------------------- max, min, iteration, maybe: sub, div - -theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) -:= sub_induction n m - (take k, - assume H : 0 ≤ k, - calc - succ k - 0 = succ k : sub_zero_right (succ k) - ... = succ (k - 0) : {symm (sub_zero_right k)}) - (take k, - assume H : succ k ≤ 0, - absurd H (not_succ_zero_le k)) - (take k l, - assume IH : k ≤ l → succ l - k = succ (l - k), - take H : succ k ≤ succ l, - calc - succ (succ l) - succ k = succ l - k : sub_succ_succ (succ l) k - ... = succ (l - k) : IH (succ_le_cancel H) - ... = succ (succ l - succ k) : {symm (sub_succ_succ l k)}) - -theorem le_imp_sub_eq_zero {n m : ℕ} (H : n ≤ m) : n - m = 0 -:= obtain (k : ℕ) (Hk : n + k = m), from le_elim H, subst Hk (sub_add_right_eq_zero n k) - -theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m -:= sub_induction n m - (take k, - assume H : 0 ≤ k, - calc - 0 + (k - 0) = k - 0 : zero_add (k - 0) - ... = k : sub_zero_right k) - (take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k)) - (take k l, - assume IH : k ≤ l → k + (l - k) = l, - take H : succ k ≤ succ l, - calc - succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ l k} - ... = succ (k + (l - k)) : succ_add k (l - k) - ... = succ l : {IH (succ_le_cancel H)}) - -theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n -:= subst (add_comm m (n - m)) 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 n - -theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m -:= subst (add_comm m (n - m)) add_sub_ge - -theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) -:= or.elim (le_total n m) - (assume H : n ≤ m, subst (symm (add_sub_le H)) H) - (assume H : m ≤ n, subst (symm (add_sub_ge H)) (le_refl n)) - -theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n) -:= or.elim (le_total n m) - (assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m)) - (assume H : m ≤ n, subst (symm (add_sub_ge H)) H) - -theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k) - : P (n - m) -:= or.elim (le_total n m) - (assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3)) - (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3)) - -theorem sub_le_self (n m : ℕ) : n - m ≤ n -:= - sub_split - (assume H : n ≤ m, zero_le n) - (take k : ℕ, assume H : m + k = n, le_intro (subst (add_comm m k) H)) - -theorem le_elim_sub (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 : {symm Hk} - ... = n : sub_add_left n k) - -theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) -:= have l1 : k ≤ m → n + m - k = n + (m - k), from - sub_induction k m - (take m : ℕ, - assume H : 0 ≤ m, - calc - n + m - 0 = n + m : sub_zero_right (n + m) - ... = n + (m - 0) : {symm (sub_zero_right m)}) - (take k : ℕ, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k)) - (take k m, - 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 n m} - ... = n + m - k : sub_succ_succ (n + m) k - ... = n + (m - k) : IH (succ_le_cancel H) - ... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}), - l1 H - -theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m -:= sub_split - (assume H1 : n ≤ m, assume H2 : 0 = 0, H1) - (take k : ℕ, - assume H1 : m + k = n, - assume H2 : k = 0, - have H3 : n = m, from subst (add_zero m) (subst H2 (symm H1)), - subst H3 (le_refl n)) - -theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) - (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) -:= or.elim (le_total n m) - (assume H3 : n ≤ m, - (le_imp_sub_eq_zero H3)⁻¹ ▸ (H2 (m - n) ((add_sub_le H3)⁻¹))) - (assume H3 : m ≤ n, - (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 (n - m) ((add_sub_le H3)⁻¹))) - -theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m -:= have H2 : k - n + n = m + n, from - calc - k - n + n = k : add_sub_ge_left (le_intro H) - ... = n + m : symm H - ... = m + n : add_comm n m, - 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, - obtain (y' : ℕ) (yeq : y = succ y'), from pos_imp_eq_succ ypos, - have xsuby_eq : x - y = x' - y', from - calc - x - y = succ x' - y : {xeq} - ... = succ x' - succ y' : {yeq} - ... = x' - y' : sub_succ_succ _ _, - have H1 : x' - y' ≤ x', from sub_le_self _ _, - have H2 : x' < succ x', from self_lt_succ _, - show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt_trans H1 H2 - --- Max, min, iteration, and absolute difference --- -------------------------------------------- - -definition max (n m : ℕ) : ℕ := n + (m - n) -definition min (n m : ℕ) : ℕ := m - (m - n) - -theorem max_le {n m : ℕ} (H : n ≤ m) : n + (m - n) = m := add_sub_le H - -theorem max_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n := add_sub_ge H - -theorem left_le_max (n m : ℕ) : n ≤ n + (m - n) := le_add_sub_left n m - -theorem right_le_max (n m : ℕ) : m ≤ max n m := le_add_sub_right n m - --- ### absolute difference - --- This section is still incomplete - -definition dist (n m : ℕ) := (n - m) + (m - n) - -theorem dist_comm (n m : ℕ) : dist n m = dist m n -:= add_comm (n - m) (m - n) - -theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m -:= - have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H, - have H3 : n ≤ m, from sub_eq_zero_imp_le H2, - 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 = (n - m) + (m - n) : refl _ - ... = 0 + (m - n) : {le_imp_sub_eq_zero H} - ... = m - n : zero_add (m - n) - -theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m -:= subst (dist_comm m n) (dist_le H) - -theorem dist_zero_right (n : ℕ) : dist n 0 = n -:= trans (dist_ge (zero_le n)) (sub_zero_right n) - -theorem dist_zero_left (n : ℕ) : dist 0 n = n -:= trans (dist_le (zero_le n)) (sub_zero_right n) - -theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m -:= calc - dist k n = k - n : dist_ge (le_intro H) - ... = m : sub_intro H - -theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m -:= - calc - dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : refl _ - ... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right _ _ _} - ... = (n - m) + (m - n) : {sub_add_add_right _ _ _} - -theorem dist_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m -:= subst (add_comm m k) (subst (add_comm n k) (dist_add_right n k m)) - -theorem dist_ge_add_right {n m : ℕ} (H : n ≥ m) : dist n m + m = n -:= calc - dist n m + m = n - m + m : {dist_ge H} - ... = n : add_sub_ge_left H - -theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m -:= calc - dist n k = dist (n + m) (k + m) : symm (dist_add_right n m k) - ... = dist (k + l) (k + m) : {H} - ... = dist l m : dist_add_left k l m - -end nat -end experiment diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean deleted file mode 100644 index 9f21880d7..000000000 --- a/tests/lean/slow/nat_wo_hints.lean +++ /dev/null @@ -1,1419 +0,0 @@ ----------------------------------------------------------------------------------------------------- --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn ----------------------------------------------------------------------------------------------------- -import logic algebra.binary -open binary eq.ops eq -open decidable - -namespace experiment -inductive nat : Type := -| zero : nat -| succ : nat → nat - - -namespace nat -notation `ℕ`:max := nat - -definition plus (x y : ℕ) : ℕ -:= nat.rec x (λ n r, succ r) y - -definition to_nat [coercion] (n : num) : ℕ -:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n - -namespace helper_tactics - definition apply_refl := tactic.apply @eq.refl - tactic_hint apply_refl -end helper_tactics -open helper_tactics - -theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x - -theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n) - -theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 -:= assume H : succ n = 0, - have H2 : true = false, from - let f := (nat.rec false (fun a b, true)) in - calc true = f (succ n) : rfl - ... = f 0 : {H} - ... = false : rfl, - absurd H2 true_ne_false - -definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n - -theorem pred_zero : pred 0 = 0 - -theorem pred_succ (n : ℕ) : pred (succ n) = n - -theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) -:= nat.induction_on n - (or.intro_left _ (eq.refl 0)) - (take m IH, or.intro_right _ - (show succ m = succ (pred (succ m)), from congr_arg succ ((pred_succ m)⁻¹))) - -theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k -:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H) - -theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n -:= nat.induction_on n H1 (take m IH, H2 m) - -theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B -:= or.elim (zero_or_succ 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 -:= calc - n = pred (succ n) : (pred_succ n)⁻¹ - ... = pred (succ m) : {H} - ... = m : pred_succ m - -theorem succ_ne_self (n : ℕ) : succ n ≠ n -:= nat.induction_on n - (take H : 1 = 0, - have ne : 1 ≠ 0, from succ_ne_zero 0, - absurd H ne) - (take k IH H, IH (succ.inj H)) - -theorem decidable_eq [instance] (n m : nat) : decidable (n = m) -:= have general : ∀n, decidable (n = m), from - nat.rec_on m - (take n, - nat.rec_on n - (inl (eq.refl 0)) - (λ m iH, inr (succ_ne_zero m))) - (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), - take n, nat.rec_on n - (inr (ne.symm (succ_ne_zero m'))) - (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), - have d1 : decidable (n' = m'), from iH1 n', - decidable.rec_on d1 - (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, - inr H1))), - general n - -theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) - (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a -:= have stronger : P a ∧ P (succ a), from - nat.induction_on a - (and.intro H1 H2) - (take k IH, - have IH1 : P k, from and.elim_left IH, - have IH2 : P (succ k), from and.elim_right IH, - and.intro IH2 (H3 k IH1 IH2)), - and.elim_left stronger - -theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) - (H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m -:= have general : ∀m, P n m, from nat.induction_on n - (take m : ℕ, H1 m) - (take k : ℕ, - assume IH : ∀m, P k m, - take m : ℕ, - discriminate - (assume Hm : m = 0, - Hm⁻¹ ▸ (H2 k)) - (take l : ℕ, - assume Hm : m = succ l, - Hm⁻¹ ▸ (H3 k l (IH l)))), - general m - --------------------------------------------------- add -definition add (x y : ℕ) : ℕ := plus x y -infixl `+` := add -theorem add_zero (n : ℕ) : n + 0 = n -theorem add_succ (n m : ℕ) : n + succ m = succ (n + m) ----------- comm, assoc - -theorem zero_add (n : ℕ) : 0 + n = n -:= nat.induction_on n - (add_zero 0) - (take m IH, show 0 + succ m = succ m, from - calc - 0 + succ m = succ (0 + m) : add_succ _ _ - ... = succ m : {IH}) - -theorem succ_add (n m : ℕ) : (succ n) + m = succ (n + m) -:= nat.induction_on m - (calc - succ n + 0 = succ n : add_zero (succ n) - ... = succ (n + 0) : {symm (add_zero n)}) - (take k IH, - calc - succ n + succ k = succ (succ n + k) : add_succ _ _ - ... = succ (succ (n + k)) : {IH} - ... = succ (n + succ k) : {symm (add_succ _ _)}) - -theorem add_comm (n m : ℕ) : n + m = m + n -:= nat.induction_on m - (trans (add_zero _) (symm (zero_add _))) - (take k IH, - calc - n + succ k = succ (n+k) : add_succ _ _ - ... = succ (k + n) : {IH} - ... = succ k + n : symm (succ_add _ _)) - -theorem succ_add_eq_add_succ (n m : ℕ) : succ n + m = n + succ m -:= calc - succ n + m = succ (n + m) : succ_add n m - ... = n +succ m : symm (add_succ n m) - -theorem add_comm_succ (n m : ℕ) : n + succ m = m + succ n -:= calc - n + succ m = succ n + m : symm (succ_add_eq_add_succ n m) - ... = m + succ n : add_comm (succ n) m - -theorem add_assoc (n m k : ℕ) : (n + m) + k = n + (m + k) -:= nat.induction_on k - (calc - (n + m) + 0 = n + m : add_zero _ - ... = n + (m + 0) : {symm (add_zero m)}) - (take l IH, - calc - (n + m) + succ l = succ ((n + m) + l) : add_succ _ _ - ... = succ (n + (m + l)) : {IH} - ... = n + succ (m + l) : symm (add_succ _ _) - ... = n + (m + succ l) : {symm (add_succ _ _)}) - -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 - - ----------- inversion - -theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k -:= - nat.induction_on n - (take H : 0 + m = 0 + k, - calc - m = 0 + m : symm (zero_add m) - ... = 0 + k : H - ... = k : zero_add k) - (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 : symm (succ_add n m) - ... = succ n + k : H - ... = succ (n + k) : succ_add n k, - have H3 : n + m = n + k, from succ.inj H2, - IH H3) - ---rename to and_cancel_right -theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k -:= - have H2 : m + n = m + k, - from calc - m + n = n + m : add_comm m n - ... = k + m : H - ... = m + k : add_comm k m, - add_cancel_left H2 - -theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 -:= - nat.induction_on n - (take (H : 0 + m = 0), eq.refl 0) - (take k IH, - assume (H : succ k + m = 0), - absurd - (show succ (k + m) = 0, from - calc - succ (k + m) = succ k + m : symm (succ_add k m) - ... = 0 : H) - (succ_ne_zero (k + m))) - -theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 -:= eq_zero_of_add_eq_zero_right (trans (add_comm m n) H) - -theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 -:= and.intro (eq_zero_of_add_eq_zero_right H) (add_eq_zero_right H) - --- add_eq_self below - ----------- misc - -theorem add_one (n:ℕ) : n + 1 = succ n -:= - calc - n + 1 = succ (n + 0) : add_succ _ _ - ... = succ n : {add_zero _} - -theorem add_one_left (n:ℕ) : 1 + n = succ n -:= - calc - 1 + n = succ (0 + n) : succ_add _ _ - ... = succ n : {zero_add _} - ---the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it -theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0) - (H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a -:= nat.rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a - --------------------------------------------------- mul - -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_succ_right (n m:ℕ) : n * succ m = n * m + n -set_option unifier.max_steps 100000 ----------- comm, distr, assoc, identity - -theorem mul_zero_left (n:ℕ) : 0 * n = 0 -:= nat.induction_on n - (mul_zero_right 0) - (take m IH, - calc - 0 * succ m = 0 * m + 0 : mul_succ_right _ _ - ... = 0 * m : add_zero _ - ... = 0 : IH) - -theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m -:= nat.induction_on m - (calc - succ n * 0 = 0 : mul_zero_right _ - ... = n * 0 : symm (mul_zero_right _) - ... = n * 0 + 0 : symm (add_zero _)) - (take k IH, - calc - 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 : symm (add_assoc _ _ _) - ... = (n * succ k) + succ k : {symm (mul_succ_right n k)}) - -theorem mul_comm (n m:ℕ) : n * m = m * n -:= nat.induction_on m - (trans (mul_zero_right _) (symm (mul_zero_left _))) - (take k IH, - calc - n * succ k = n * k + n : mul_succ_right _ _ - ... = k * n + n : {IH} - ... = (succ k) * n : symm (mul_succ_left _ _)) - -theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k -:= nat.induction_on k - (calc - (n + m) * 0 = 0 : mul_zero_right _ - ... = 0 + 0 : symm (add_zero _) - ... = n * 0 + 0 : eq.refl _ - ... = n * 0 + m * 0 : eq.refl _) - (take l IH, calc - (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 : symm (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) : {symm (mul_succ_right _ _)} - ... = n * succ l + m * succ l : {symm (mul_succ_right _ _)}) - -theorem mul_add_distr_right (n m k : ℕ) : n * (m + k) = n * m + n * k -:= calc - n * (m + k) = (m + k) * n : mul_comm _ _ - ... = m * n + k * n : mul_add_distr_left _ _ _ - ... = n * m + k * n : {mul_comm _ _} - ... = n * m + n * k : {mul_comm _ _} - -theorem mul_assoc (n m k:ℕ) : (n * m) * k = n * (m * k) -:= nat.induction_on k - (calc - (n * m) * 0 = 0 : mul_zero_right _ - ... = n * 0 : symm (mul_zero_right _) - ... = n * (m * 0) : {symm (mul_zero_right _)}) - (take l IH, - calc - (n * m) * succ l = (n * m) * l + n * m : mul_succ_right _ _ - ... = n * (m * l) + n * m : {IH} - ... = n * (m * l + m) : symm (mul_add_distr_right _ _ _) - ... = n * (m * succ l) : {symm (mul_succ_right _ _)}) - -theorem mul_comm_left (n m k : ℕ) : n * (m * k) = m * (n * k) -:= left_comm mul_comm mul_assoc n m k - -theorem mul_comm_right (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 -:= calc - n * 1 = n * 0 + n : mul_succ_right n 0 - ... = 0 + n : {mul_zero_right n} - ... = n : zero_add n - -theorem mul_one_left (n : ℕ) : 1 * n = n -:= calc - 1 * n = n * 1 : mul_comm _ _ - ... = n : mul_one_right n - ----------- inversion - -theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 -:= - discriminate - (take Hn : n = 0, or.intro_left _ Hn) - (take (k : ℕ), - assume (Hk : n = succ k), - discriminate - (take (Hm : m = 0), or.intro_right _ Hm) - (take (l : ℕ), - assume (Hl : m = succ l), - have Heq : succ (k * succ l + l) = n * m, from - symm (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 _ _), - absurd (trans Heq H) (succ_ne_zero _))) - --- see more under "positivity" below --------------------------------------------------- le - -definition le (n m:ℕ) : Prop := ∃k, n + k = m -infix `<=` := le -infix `≤` := le - -theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m -:= exists.intro k H - -theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃ k, n + k = m -:= H - ----------- partial order (totality is part of lt) - -theorem le_intro2 (n m : ℕ) : n ≤ n + m -:= le_intro (eq.refl (n + m)) - -theorem le_refl (n : ℕ) : n ≤ n -:= le_intro (add_zero n) - -theorem zero_le (n : ℕ) : 0 ≤ n -:= le_intro (zero_add n) - -theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 -:= - obtain (k : ℕ) (Hk : n + k = 0), from le_elim H, - eq_zero_of_add_eq_zero_right Hk - -theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 -:= assume H : succ n ≤ 0, - have H2 : succ n = 0, from le_zero H, - absurd H2 (succ_ne_zero n) - -theorem le_zero_inv {n : ℕ} (H : n ≤ 0) : n = 0 -:= obtain (k : ℕ) (Hk : n + k = 0), from le_elim H, - eq_zero_of_add_eq_zero_right Hk - -theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k -:= 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 : symm (add_assoc n l1 l2) - ... = m + l2 : { Hl1 } - ... = k : Hl2) - -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 - (calc - n + (k + l) = n + k + l : { symm (add_assoc n k l) } - ... = m + l : { Hk } - ... = n : Hl - ... = n + 0 : symm (add_zero n)), - have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1, - calc - n = n + 0 : symm (add_zero n) - ... = n + k : { symm L2 } - ... = m : Hk - ----------- interaction with add - -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 + m : { Hl }) - -theorem add_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n + k ≤ m + k -:= (add_comm k m) ▸ (add_comm k n) ▸ (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) - -theorem add_le_left_inv {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 - (calc - k + (n + l) = k + n + l : symm (add_assoc k n l) - ... = k + m : Hl)) - -theorem add_le_right_inv {n m k : ℕ} (H : n + k ≤ m + k) : n ≤ m -:= add_le_left_inv (add_comm m k ▸ add_comm n k ▸ H) - ----------- interaction with succ and pred - -theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m -:= add_one m ▸ add_one n ▸ add_le_right H 1 - -theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m -:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) - -theorem self_le_succ (n : ℕ) : n ≤ succ n -:= le_intro (add_one n) - -theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m -:= le_trans H (self_le_succ m) - -theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m -:= obtain (k : ℕ) (Hk : n + k = m), from (le_elim H), - discriminate - (assume H3 : k = 0, - have Heq : n = m, - from calc - n = n + 0 : (add_zero n)⁻¹ - ... = n + k : {H3⁻¹} - ... = m : Hk, - or.intro_right _ Heq) - (take l:ℕ, - assume H3 : k = succ l, - have Hlt : succ n ≤ m, from - (le_intro - (calc - succ n + l = n + succ l : succ_add_eq_add_succ n l - ... = n + k : {H3⁻¹} - ... = m : Hk)), - or.intro_left _ Hlt) - -theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= or_resolve_left (succ_le_left_or H1) H2 - -theorem succ_le_right_inv {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= or_of_or_of_imp_of_imp (succ_le_left_or H) - (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) - (take H2 : n = succ m, H2) - -theorem succ_le_left_inv {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m -:= 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 : symm (succ_add_eq_add_succ n k) - ... = m : H2, - show n ≤ m, from le_intro H3) - (assume H3 : n = m, - have H4 : succ n ≤ n, from subst (symm H3) H, - have H5 : succ n = n, from le_antisym H4 (self_le_succ n), - show false, from absurd H5 (succ_ne_self n)) - -theorem le_pred_self (n : ℕ) : pred n ≤ n -:= case n - (subst (symm pred_zero) (le_refl 0)) - (take k : ℕ, subst (symm (pred_succ k)) (self_le_succ k)) - -theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m -:= discriminate - (take Hn : n = 0, - have H2 : pred n = 0, - from calc - pred n = pred 0 : {Hn} - ... = 0 : pred_zero, - subst (symm H2) (zero_le (pred m))) - (take k : ℕ, - assume Hn : n = succ k, - obtain (l : ℕ) (Hl : n + l = m), from le_elim H, - have H2 : pred n + l = pred m, - from calc - pred n + l = pred (succ k) + l : {Hn} - ... = k + l : {pred_succ k} - ... = pred (succ (k + l)) : symm (pred_succ (k + l)) - ... = pred (succ k + l) : {symm (succ_add k l)} - ... = pred (n + l) : {symm Hn} - ... = pred m : {Hl}, - le_intro H2) - -theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m -:= discriminate - (take Hn : n = 0, - or.intro_left _ (subst (symm Hn) (zero_le m))) - (take k : ℕ, - assume Hn : n = succ k, - have H2 : pred n = k, - from calc - pred n = pred (succ k) : {Hn} - ... = k : pred_succ k, - have H3 : k ≤ m, from subst H2 H, - have H4 : succ k ≤ m ∨ k = m, from succ_le_left_or H3, - show n ≤ m ∨ n = succ m, from - or_of_or_of_imp_of_imp H4 - (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) - (take H5 : k = m, show n = succ m, from subst H5 Hn)) - --- ### interaction with successor and predecessor - -theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m -:= - obtain (k : ℕ) (Hk : n + k = m), from (le_elim H), - discriminate - (assume H3 : k = 0, - have Heq : n = m, - from calc - n = n + 0 : symm (add_zero n) - ... = n + k : {symm H3} - ... = m : Hk, - or.intro_right _ Heq) - (take l : nat, - assume H3 : k = succ l, - have Hlt : succ n ≤ m, from - (le_intro - (calc - succ n + l = n + succ l : succ_add_eq_add_succ n l - ... = n + k : {symm H3} - ... = m : Hk)), - or.intro_left _ Hlt) - -theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= or_resolve_left (le_imp_succ_le_or_eq H1) H2 - -theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= or_of_or_of_imp_left (le_imp_succ_le_or_eq H) - (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) - -theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m -:= - and.intro - (le_trans (self_le_succ n) H) - (assume H2 : n = m, - have H3 : succ n ≤ n, from subst (symm H2) H, - have H4 : succ n = n, from le_antisym H3 (self_le_succ n), - show false, from absurd H4 (succ_ne_self n)) - -theorem pred_le_self (n : ℕ) : pred n ≤ n -:= - case n - (subst (symm pred_zero) (le_refl 0)) - (take k : nat, subst (symm (pred_succ k)) (self_le_succ k)) - -theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m -:= - discriminate - (take Hn : n = 0, - or.intro_left _ (subst (symm Hn) (zero_le m))) - (take k : nat, - assume Hn : n = succ k, - have H2 : pred n = k, - from calc - pred n = pred (succ k) : {Hn} - ... = k : pred_succ k, - have H3 : k ≤ m, from subst H2 H, - have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, - show n ≤ m ∨ n = succ m, from - or_of_or_of_imp_of_imp H4 - (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) - (take H5 : k = m, show n = succ m, from subst H5 Hn)) - ----------- interaction with mul - -theorem mul_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k * n ≤ k * m -:= - obtain (l : ℕ) (Hl : n + l = m), from (le_elim H), - nat.induction_on k - (have H2 : 0 * n = 0 * m, - from calc - 0 * n = 0 : mul_zero_left n - ... = 0 * m : symm (mul_zero_left m), - show 0 * n ≤ 0 * m, from subst H2 (le_refl (0 * n))) - (take (l : ℕ), - assume IH : l * n ≤ l * m, - have H2 : l * n + n ≤ l * m + m, from add_le IH H, - have H3 : succ l * n ≤ l * m + m, from subst (symm (mul_succ_left l n)) H2, - show succ l * n ≤ succ l * m, from subst (symm (mul_succ_left l m)) H3) - -theorem mul_le_right {n m : ℕ} (H : n ≤ m) (k : ℕ) : n * k ≤ m * k -:= mul_comm k m ▸ mul_comm k n ▸ (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) - --- mul_le_[left|right]_inv below - --------------------------------------------------- lt - -definition lt (n m : ℕ) := succ n ≤ m -infix `<` := lt - -theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m -:= le_intro H - -theorem lt_elim {n m : ℕ} (H : n < m) : ∃ k, succ n + k = m -:= le_elim H - -theorem lt_intro2 (n m : ℕ) : n < n + succ m -:= lt_intro (succ_add_eq_add_succ n m) - --------------------------------------------------- ge, gt - -definition ge (n m : ℕ) := m ≤ n -infix `>=` := ge -infix `≥` := ge - -definition gt (n m : ℕ) := m < n -infix `>` := gt - ----------- basic facts - -theorem lt_ne {n m : ℕ} (H : n < m) : n ≠ m -:= and.elim_right (succ_le_left_inv H) - -theorem lt_irrefl (n : ℕ) : ¬ n < n -:= assume H : n < n, absurd (eq.refl n) (lt_ne H) - -theorem lt_zero (n : ℕ) : 0 < succ n -:= succ_le (zero_le n) - -theorem lt_zero_inv (n : ℕ) : ¬ n < 0 -:= assume H : n < 0, - have H2 : succ n = 0, from le_zero_inv H, - absurd H2 (succ_ne_zero n) - -theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k -:= discriminate - (take (Hm : m = 0), absurd (subst Hm H) (lt_zero_inv n)) - (take (l : ℕ) (Hm : m = succ l), exists.intro l Hm) - ----------- interaction with le - -theorem lt_imp_le_succ {n m : ℕ} (H : n < m) : succ n ≤ m -:= H - -theorem le_succ_imp_lt {n m : ℕ} (H : succ n ≤ m) : n < m -:= H - -theorem self_lt_succ (n : ℕ) : n < succ n -:= le_refl (succ n) - -theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m -:= and.elim_left (succ_le_imp_le_and_ne H) - -theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m -:= le_imp_succ_le_or_eq H - -theorem le_ne_imp_lt {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : n < m -:= le_ne_imp_succ_le H1 H2 - -theorem le_imp_lt_succ {n m : ℕ} (H : n ≤ m) : n < succ m -:= succ_le H - -theorem lt_succ_imp_le {n m : ℕ} (H : n < succ m) : n ≤ m -:= succ_le_cancel H - ----------- trans, antisym - -theorem lt_le_trans {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k -:= le_trans H1 H2 - -theorem le_lt_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k -:= le_trans (succ_le H1) H2 - -theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k -:= lt_le_trans H1 (lt_imp_le H2) - -theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m -:= assume H2 : m < n, absurd (le_lt_trans H H2) (lt_irrefl n) - -theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m -:= assume H2 : m ≤ n, absurd (lt_le_trans H H2) (lt_irrefl n) - -theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n -:= le_imp_not_gt (lt_imp_le H) - ----------- interaction with add - -theorem add_lt_left {n m : ℕ} (H : n < m) (k : ℕ) : k + n < k + m -:= add_succ k n ▸ add_le_left H k - -theorem add_lt_right {n m : ℕ} (H : n < m) (k : ℕ) : n + k < m + k -:= add_comm k m ▸ add_comm k n ▸ 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) - -theorem add_lt_le {n m k l : ℕ} (H1 : n < k) (H2 : m ≤ l) : n + m < k + l -:= lt_le_trans (add_lt_right H1 m) (add_le_left H2 k) - -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_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m -:= add_le_left_inv ((add_succ k n)⁻¹ ▸ H) - -theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m -:= add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H) - ----------- interaction with succ (see also the interaction with le) - -theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m -:= add_one m ▸ add_one n ▸ add_lt_right H 1 - -theorem succ_lt_inv {n m : ℕ} (H : succ n < succ m) : n < m -:= add_lt_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) - -theorem lt_self_succ (n : ℕ) : n < succ n -:= le_refl (succ n) - -theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m -:= lt_trans H (lt_self_succ m) - ----------- totality of lt and le - -theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n -:= nat.induction_on n - (or.intro_left _ (zero_le m)) - (take (k : ℕ), - assume IH : k ≤ m ∨ m < k, - or.elim IH - (assume H : k ≤ m, - obtain (l : ℕ) (Hl : k + l = m), from le_elim H, - discriminate - (assume H2 : l = 0, - have H3 : m = k, - from calc - m = k + l : symm Hl - ... = k + 0 : {H2} - ... = k : add_zero k, - have H4 : m < succ k, from subst H3 (lt_self_succ m), - or.intro_right _ H4) - (take l2 : ℕ, - assume H2 : l = succ l2, - have H3 : succ k + l2 = m, - from calc - succ k + l2 = k + succ l2 : succ_add_eq_add_succ k l2 - ... = k + l : {symm H2} - ... = m : Hl, - or.intro_left _ (le_intro H3))) - (assume H : m < k, or.intro_right _ (succ_lt_right H))) - -theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n -:= or_of_or_of_imp_of_imp (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) - -theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ m < n -:= iff.elim_left or.assoc (trichotomy_alt n m) - -theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n -:= or_of_or_of_imp_of_imp (le_or_lt n m) (assume H : n ≤ m, H) (assume H : m < n, lt_imp_le H) - --- interaction with mul under "positivity" - -theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m < n → P m) → P n) : P n -:= have stronger : ∀k, k ≤ n → P k, from - nat.induction_on n - (take (k : ℕ), - assume H : k ≤ 0, - have H2 : k = 0, from le_zero_inv H, - have H3 : ∀m, m < k → P m, from - (take m : ℕ, - assume H4 : m < k, - have H5 : m < 0, from subst H2 H4, - absurd H5 (lt_zero_inv m)), - show P k, from IH k H3) - (take l : ℕ, - assume IHl : ∀k, k ≤ l → P k, - take k : ℕ, - assume H : k ≤ succ l, - or.elim (succ_le_right_inv H) - (assume H2 : k ≤ l, show P k, from IHl k H2) - (assume H2 : k = succ l, - have H3 : ∀m, m < k → P m, from - (take m : ℕ, - assume H4 : m < k, - have H5 : m ≤ l, from lt_succ_imp_le (subst H2 H4), - show P m, from IHl m H5), - show P k, from IH k H3)), - stronger n (le_refl n) - -theorem case_strong_induction_on {P : ℕ → Prop} (a : ℕ) (H0 : P 0) (Hind : ∀(n : ℕ), (∀m, m ≤ n → P m) → P (succ n)) : P a -:= strong_induction_on a - (take n, case n - (assume H : (∀m, m < 0 → P m), H0) - (take n, assume H : (∀m, m < succ n → P m), - Hind n (take m, assume H1 : m ≤ n, H m (le_imp_lt_succ H1)))) - -theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0 -:= discriminate - (take Hm : m = 0, Hm) - (take k : ℕ, - assume Hm : m = succ k, - have H2 : succ n + k = n, - from calc - succ n + k = n + succ k : succ_add_eq_add_succ n k - ... = n + m : {symm Hm} - ... = n : H, - have H3 : n < n, from lt_intro H2, - have H4 : n ≠ n, from lt_ne H3, - absurd (eq.refl n) H4) - --------------------------------------------------- positivity - --- we use " _ > 0" as canonical way of denoting that a number is positive - ----------- basic - -theorem zero_or_positive (n : ℕ) : n = 0 ∨ n > 0 -:= or_of_or_of_imp_of_imp (or.swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) (take H : n > 0, H) - -theorem succ_positive {n m : ℕ} (H : n = succ m) : n > 0 -:= subst (symm H) (lt_zero m) - -theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0 -:= or.elim (zero_or_positive n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) - -theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l -:= discriminate - (take H2, absurd (subst H2 H) (lt_irrefl 0)) - (take l Hl, exists.intro l Hl) - -theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n -:= obtain (l : ℕ) (Hl : k = succ l), from pos_imp_eq_succ H, - subst (symm Hl) (lt_intro2 n l) - -theorem add_positive_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n -:= subst (add_comm n k) (add_positive_right n H) - - --- Positivity --- --------- --- --- Writing "t > 0" is the preferred way to assert that a natural number is positive. - --- ### basic - --- See also succ_pos. - -theorem succ_pos (n : ℕ) : 0 < succ n -:= succ_le (zero_le n) - -theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y -:= case y H0 (take y', H1 _ (succ_pos _)) - -theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 -:= or_of_or_of_imp_left (or.swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) - -theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 -:= subst (symm H) (succ_pos m) - -theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0 -:= or.elim (zero_or_pos n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) - -theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n -:= subst (add_zero n) (add_lt_left H n) - -theorem add_pos_left (n : ℕ) {k : ℕ} (H : k > 0) : k + n > n -:= subst (add_comm n k) (add_pos_right n H) - ----------- mul - -theorem mul_positive {n m : ℕ} (Hn : n > 0) (Hm : m > 0) : n * m > 0 -:= obtain (k : ℕ) (Hk : n = succ k), from pos_imp_eq_succ Hn, - obtain (l : ℕ) (Hl : m = succ l), from pos_imp_eq_succ Hm, - succ_positive (calc - n * m = succ k * m : {Hk} - ... = succ k * succ l : {Hl} - ... = succ k * l + succ k : mul_succ_right (succ k) l - ... = succ (succ k * l + k) : add_succ _ _) - -theorem mul_positive_inv_left {n m : ℕ} (H : n * m > 0) : n > 0 -:= discriminate - (assume H2 : n = 0, - have H3 : n * m = 0, - from calc - n * m = 0 * m : {H2} - ... = 0 : mul_zero_left m, - have H4 : 0 > 0, from subst H3 H, - absurd H4 (lt_irrefl 0)) - (take l : ℕ, - assume Hl : n = succ l, - subst (symm Hl) (lt_zero l)) - -theorem mul_positive_inv_right {n m : ℕ} (H : n * m > 0) : m > 0 -:= mul_positive_inv_left (subst (mul_comm n m) H) - -theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k -:= - have general : ∀m, n * m = n * k → m = k, from - nat.induction_on k - (take m:ℕ, - assume H : n * m = n * 0, - have H2 : n * m = 0, - from calc - n * m = n * 0 : H - ... = 0 : mul_zero_right n, - have H3 : n = 0 ∨ m = 0, from mul_eq_zero H2, - or_resolve_right H3 (ne.symm (lt_ne Hn))) - (take (l : ℕ), - assume (IH : ∀ m, n * m = n * l → m = l), - take (m : ℕ), - assume (H : n * m = n * succ l), - have H2 : n * succ l > 0, from mul_positive Hn (lt_zero l), - have H3 : m > 0, from mul_positive_inv_right (subst (symm H) H2), - obtain (l2:ℕ) (Hm : m = succ l2), from pos_imp_eq_succ H3, - have H4 : n * l2 + n = n * l + n, - from calc - n * l2 + n = n * succ l2 : symm (mul_succ_right n l2) - ... = n * m : {symm Hm} - ... = n * succ l : H - ... = n * l + n : mul_succ_right n l, - have H5 : n * l2 = n * l, from add_cancel_right H4, - calc - m = succ l2 : Hm - ... = succ l : {IH l2 H5}), - general m H - -theorem mul_right_inj {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k -:= mul_left_inj Hm (subst (mul_comm k m) (subst (mul_comm n m) H)) - --- mul_eq_one below - ----------- 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_positive_right (k * n) Hk, - have H3 : k * n + k ≤ k * m, from subst (mul_succ_right k n) (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 -:= subst (mul_comm k m) (subst (mul_comm k n) (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) - -theorem mul_lt_le {n m k l : ℕ} (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) : n * m < k * l -:= le_lt_trans (mul_le_left H2 n) (mul_lt_right Hl H1) - -theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l -:= - have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m, - have H4 : k * m < k * l, from mul_lt_left (le_lt_trans (zero_le n) H1) H2, - le_lt_trans H3 H4 - -theorem mul_lt_left_inv {n m k : ℕ} (H : k * n < k * m) : n < m -:= - have general : ∀ m, k * n < k * m → n < m, from - nat.induction_on n - (take m : ℕ, - assume H2 : k * 0 < k * m, - have H3 : 0 < k * m, from mul_zero_right k ▸ H2, - show 0 < m, from mul_positive_inv_right H3) - (take l : ℕ, - assume IH : ∀ m, k * l < k * m → l < m, - take m : ℕ, - assume H2 : k * succ l < k * m, - have H3 : 0 < k * m, from le_lt_trans (zero_le _) H2, - have H4 : 0 < m, from mul_positive_inv_right H3, - obtain (l2 : ℕ) (Hl2 : m = succ l2), from pos_imp_eq_succ H4, - have H5 : k * l + k < k * m, from mul_succ_right k l ▸ H2, - have H6 : k * l + k < k * succ l2, from Hl2 ▸ H5, - have H7 : k * l + k < k * l2 + k, from mul_succ_right k l2 ▸ H6, - have H8 : k * l < k * l2, from add_lt_right_inv H7, - have H9 : l < l2, from IH l2 H8, - have H10 : succ l < succ l2, from succ_lt H9, - show succ l < m, from Hl2⁻¹ ▸ H10), - general m H - -theorem mul_lt_right_inv {n m k : ℕ} (H : n * k < m * k) : n < m -:= mul_lt_left_inv (mul_comm m k ▸ mul_comm n k ▸ H) - -theorem mul_le_left_inv {n m k : ℕ} (H : succ k * n ≤ succ k * m) : n ≤ m -:= - have H2 : succ k * n < succ k * m + succ k, from le_lt_trans H (lt_intro2 _ _), - have H3 : succ k * n < succ k * succ m, from subst (symm (mul_succ_right (succ k) m)) H2, - have H4 : n < succ m, from mul_lt_left_inv H3, - show n ≤ m, from lt_succ_imp_le H4 - -theorem mul_le_right_inv {n m k : ℕ} (H : n * succ m ≤ k * succ m) : n ≤ k -:= mul_le_left_inv (subst (mul_comm k (succ m)) (subst (mul_comm n (succ m)) H)) - -theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 -:= - have H2 : n * m > 0, from subst (symm H) (lt_zero 0), - have H3 : n > 0, from mul_positive_inv_left H2, - have H4 : m > 0, from mul_positive_inv_right H2, - or.elim (le_or_lt n 1) - (assume H5 : n ≤ 1, - 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 subst (mul_one_right 2) (subst H H6), - absurd (self_lt_succ 1) (le_imp_not_gt H7)) - -theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 -:= mul_eq_one_left (subst (mul_comm n m) H) - -theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1 -:= and.intro (mul_eq_one_left H) (mul_eq_one_right H) - --------------------------------------------------- sub - -definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m -infixl `-` := sub -theorem sub_zero_right (n : ℕ) : n - 0 = n -theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m) - -theorem sub_zero_left (n : ℕ) : 0 - n = 0 -:= nat.induction_on n (sub_zero_right 0) - (take k : ℕ, - assume IH : 0 - k = 0, - calc - 0 - succ k = pred (0 - k) : sub_succ_right 0 k - ... = pred 0 : {IH} - ... = 0 : pred_zero) - -theorem sub_succ_succ (n m : ℕ) : succ n - succ m = n - m -:= nat.induction_on m - (calc - succ n - 1 = pred (succ n - 0) : sub_succ_right (succ n) 0 - ... = pred (succ n) : {sub_zero_right (succ n)} - ... = n : pred_succ n - ... = n - 0 : symm (sub_zero_right n)) - (take k : ℕ, - assume IH : succ n - succ k = n - k, - calc - succ n - succ (succ k) = pred (succ n - succ k) : sub_succ_right (succ n) (succ k) - ... = pred (n - k) : {IH} - ... = n - succ k : symm (sub_succ_right n k)) - -theorem sub_one (n : ℕ) : n - 1 = pred n -:= calc - n - 1 = pred (n - 0) : sub_succ_right n 0 - ... = pred n : {sub_zero_right n} - -theorem sub_self (n : ℕ) : n - n = 0 -:= nat.induction_on n (sub_zero_right 0) (take k IH, trans (sub_succ_succ k k) IH) - -theorem sub_add_add_right (n m k : ℕ) : (n + k) - (m + k) = n - m -:= nat.induction_on k - (calc - (n + 0) - (m + 0) = n - (m + 0) : {add_zero _} - ... = n - m : {add_zero _}) - (take l : ℕ, - assume IH : (n + l) - (m + l) = n - m, - calc - (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {add_succ _ _} - ... = succ (n + l) - succ (m + l) : {add_succ _ _} - ... = (n + l) - (m + l) : sub_succ_succ _ _ - ... = n - m : IH) - -theorem sub_add_add_left (n m k : ℕ) : (k + n) - (k + m) = n - m -:= subst (add_comm m k) (subst (add_comm n k) (sub_add_add_right n m k)) - -theorem sub_add_left (n m : ℕ) : n + m - m = n -:= nat.induction_on m - (subst (symm (add_zero n)) (sub_zero_right n)) - (take k : ℕ, - assume IH : n + k - k = n, - calc - n + succ k - succ k = succ (n + k) - succ k : {add_succ n k} - ... = n + k - k : sub_succ_succ _ _ - ... = n : IH) - -theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) -:= nat.induction_on k - (calc - n - m - 0 = n - m : sub_zero_right _ - ... = n - (m + 0) : {symm (add_zero m)}) - (take l : ℕ, - assume IH : n - m - l = n - (m + l), - calc - n - m - succ l = pred (n - m - l) : sub_succ_right (n - m) l - ... = pred (n - (m + l)) : {IH} - ... = n - succ (m + l) : symm (sub_succ_right n (m + l)) - ... = n - (m + succ l) : {symm (add_succ m l)}) - -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 m k} - ... = n - (m + k) : sub_succ_succ _ _ - ... = n - m - k : symm (sub_sub n m k) - -theorem sub_add_right_eq_zero (n m : ℕ) : n - (n + m) = 0 -:= calc - n - (n + m) = n - n - m : symm (sub_sub n n m) - ... = 0 - m : {sub_self n} - ... = 0 : sub_zero_left m - -theorem sub_comm (m n k : ℕ) : m - n - k = m - k - n -:= calc - m - n - k = m - (n + k) : sub_sub m n k - ... = m - (k + n) : {add_comm n k} - ... = m - k - n : symm (sub_sub m k n) - -theorem succ_sub_one (n : ℕ) : succ n - 1 = n -:= sub_succ_succ n 0 ⬝ sub_zero_right n - ----------- mul - -theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m -:= nat.induction_on n - (calc - pred 0 * m = 0 * m : {pred_zero} - ... = 0 : mul_zero_left _ - ... = 0 - m : symm (sub_zero_left m) - ... = 0 * m - m : {symm (mul_zero_left m)}) - (take k : ℕ, - assume IH : pred k * m = k * m - m, - calc - pred (succ k) * m = k * m : {pred_succ k} - ... = k * m + m - m : symm (sub_add_left _ _) - ... = succ k * m - m : {symm (mul_succ_left k m)}) - -theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n -:= calc n * pred m = pred m * n : mul_comm _ _ - ... = m * n - n : mul_pred_left m n - ... = n * m - n : {mul_comm m n} - -theorem mul_sub_distr_left (n m k : ℕ) : (n - m) * k = n * k - m * k -:= nat.induction_on m - (calc - (n - 0) * k = n * k : {sub_zero_right n} - ... = n * k - 0 : symm (sub_zero_right _) - ... = n * k - 0 * k : {symm (mul_zero_left _)}) - (take l : ℕ, - assume IH : (n - l) * k = n * k - l * k, - calc - (n - succ l) * k = pred (n - l) * k : {sub_succ_right n l} - ... = (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) : {symm (mul_succ_left l k)}) - -theorem mul_sub_distr_right (n m k : ℕ) : n * (m - k) = n * m - n * k -:= calc - n * (m - k) = (m - k) * n : mul_comm _ _ - ... = m * n - k * n : mul_sub_distr_left _ _ _ - ... = n * m - k * n : {mul_comm _ _} - ... = n * m - n * k : {mul_comm _ _} - --------------------------------------------------- max, min, iteration, maybe: sub, div - -theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n = succ (m - n) -:= sub_induction n m - (take k, - assume H : 0 ≤ k, - calc - succ k - 0 = succ k : sub_zero_right (succ k) - ... = succ (k - 0) : {symm (sub_zero_right k)}) - (take k, - assume H : succ k ≤ 0, - absurd H (not_succ_zero_le k)) - (take k l, - assume IH : k ≤ l → succ l - k = succ (l - k), - take H : succ k ≤ succ l, - calc - succ (succ l) - succ k = succ l - k : sub_succ_succ (succ l) k - ... = succ (l - k) : IH (succ_le_cancel H) - ... = succ (succ l - succ k) : {symm (sub_succ_succ l k)}) - -theorem le_imp_sub_eq_zero {n m : ℕ} (H : n ≤ m) : n - m = 0 -:= obtain (k : ℕ) (Hk : n + k = m), from le_elim H, subst Hk (sub_add_right_eq_zero n k) - -theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m -:= sub_induction n m - (take k, - assume H : 0 ≤ k, - calc - 0 + (k - 0) = k - 0 : zero_add (k - 0) - ... = k : sub_zero_right k) - (take k, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k)) - (take k l, - assume IH : k ≤ l → k + (l - k) = l, - take H : succ k ≤ succ l, - calc - succ k + (succ l - succ k) = succ k + (l - k) : {sub_succ_succ l k} - ... = succ (k + (l - k)) : succ_add k (l - k) - ... = succ l : {IH (succ_le_cancel H)}) - -theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n -:= subst (add_comm m (n - m)) 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 n - -theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m -:= subst (add_comm m (n - m)) add_sub_ge - -theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) -:= or.elim (le_total n m) - (assume H : n ≤ m, subst (symm (add_sub_le H)) H) - (assume H : m ≤ n, subst (symm (add_sub_ge H)) (le_refl n)) - -theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n) -:= or.elim (le_total n m) - (assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m)) - (assume H : m ≤ n, subst (symm (add_sub_ge H)) H) - -theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k) - : P (n - m) -:= or.elim (le_total n m) - (assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3)) - (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3)) - -theorem sub_le_self (n m : ℕ) : n - m ≤ n -:= - sub_split - (assume H : n ≤ m, zero_le n) - (take k : ℕ, assume H : m + k = n, le_intro (subst (add_comm m k) H)) - -theorem le_elim_sub (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 : {symm Hk} - ... = n : sub_add_left n k) - -theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) -:= have l1 : k ≤ m → n + m - k = n + (m - k), from - sub_induction k m - (take m : ℕ, - assume H : 0 ≤ m, - calc - n + m - 0 = n + m : sub_zero_right (n + m) - ... = n + (m - 0) : {symm (sub_zero_right m)}) - (take k : ℕ, assume H : succ k ≤ 0, absurd H (not_succ_zero_le k)) - (take k m, - 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 n m} - ... = n + m - k : sub_succ_succ (n + m) k - ... = n + (m - k) : IH (succ_le_cancel H) - ... = n + (succ m - succ k) : {symm (sub_succ_succ m k)}), - l1 H - -theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m -:= sub_split - (assume H1 : n ≤ m, assume H2 : 0 = 0, H1) - (take k : ℕ, - assume H1 : m + k = n, - assume H2 : k = 0, - have H3 : n = m, from subst (add_zero m) (subst H2 (symm H1)), - subst H3 (le_refl n)) - -theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) - (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) -:= or.elim (le_total n m) - (assume H3 : n ≤ m, - (le_imp_sub_eq_zero H3)⁻¹ ▸ (H2 (m - n) ((add_sub_le H3)⁻¹))) - (assume H3 : m ≤ n, - (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 (n - m) ((add_sub_le H3)⁻¹))) - -theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m -:= have H2 : k - n + n = m + n, from - calc - k - n + n = k : add_sub_ge_left (le_intro H) - ... = n + m : symm H - ... = m + n : add_comm n m, - 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, - obtain (y' : ℕ) (yeq : y = succ y'), from pos_imp_eq_succ ypos, - have xsuby_eq : x - y = x' - y', from - calc - x - y = succ x' - y : {xeq} - ... = succ x' - succ y' : {yeq} - ... = x' - y' : sub_succ_succ _ _, - have H1 : x' - y' ≤ x', from sub_le_self _ _, - have H2 : x' < succ x', from self_lt_succ _, - show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt_trans H1 H2 - --- Max, min, iteration, and absolute difference --- -------------------------------------------- - -definition max (n m : ℕ) : ℕ := n + (m - n) -definition min (n m : ℕ) : ℕ := m - (m - n) - -theorem max_le {n m : ℕ} (H : n ≤ m) : n + (m - n) = m := add_sub_le H - -theorem max_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n := add_sub_ge H - -theorem left_le_max (n m : ℕ) : n ≤ n + (m - n) := le_add_sub_left n m - -theorem right_le_max (n m : ℕ) : m ≤ max n m := le_add_sub_right n m - --- ### absolute difference - --- This section is still incomplete - -definition dist (n m : ℕ) := (n - m) + (m - n) - -theorem dist_comm (n m : ℕ) : dist n m = dist m n -:= add_comm (n - m) (m - n) - -theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m -:= - have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H, - have H3 : n ≤ m, from sub_eq_zero_imp_le H2, - 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 = (n - m) + (m - n) : eq.refl _ - ... = 0 + (m - n) : {le_imp_sub_eq_zero H} - ... = m - n : zero_add (m - n) - -theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m -:= subst (dist_comm m n) (dist_le H) - -theorem dist_zero_right (n : ℕ) : dist n 0 = n -:= trans (dist_ge (zero_le n)) (sub_zero_right n) - -theorem dist_zero_left (n : ℕ) : dist 0 n = n -:= trans (dist_le (zero_le n)) (sub_zero_right n) - -theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m -:= calc - dist k n = k - n : dist_ge (le_intro H) - ... = m : sub_intro H - -theorem dist_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m -:= - calc - dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : eq.refl _ - ... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right _ _ _} - ... = (n - m) + (m - n) : {sub_add_add_right _ _ _} - -theorem dist_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m -:= subst (add_comm m k) (subst (add_comm n k) (dist_add_right n k m)) - -theorem dist_ge_add_right {n m : ℕ} (H : n ≥ m) : dist n m + m = n -:= calc - dist n m + m = n - m + m : {dist_ge H} - ... = n : add_sub_ge_left H - -theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m -:= calc - dist n k = dist (n + m) (k + m) : symm (dist_add_right n m k) - ... = dist (k + l) (k + m) : {H} - ... = dist l m : dist_add_left k l m - - - -end nat -end experiment diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index 0a7466fbc..430227112 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -1,4 +1,17 @@ decidable : Prop → Type₁ +has_add : Type → Type +has_divide : Type → Type +has_division : Type → Type +has_dvd : Type → Type +has_inv : Type → Type +has_le : Type → Type +has_lt : Type → Type +has_modulo : Type → Type +has_mul : Type → Type +has_neg : Type → Type +has_one : Type → Type +has_sub : Type → Type +has_zero : Type → Type inhabited : Type → Type measurable : Type → Type nonempty : Type → Prop @@ -7,6 +20,19 @@ setoid : Type → Type subsingleton : Type → Prop well_founded : Π {A : Type}, (A → A → Prop) → Prop decidable : Prop → Type₁ +has_add : Type → Type +has_divide : Type → Type +has_division : Type → Type +has_dvd : Type → Type +has_inv : Type → Type +has_le : Type → Type +has_lt : Type → Type +has_modulo : Type → Type +has_mul : Type → Type +has_neg : Type → Type +has_one : Type → Type +has_sub : Type → Type +has_zero : Type → Type inhabited : Type → Type measurable : Type → Type nonempty : Type → Prop diff --git a/tests/lean/unfold_rec.lean b/tests/lean/unfold_rec.lean index 4cba6a278..3ad4114ad 100644 --- a/tests/lean/unfold_rec.lean +++ b/tests/lean/unfold_rec.lean @@ -7,7 +7,6 @@ variable {n : nat} theorem tst1 : ∀ n m, succ n + succ m = succ (succ (n + m)) := begin intro n m, - esimp [add], state, rewrite [succ_add] end diff --git a/tests/lean/unfold_rec.lean.expected.out b/tests/lean/unfold_rec.lean.expected.out index 0961d8d4d..b7a993e92 100644 --- a/tests/lean/unfold_rec.lean.expected.out +++ b/tests/lean/unfold_rec.lean.expected.out @@ -1,14 +1,14 @@ -unfold_rec.lean:11:2: proof state +unfold_rec.lean:10:2: proof state n m : ℕ -⊢ succ (succ n + m) = succ (succ (n + m)) -unfold_rec.lean:24:2: proof state +⊢ succ n + succ m = succ (succ (n + m)) +unfold_rec.lean:23:2: proof state n m : ℕ ⊢ succ (n + succ m) = succ (succ (n + m)) -unfold_rec.lean:39:2: proof state +unfold_rec.lean:38:2: proof state fibgt0 : ∀ (b n c : ℕ), fib ℕ b n c > 0, b m c : ℕ ⊢ fib ℕ b m c + fib ℕ b (succ m) c > 0 -unfold_rec.lean:48:2: proof state +unfold_rec.lean:47:2: proof state A : Type, B : Type, unzip_zip : ∀ {n : ℕ} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂), diff --git a/tests/lean/unfoldf.lean b/tests/lean/unfoldf.lean index 95bd708db..4a943a9fa 100644 --- a/tests/lean/unfoldf.lean +++ b/tests/lean/unfoldf.lean @@ -1,6 +1,6 @@ open nat -definition id [unfold-full] {A : Type} (a : A) := a +definition id [unfold_full] {A : Type} (a : A) := a definition compose {A B C : Type} (g : B → C) (f : A → B) (a : A) := g (f a) notation g ∘ f := compose g f @@ -18,7 +18,7 @@ begin exact H end -attribute compose [unfold-full] +attribute compose [unfold_full] example (a b : nat) (H : a = b) : (id ∘ id) a = b := begin diff --git a/tests/lean/unzip_error.lean b/tests/lean/unzip_error.lean index 25fb95ce2..785a7772f 100644 --- a/tests/lean/unzip_error.lean +++ b/tests/lean/unzip_error.lean @@ -6,9 +6,9 @@ variables {A B : Type} definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n | unzip nil := (nil, nil) | unzip ((a, b) :: v) := - match unzip v with + match unzip v with -- ERROR (va, vb) := (a :: va, b :: vb) end -example : unzip ((1, 20) :: (2, 30) :: nil) = (1 :: 2 :: nil, 20 :: 30 :: nil) := +example : unzip ((1, 20) :: (2, 30) :: nil) = ((1 :: 2 :: nil, 20 :: 30 :: nil) : vector nat 2 × vector nat 2) := rfl diff --git a/tests/lean/urec.lean.expected.out b/tests/lean/urec.lean.expected.out index 357e76c28..e95bb410a 100644 --- a/tests/lean/urec.lean.expected.out +++ b/tests/lean/urec.lean.expected.out @@ -21,7 +21,7 @@ recursor information dep. elimination: 1 vector.induction_on.{l_1} : ∀ {A : Type.{l_1}} {C : Π (a : ℕ), vector.{l_1} A a → Prop} {a : ℕ} (n : vector.{l_1} A a), - C nat.zero (@vector.nil.{l_1} A) → + C 0 (@vector.nil.{l_1} A) → (∀ {n : ℕ} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) → C a n recursor information diff --git a/tests/lean/whnf.lean b/tests/lean/whnf.lean index e6405e730..76efca607 100644 --- a/tests/lean/whnf.lean +++ b/tests/lean/whnf.lean @@ -1,7 +1,7 @@ open nat -eval [whnf] (fun x, x + 1) 2 -eval (fun x, x + 1) 2 +eval [whnf] (fun x, x + 1) (2:nat) +eval (fun x, x + 1) (2:nat) variable a : nat eval [whnf] a + succ zero