diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index b818a6718c..fc1b4ed810 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -17,22 +17,22 @@ or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl) theorem lt_or_eq_of_le {m n : ℕ} (H : m ≤ n) : m < n ∨ m = n := lt.by_cases - (assume H1 : m < n, or.inl H1) - (assume H1 : m = n, or.inr H1) - (assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl) + (suppose m < n, or.inl this) + (suppose m = n, or.inr this) + (suppose m > n, absurd (lt_of_le_of_lt H this) !lt.irrefl) theorem le_iff_lt_or_eq (m n : ℕ) : m ≤ n ↔ m < n ∨ m = n := iff.intro lt_or_eq_of_le le_of_lt_or_eq theorem lt_of_le_and_ne {m n : ℕ} (H1 : m ≤ n) (H2 : m ≠ n) : m < n := or.elim (lt_or_eq_of_le H1) - (take H3 : m < n, H3) - (take H3 : m = n, by contradiction) + (suppose m < n, this) + (suppose m = n, by contradiction) theorem lt_iff_le_and_ne (m n : ℕ) : m < n ↔ m ≤ n ∧ m ≠ n := iff.intro - (take H, and.intro (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H))) - (take H, lt_of_le_and_ne (and.elim_left H) (and.elim_right H)) + (suppose m < n, and.intro (le_of_lt this) (take H1, lt.irrefl _ (H1 ▸ this))) + (suppose m ≤ n ∧ m ≠ n, lt_of_le_and_ne (and.elim_left this) (and.elim_right this)) theorem le_add_right (n k : ℕ) : n ≤ n + k := nat.induction_on k @@ -54,9 +54,9 @@ by induction h with m h ih;existsi 0; reflexivity; theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m := lt.by_cases - (assume H : m < n, or.inl (le_of_lt H)) - (assume H : m = n, or.inl (by subst m)) - (assume H : m > n, or.inr (le_of_lt H)) + (suppose m < n, or.inl (le_of_lt this)) + (suppose m = n, or.inl (by subst m)) + (suppose m > n, or.inr (le_of_lt this)) /- addition -/ @@ -94,8 +94,8 @@ theorem lt_add_of_pos_right {n k : ℕ} (H : k > 0) : n < n + k := theorem mul_le_mul_left {n m : ℕ} (k : ℕ) (H : n ≤ m) : k * n ≤ k * m := obtain (l : ℕ) (Hl : n + l = m), from le.elim H, -have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl], -le.intro H2 +have k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl], +le.intro this theorem mul_le_mul_right {n m : ℕ} (k : ℕ) (H : n ≤ m) : n * k ≤ m * k := !mul.comm ▸ !mul.comm ▸ !mul_le_mul_left H @@ -104,9 +104,8 @@ theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2) theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m := -have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk, -have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H), -lt_of_lt_of_le H2 H3 +calc k * n < k * n + k : lt_add_of_pos_right Hk + ... ≤ k * m : !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H) theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k := !mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk @@ -123,27 +122,26 @@ eq.rec_on !if_t_t rfl theorem max_le {n m k : ℕ} (H₁ : n ≤ k) (H₂ : m ≤ k) : max n m ≤ k := decidable.by_cases - (assume H : n < m, by rewrite [↑max, if_pos H]; apply H₂) - (assume H : ¬ n < m, by rewrite [↑max, if_neg H]; apply H₁) + (suppose n < m, by rewrite [↑max, if_pos this]; apply H₂) + (suppose ¬ n < m, by rewrite [↑max, if_neg this]; apply H₁) theorem min_le_left (n m : ℕ) : min n m ≤ n := decidable.by_cases - (assume H : n < m, by rewrite [↑min, if_pos H]) - (assume H : ¬ n < m, - assert H' : m ≤ n, from or_resolve_right !lt_or_ge H, - by rewrite [↑min, if_neg H]; apply H') + (suppose n < m, by rewrite [↑min, if_pos this]) + (suppose ¬ n < m, + assert m ≤ n, from or_resolve_right !lt_or_ge this, + by rewrite [↑min, if_neg `¬ n < m`]; apply this) theorem min_le_right (n m : ℕ) : min n m ≤ m := decidable.by_cases - (assume H : n < m, by rewrite [↑min, if_pos H]; apply le_of_lt H) - (assume H : ¬ n < m, - assert H' : m ≤ n, from or_resolve_right !lt_or_ge H, - by rewrite [↑min, if_neg H]) + (suppose n < m, by rewrite [↑min, if_pos this]; apply le_of_lt this) + (suppose ¬ n < m, + by rewrite [↑min, if_neg `¬ n < m`]) theorem le_min {n m k : ℕ} (H₁ : k ≤ n) (H₂ : k ≤ m) : k ≤ min n m := decidable.by_cases - (assume H : n < m, by rewrite [↑min, if_pos H]; apply H₁) - (assume H : ¬ n < m, by rewrite [↑min, if_neg H]; apply H₂) + (suppose n < m, by rewrite [↑min, if_pos this]; apply H₁) + (suppose ¬ n < m, by rewrite [↑min, if_neg this]; apply H₂) theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b := (if_pos H)⁻¹ @@ -163,8 +161,8 @@ by_cases theorem le_max_left (a b : ℕ) : a ≤ max a b := by_cases - (λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h)) - (λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl) + (suppose a < b, le_of_lt (eq.rec_on (eq_max_right this) this)) + (suppose ¬ a < b, eq.rec_on (eq_max_left this) !le.refl) /- nat is an instance of a linearly ordered semiring and a lattice-/ @@ -282,31 +280,31 @@ le.intro !add_one theorem succ_le_or_eq_of_le {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m := or.elim (lt_or_eq_of_le H) - (assume H1 : n < m, or.inl (succ_le_of_lt H1)) - (assume H1 : n = m, or.inr H1) + (suppose n < m, or.inl (succ_le_of_lt this)) + (suppose n = m, or.inr this) theorem pred_le_of_le_succ {n m : ℕ} : n ≤ succ m → pred n ≤ m := nat.cases_on n (assume H, !pred_zero⁻¹ ▸ zero_le m) (take n', - assume H : succ n' ≤ succ m, - have H1 : n' ≤ m, from le_of_succ_le_succ H, - !pred_succ⁻¹ ▸ H1) + suppose succ n' ≤ succ m, + have n' ≤ m, from le_of_succ_le_succ this, + !pred_succ⁻¹ ▸ this) theorem succ_le_of_le_pred {n m : ℕ} : succ n ≤ m → n ≤ pred m := nat.cases_on m (assume H, absurd H !not_succ_le_zero) (take m', - assume H : succ n ≤ succ m', - have H1 : n ≤ m', from le_of_succ_le_succ H, - !pred_succ⁻¹ ▸ H1) + suppose succ n ≤ succ m', + have n ≤ m', from le_of_succ_le_succ this, + !pred_succ⁻¹ ▸ this) theorem pred_le_pred_of_le {n m : ℕ} : n ≤ m → pred n ≤ pred m := nat.cases_on n (assume H, pred_zero⁻¹ ▸ zero_le (pred m)) (take n', - assume H : succ n' ≤ m, - !pred_succ⁻¹ ▸ succ_le_of_le_pred H) + suppose succ n' ≤ m, + !pred_succ⁻¹ ▸ succ_le_of_le_pred this) theorem pre_lt_of_lt : ∀ {n m : ℕ}, n < m → pred n < m | 0 m h := h @@ -314,12 +312,12 @@ theorem pre_lt_of_lt : ∀ {n m : ℕ}, n < m → pred n < m theorem lt_of_pred_lt_pred {n m : ℕ} (H : pred n < pred m) : n < m := lt_of_not_ge - (take H1 : m ≤ n, - not_lt_of_ge (pred_le_pred_of_le H1) H) + (suppose m ≤ n, + not_lt_of_ge (pred_le_pred_of_le this) H) theorem le_or_eq_succ_of_le_succ {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m := or_of_or_of_imp_left (succ_le_or_eq_of_le H) - (take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2) + (suppose succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ this) theorem le_pred_self (n : ℕ) : pred n ≤ n := nat.cases_on n @@ -334,8 +332,9 @@ theorem succ_pred_of_pos {n : ℕ} (H : n > 0) : succ (pred n) = n := theorem exists_eq_succ_of_lt {n m : ℕ} (H : n < m) : exists k, m = succ k := discriminate - (take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero) - (take (l : ℕ) (Hm : m = succ l), exists.intro l Hm) + (suppose m = 0, absurd (this ▸ H) !not_lt_zero) + (take l, suppose m = succ l, + exists.intro l this) theorem lt_succ_self (n : ℕ) : n < succ n := lt.base n @@ -346,20 +345,20 @@ assume Plt, lt.trans Plt (self_lt_succ j) /- other forms of induction -/ protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := -have H1 : ∀ {n m : nat}, m < n → P m, from +have ∀ {n m : nat}, m < n → P m, from take n, nat.rec_on n (show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero) (take n', assume IH : ∀ {m : nat}, m < n' → P m, - assert H2: P n', from H n' @IH, + assert P n', from H n' @IH, show ∀m, m < succ n' → P m, from take m, - assume H3 : m < succ n', - or.by_cases (lt_or_eq_of_le (le_of_lt_succ H3)) - (assume H4: m < n', IH H4) - (assume H4: m = n', by subst m; assumption)), -H1 !lt_succ_self + suppose m < succ n', + or.by_cases (lt_or_eq_of_le (le_of_lt_succ this)) + (suppose m < n', IH this) + (suppose m = n', by subst m; assumption)), +this !lt_succ_self protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := @@ -371,11 +370,11 @@ nat.strong_induction_on a (take n, show (∀ m, m < n → P m) → P n, from nat.cases_on n - (assume H : (∀m, m < 0 → P m), show P 0, from H0) + (suppose (∀ m, m < 0 → P m), show P 0, from H0) (take n, - assume H : (∀m, m < succ n → P m), + suppose (∀ m, m < succ n → P m), show P (succ n), from - Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1)))) + Hind n (take m, assume H1 : m ≤ n, this _ (lt_succ_of_le H1)))) /- pos -/ @@ -386,7 +385,7 @@ nat.cases_on y H0 (take y, H1 !succ_pos) theorem eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 := or_of_or_of_imp_left (or.swap (lt_or_eq_of_le !zero_le)) - (take H : 0 = n, by subst n) + (suppose 0 = n, by subst n) theorem pos_of_ne_zero {n : ℕ} (H : n ≠ 0) : n > 0 := or.elim !eq_zero_or_pos (take H2 : n = 0, by contradiction) (take H2 : n > 0, H2) @@ -399,9 +398,9 @@ exists_eq_succ_of_lt H theorem pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) : m > 0 := pos_of_ne_zero - (assume H3 : m = 0, - assert H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1), - ne_of_lt H2 (by subst n)) + (suppose m = 0, + assert n = 0, from eq_zero_of_zero_dvd (this ▸ H1), + ne_of_lt H2 (by subst n)) /- multiplication -/ @@ -420,10 +419,10 @@ lt_of_le_of_lt H3 H4 theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k := have n * m ≤ n * k, by rewrite H, -have h : m ≤ k, from le_of_mul_le_mul_left this Hn, +have m ≤ k, from le_of_mul_le_mul_left this Hn, have n * k ≤ n * m, by rewrite H, -have k ≤ m, from le_of_mul_le_mul_left this Hn, -le.antisymm h this +have k ≤ m, from le_of_mul_le_mul_left this Hn, +le.antisymm `m ≤ k` this theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k := eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H) @@ -438,12 +437,12 @@ eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H) theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 := have H2 : n * m > 0, by rewrite H; apply succ_pos, or.elim (le_or_gt n 1) - (assume H5 : n ≤ 1, + (suppose n ≤ 1, have n > 0, from pos_of_mul_pos_right H2, - show n = 1, from le.antisymm H5 (succ_le_of_lt this)) - (assume H5 : n > 1, + show n = 1, from le.antisymm `n ≤ 1` (succ_le_of_lt this)) + (suppose n > 1, have m > 0, from pos_of_mul_pos_left H2, - have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt this), + have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt `n > 1`) (succ_le_of_lt this), have 1 ≥ 2, from !mul_one ▸ H ▸ this, absurd !lt_succ_self (not_lt_of_ge this)) @@ -458,9 +457,8 @@ eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H) theorem eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) : n = 1 := dvd.elim H - (take m, - assume H1 : 1 = n * m, - eq_one_of_mul_eq_one_right H1⁻¹) + (take m, suppose 1 = n * m, + eq_one_of_mul_eq_one_right this⁻¹) /- min and max -/ open decidable @@ -494,45 +492,45 @@ theorem max_succ_succ [simp] (a b : ℕ) : max (succ a) (succ b) = succ (max a b by_cases (suppose a < b, by unfold max; rewrite [if_pos this, if_pos (succ_lt_succ this)]) (suppose ¬ a < b, - assert h : ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this, - by unfold max; rewrite [if_neg this, if_neg h]) + assert ¬ succ a < succ b, from assume h, absurd (lt_of_succ_lt_succ h) this, + by unfold max; rewrite [if_neg `¬ a < b`, if_neg `¬ succ a < succ b`]) theorem lt_min {a b c : ℕ} (H₁ : a < b) (H₂ : a < c) : a < min b c := decidable.by_cases - (assume H : b ≤ c, by rewrite (min_eq_left H); apply H₁) - (assume H : ¬ b ≤ c, - assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H), - by rewrite (min_eq_right H'); apply H₂) + (suppose b ≤ c, by rewrite (min_eq_left this); apply H₁) + (suppose ¬ b ≤ c, + assert c ≤ b, from le_of_lt (lt_of_not_ge this), + by rewrite (min_eq_right this); apply H₂) theorem max_lt {a b c : ℕ} (H₁ : a < c) (H₂ : b < c) : max a b < c := decidable.by_cases - (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂) - (assume H : ¬ a ≤ b, - assert H' : b ≤ a, from le_of_lt (lt_of_not_ge H), - by rewrite (max_eq_left H'); apply H₁) + (suppose a ≤ b, by rewrite (max_eq_right this); apply H₂) + (suppose ¬ a ≤ b, + assert b ≤ a, from le_of_lt (lt_of_not_ge this), + by rewrite (max_eq_left this); apply H₁) theorem min_add_add_left (a b c : ℕ) : min (a + b) (a + c) = a + min b c := decidable.by_cases - (assume H : b ≤ c, - assert H1 : a + b ≤ a + c, from add_le_add_left H _, - by rewrite [min_eq_left H, min_eq_left H1]) - (assume H : ¬ b ≤ c, - assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H), - assert H1 : a + c ≤ a + b, from add_le_add_left H' _, - by rewrite [min_eq_right H', min_eq_right H1]) + (suppose b ≤ c, + assert a + b ≤ a + c, from add_le_add_left this _, + by rewrite [min_eq_left `b ≤ c`, min_eq_left this]) + (suppose ¬ b ≤ c, + assert c ≤ b, from le_of_lt (lt_of_not_ge this), + assert a + c ≤ a + b, from add_le_add_left this _, + by rewrite [min_eq_right `c ≤ b`, min_eq_right this]) theorem min_add_add_right (a b c : ℕ) : min (a + c) (b + c) = min a b + c := by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply min_add_add_left theorem max_add_add_left (a b c : ℕ) : max (a + b) (a + c) = a + max b c := decidable.by_cases - (assume H : b ≤ c, - assert H1 : a + b ≤ a + c, from add_le_add_left H _, - by rewrite [max_eq_right H, max_eq_right H1]) - (assume H : ¬ b ≤ c, - assert H' : c ≤ b, from le_of_lt (lt_of_not_ge H), - assert H1 : a + c ≤ a + b, from add_le_add_left H' _, - by rewrite [max_eq_left H', max_eq_left H1]) + (suppose b ≤ c, + assert a + b ≤ a + c, from add_le_add_left this _, + by rewrite [max_eq_right `b ≤ c`, max_eq_right this]) + (suppose ¬ b ≤ c, + assert c ≤ b, from le_of_lt (lt_of_not_ge this), + assert a + c ≤ a + b, from add_le_add_left this _, + by rewrite [max_eq_left `c ≤ b`, max_eq_left this]) theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c := by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply max_add_add_left diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean index ce2690cfc8..e3e5ccf18d 100644 --- a/library/data/nat/pairing.lean +++ b/library/data/nat/pairing.lean @@ -19,54 +19,54 @@ if n - s*s < s then (n - s*s, s) else (s, n - s*s - s) theorem mkpair_unpair (n : nat) : mkpair (pr1 (unpair n)) (pr2 (unpair n)) = n := let s := sqrt n in by_cases - (λ h₁ : n - s*s < s, + (suppose n - s*s < s, begin esimp [unpair], - rewrite [if_pos h₁], + rewrite [if_pos this], esimp [mkpair], - rewrite [if_pos h₁, add_sub_of_le (sqrt_lower n)] + rewrite [if_pos this, add_sub_of_le (sqrt_lower n)] end) - (λ h₂ : ¬ n - s*s < s, - have g₁ : s ≤ n - s*s, from le_of_not_gt h₂, - assert g₂ : s + s*s ≤ n - s*s + s*s, from add_le_add_right g₁ (s*s), - assert g₃ : s*s + s ≤ n, by rewrite [sub_add_cancel (sqrt_lower n) at g₂, add.comm at g₂]; assumption, - have l₁ : n ≤ s*s + s + s, from sqrt_upper n, - have l₂ : n - s*s ≤ s + s, from calc - n - s*s ≤ (s*s + s + s) - s*s : sub_le_sub_right l₁ (s*s) + (suppose h₁ : ¬ n - s*s < s, + have s ≤ n - s*s, from le_of_not_gt h₁, + assert s + s*s ≤ n - s*s + s*s, from add_le_add_right this (s*s), + assert s*s + s ≤ n, by rewrite [sub_add_cancel (sqrt_lower n) at this, add.comm at this]; assumption, + have n ≤ s*s + s + s, from sqrt_upper n, + have n - s*s ≤ s + s, from calc + n - s*s ≤ (s*s + s + s) - s*s : sub_le_sub_right this (s*s) ... = (s*s + (s+s)) - s*s : by rewrite add.assoc ... = s + s : by rewrite add_sub_cancel_left, - have l₃ : n - s*s - s ≤ s, from calc - n - s*s - s ≤ (s + s) - s : sub_le_sub_right l₂ s + have n - s*s - s ≤ s, from calc + n - s*s - s ≤ (s + s) - s : sub_le_sub_right this s ... = s : by rewrite add_sub_cancel_left, - assert l₄ : ¬ s < n - s*s - s, from not_lt_of_ge l₃, + assert h₂ : ¬ s < n - s*s - s, from not_lt_of_ge this, begin esimp [unpair], - rewrite [if_neg h₂], esimp, + rewrite [if_neg h₁], esimp, esimp [mkpair], - rewrite [if_neg l₄, sub_sub, add_sub_of_le g₃], + rewrite [if_neg h₂, sub_sub, add_sub_of_le `s*s + s ≤ n`], end) theorem unpair_mkpair (a b : nat) : unpair (mkpair a b) = (a, b) := by_cases - (λ h : a < b, - assert aux₁ : a ≤ b + b, from calc - a ≤ b : le_of_lt h + (suppose a < b, + assert a ≤ b + b, from calc + a ≤ b : le_of_lt this ... ≤ b+b : !le_add_right, begin esimp [mkpair], - rewrite [if_pos h], + rewrite [if_pos `a < b`], esimp [unpair], - rewrite [sqrt_offset_eq aux₁, add_sub_cancel_left, if_pos h] + rewrite [sqrt_offset_eq `a ≤ b + b`, add_sub_cancel_left, if_pos `a < b`] end) - (λ h : ¬ a < b, - have h₁ : b ≤ a, from le_of_not_gt h, - assert aux₁ : a + b ≤ a + a, from add_le_add_left h₁ a, - have aux₂ : a + b ≥ a, from !le_add_right, - assert aux₃ : ¬ a + b < a, from not_lt_of_ge aux₂, + (suppose ¬ a < b, + have b ≤ a, from le_of_not_gt this, + assert a + b ≤ a + a, from add_le_add_left this a, + have a + b ≥ a, from !le_add_right, + assert ¬ a + b < a, from not_lt_of_ge this, begin esimp [mkpair], - rewrite [if_neg h], + rewrite [if_neg `¬ a < b`], esimp [unpair], - rewrite [add.assoc (a * a) a b, sqrt_offset_eq aux₁, *add_sub_cancel_left, if_neg aux₃] + rewrite [add.assoc (a * a) a b, sqrt_offset_eq `a + b ≤ a + a`, *add_sub_cancel_left, if_neg `¬ a + b < a`] end) end nat diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean index 6f8c3e64c7..db151a7da7 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -13,12 +13,12 @@ open decidable definition even (n : nat) := n mod 2 = 0 definition decidable_even [instance] : ∀ n, decidable (even n) := -λ n, !nat.has_decidable_eq +take n, !nat.has_decidable_eq definition odd (n : nat) := ¬even n definition decidable_odd [instance] : ∀ n, decidable (odd n) := -λ n, decidable_not +take n, decidable_not lemma even_of_dvd {n} : 2 ∣ n → even n := mod_eq_zero_of_dvd @@ -38,29 +38,34 @@ dec_trivial lemma not_even_one : ¬ even 1 := dec_trivial -lemma odd_eq_not_even : ∀ n, odd n = ¬ even n := -λ n, rfl +lemma odd_eq_not_even (n : nat) : odd n = ¬ even n := +rfl -lemma odd_iff_not_even : ∀ n, odd n ↔ ¬ even n := -λ n, !iff.refl +lemma odd_iff_not_even (n : nat) : odd n ↔ ¬ even n := +!iff.refl lemma odd_of_not_even {n} : ¬ even n → odd n := -λ h, iff.mpr !odd_iff_not_even h +suppose ¬ even n, +iff.mpr !odd_iff_not_even this lemma even_of_not_odd {n} : ¬ odd n → even n := -λ h, not_not_elim (iff.mp (not_iff_not_of_iff !odd_iff_not_even) h) +suppose ¬ odd n, +not_not_elim (iff.mp (not_iff_not_of_iff !odd_iff_not_even) this) lemma not_odd_of_even {n} : even n → ¬ odd n := -λ h, iff.mpr (not_iff_not_of_iff !odd_iff_not_even) (not_not_intro h) +suppose even n, +iff.mpr (not_iff_not_of_iff !odd_iff_not_even) (not_not_intro this) lemma not_even_of_odd {n} : odd n → ¬ even n := -λ h, iff.mp !odd_iff_not_even h +suppose odd n, +iff.mp !odd_iff_not_even this lemma odd_succ_of_even {n} : even n → odd (succ n) := -λ h, by_contradiction (λ hn : ¬ odd (succ n), +suppose even n, +by_contradiction (suppose ¬ odd (succ n), assert 0 = 1, from calc - 0 = (n+1) mod 2 : even_of_not_odd hn - ... = 1 mod 2 : add_mod_eq_add_mod_right 1 h, + 0 = (n+1) mod 2 : even_of_not_odd this + ... = 1 mod 2 : add_mod_eq_add_mod_right 1 `even n`, by contradiction) lemma eq_1_of_ne_0_lt_2 : ∀ {n : nat}, n ≠ 0 → n < 2 → n = 1 @@ -69,64 +74,72 @@ lemma eq_1_of_ne_0_lt_2 : ∀ {n : nat}, n ≠ 0 → n < 2 → n = 1 | (n+2) h₁ h₂ := absurd (lt_of_succ_lt_succ (lt_of_succ_lt_succ h₂)) !not_lt_zero lemma mod_eq_of_odd {n} : odd n → n mod 2 = 1 := -λ h, - have h₁ : ¬ n mod 2 = 0, from h, - have h₂ : n mod 2 < 2, from mod_lt n dec_trivial, - eq_1_of_ne_0_lt_2 h₁ h₂ +suppose odd n, + have ¬ n mod 2 = 0, from this, + have n mod 2 < 2, from mod_lt n dec_trivial, + eq_1_of_ne_0_lt_2 `¬ n mod 2 = 0` `n mod 2 < 2` lemma odd_of_mod_eq {n} : n mod 2 = 1 → odd n := -λ h, by_contradiction (λ hn, - assert h₁ : n mod 2 = 0, from even_of_not_odd hn, - by rewrite h at h₁; contradiction) +suppose n mod 2 = 1, +by_contradiction (suppose ¬ odd n, + assert n mod 2 = 0, from even_of_not_odd this, + by rewrite this at *; contradiction) lemma even_succ_of_odd {n} : odd n → even (succ n) := -λ h, - have h₁ : n mod 2 = 1, from mod_eq_of_odd h, - have h₂ : n mod 2 = 1 mod 2, from mod_eq_of_odd h, - have h₃ : (n+1) mod 2 = 0, from add_mod_eq_add_mod_right 1 h₂, - h₃ +suppose odd n, + have n mod 2 = 1 mod 2, from mod_eq_of_odd this, + have (n+1) mod 2 = 0, from add_mod_eq_add_mod_right 1 this, + this lemma odd_succ_succ_of_odd {n} : odd n → odd (succ (succ n)) := -λ h, odd_succ_of_even (even_succ_of_odd h) +suppose odd n, +odd_succ_of_even (even_succ_of_odd this) lemma even_succ_succ_of_even {n} : even n → even (succ (succ n)) := -λ h, even_succ_of_odd (odd_succ_of_even h) +suppose even n, +even_succ_of_odd (odd_succ_of_even this) lemma even_of_odd_succ {n} : odd (succ n) → even n := -λ h, by_contradiction (λ he, - have h₁ : odd n, from odd_of_not_even he, - have h₂ : even (succ n), from even_succ_of_odd h₁, - absurd h₂ (not_even_of_odd h)) +suppose odd (succ n), +by_contradiction (suppose ¬ even n, + have odd n, from odd_of_not_even this, + have even (succ n), from even_succ_of_odd this, + absurd this (not_even_of_odd `odd (succ n)`)) lemma odd_of_even_succ {n} : even (succ n) → odd n := -λ h, by_contradiction (λ he, - have h₁ : even n, from even_of_not_odd he, - have h₂ : odd (succ n), from odd_succ_of_even h₁, - absurd h (not_even_of_odd h₂)) +suppose even (succ n), +by_contradiction (suppose ¬ odd n, + have even n, from even_of_not_odd this, + have odd (succ n), from odd_succ_of_even this, + absurd `even (succ n)` (not_even_of_odd this)) lemma even_of_even_succ_succ {n} : even (succ (succ n)) → even n := -λ h, even_of_odd_succ (odd_of_even_succ h) +suppose even (n+2), +even_of_odd_succ (odd_of_even_succ this) lemma odd_of_odd_succ_succ {n} : odd (succ (succ n)) → odd n := -λ h, odd_of_even_succ (even_of_odd_succ h) +suppose odd (n+2), +odd_of_even_succ (even_of_odd_succ this) lemma dvd_of_odd {n} : odd n → 2 ∣ n+1 := -λ h, dvd_of_even (even_succ_of_odd h) +suppose odd n, +dvd_of_even (even_succ_of_odd this) lemma odd_of_dvd {n} : 2 ∣ n+1 → odd n := -λ h, odd_of_even_succ (even_of_dvd h) +suppose 2 ∣ n+1, +odd_of_even_succ (even_of_dvd this) lemma even_two_mul : ∀ n, even (2 * n) := -λ n, even_of_dvd (dvd_mul_right 2 n) +take n, even_of_dvd (dvd_mul_right 2 n) lemma odd_two_mul_plus_one : ∀ n, odd (2 * n + 1) := -λ n, odd_succ_of_even (even_two_mul n) +take n, odd_succ_of_even (even_two_mul n) lemma not_even_two_mul_plus_one : ∀ n, ¬ even (2 * n + 1) := -λ n, not_even_of_odd (odd_two_mul_plus_one n) +take n, not_even_of_odd (odd_two_mul_plus_one n) lemma not_odd_two_mul : ∀ n, ¬ odd (2 * n) := -λ n, not_odd_of_even (even_two_mul n) +take n, not_odd_of_even (even_two_mul n) lemma even_pred_of_odd : ∀ {n}, odd n → even (pred n) | 0 h := absurd h not_odd_zero @@ -147,59 +160,61 @@ lemma exists_of_odd : ∀ {n}, odd n → ∃ k, n = 2*k + 1 exists.intro k (by subst n) lemma even_of_exists {n} : (∃ k, n = 2 * k) → even n := -λ h, obtain k (hk : n = 2 * k), from h, - have h₁ : 2 ∣ n, by subst n; apply dvd_mul_right, - even_of_dvd h₁ +suppose ∃ k, n = 2 * k, +obtain k (hk : n = 2 * k), from this, +have 2 ∣ n, by subst n; apply dvd_mul_right, +even_of_dvd this lemma odd_of_exists {n} : (∃ k, n = 2 * k + 1) → odd n := -λ h, by_contradiction (λ hn, - have h₁ : even n, from even_of_not_odd hn, - have h₂ : ∃ k, n = 2 * k, from exists_of_even h₁, +assume h, by_contradiction (λ hn, + have even n, from even_of_not_odd hn, + have ∃ k, n = 2 * k, from exists_of_even this, obtain k₁ (hk₁ : n = 2 * k₁ + 1), from h, - obtain k₂ (hk₂ : n = 2 * k₂), from h₂, - assert h₃ : (2 * k₁ + 1) mod 2 = (2 * k₂) mod 2, by rewrite [-hk₁, -hk₂], + obtain k₂ (hk₂ : n = 2 * k₂), from this, + assert (2 * k₁ + 1) mod 2 = (2 * k₂) mod 2, by rewrite [-hk₁, -hk₂], begin - rewrite [mul_mod_right at h₃, add.comm at h₃, add_mul_mod_self_left at h₃], + rewrite [mul_mod_right at this, add.comm at this, add_mul_mod_self_left at this], contradiction end) lemma even_add_of_even_of_even {n m} : even n → even m → even (n+m) := -λ h₁ h₂, -obtain k₁ (hk₁ : n = 2 * k₁), from exists_of_even h₁, -obtain k₂ (hk₂ : m = 2 * k₂), from exists_of_even h₂, +suppose even n, suppose even m, +obtain k₁ (hk₁ : n = 2 * k₁), from exists_of_even `even n`, +obtain k₂ (hk₂ : m = 2 * k₂), from exists_of_even `even m`, even_of_exists (exists.intro (k₁+k₂) (by rewrite [hk₁, hk₂, mul.left_distrib])) lemma even_add_of_odd_of_odd {n m} : odd n → odd m → even (n+m) := -λ h₁ h₂, - assert h₃ : even (succ n + succ m), from even_add_of_even_of_even (even_succ_of_odd h₁) (even_succ_of_odd h₂), - have h₄ : even(succ (succ (n + m))), by rewrite [add_succ at h₃, succ_add at h₃]; exact h₃, - even_of_even_succ_succ h₄ +suppose odd n, suppose odd m, +assert even (succ n + succ m), from even_add_of_even_of_even (even_succ_of_odd `odd n`) (even_succ_of_odd `odd m`), +have even(succ (succ (n + m))), by rewrite [add_succ at this, succ_add at this]; exact this, +even_of_even_succ_succ this lemma odd_add_of_even_of_odd {n m} : even n → odd m → odd (n+m) := -λ h₁ h₂, - assert h₃ : even (n + succ m), from even_add_of_even_of_even h₁ (even_succ_of_odd h₂), - odd_of_even_succ h₃ +suppose even n, suppose odd m, +assert even (n + succ m), from even_add_of_even_of_even `even n` (even_succ_of_odd `odd m`), +odd_of_even_succ this lemma odd_add_of_odd_of_even {n m} : odd n → even m → odd (n+m) := -λ h₁ h₂, - assert h₃ : odd (m+n), from odd_add_of_even_of_odd h₂ h₁, - by rewrite add.comm at h₃; exact h₃ +suppose odd n, suppose even m, +assert odd (m+n), from odd_add_of_even_of_odd `even m` `odd n`, +by rewrite add.comm at this; exact this lemma even_mul_of_even_left {n} (m) : even n → even (n*m) := -λ h, - obtain k (hk : n = 2*k), from exists_of_even h, - even_of_exists (exists.intro (k*m) (by rewrite [hk, mul.assoc])) +suppose even n, +obtain k (hk : n = 2*k), from exists_of_even this, +even_of_exists (exists.intro (k*m) (by rewrite [hk, mul.assoc])) lemma even_mul_of_even_right {n} (m) : even n → even (m*n) := -λ h₁, - assert h₂ : even (n*m), from even_mul_of_even_left _ h₁, - by rewrite mul.comm at h₂; exact h₂ +suppose even n, +assert even (n*m), from even_mul_of_even_left _ this, +by rewrite mul.comm at this; exact this lemma odd_mul_of_odd_of_odd {n m} : odd n → odd m → odd (n*m) := -λ h₁ h₂, - assert h₃ : even (n * succ m), from even_mul_of_even_right _ (even_succ_of_odd h₂), - assert h₄ : even (n * m + n), by rewrite mul_succ at h₃; exact h₃, - by_contradiction (λ hn, - assert h₅ : even (n*m), from even_of_not_odd hn, - absurd h₄ (not_even_of_odd (odd_add_of_even_of_odd h₅ h₁))) +suppose odd n, suppose odd m, +assert even (n * succ m), from even_mul_of_even_right _ (even_succ_of_odd `odd m`), +assert even (n * m + n), by rewrite mul_succ at this; exact this, +by_contradiction (suppose ¬ odd (n*m), + assert even (n*m), from even_of_not_odd this, + absurd `even (n * m + n)` (not_even_of_odd (odd_add_of_even_of_odd this `odd n`))) + end nat diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 324b79eae1..3f5ab3a5d5 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -32,16 +32,16 @@ end migrate_algebra -- generalize to semirings? theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i | 0 := !zero_le -| (succ j) := have xpos : x > 0, from lt.trans zero_lt_one H, - have xjge1 : x^j ≥ 1, from succ_le_of_lt (pow_pos_of_pos _ xpos), - have xge2 : x ≥ 2, from succ_le_of_lt H, +| (succ j) := have x > 0, from lt.trans zero_lt_one H, + have x^j ≥ 1, from succ_le_of_lt (pow_pos_of_pos _ this), + have x ≥ 2, from succ_le_of_lt H, calc succ j = j + 1 : rfl ... ≤ x^j + 1 : add_le_add_right (le_pow_self j) - ... ≤ x^j + x^j : add_le_add_left xjge1 + ... ≤ x^j + x^j : add_le_add_left `x^j ≥ 1` ... = x^j * (1 + 1) : by rewrite [mul.left_distrib, *mul_one] ... = x^j * 2 : rfl - ... ≤ x^j * x : mul_le_mul_left _ xge2 + ... ≤ x^j * x : mul_le_mul_left _ `x ≥ 2` ... = x^(succ j) : rfl -- TODO: eventually this will be subsumed under the algebraic theorems @@ -53,17 +53,17 @@ by rewrite [*pow_succ, *pow_zero, one_mul] theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → pow a b = pow a c → b = c | a 0 0 h₁ h₂ := rfl | a (succ b) 0 h₁ h₂ := - assert aeq1 : a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂), - assert h₁ : 1 < 1, by rewrite [aeq1 at h₁]; exact h₁, - absurd h₁ !lt.irrefl + assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂), + assert 1 < 1, by rewrite [this at h₁]; exact h₁, + absurd `1 < 1` !lt.irrefl | a 0 (succ c) h₁ h₂ := - assert aeq1 : a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)), - assert h₁ : 1 < 1, by rewrite [aeq1 at h₁]; exact h₁, - absurd h₁ !lt.irrefl + assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)), + assert 1 < 1, by rewrite [this at h₁]; exact h₁, + absurd `1 < 1` !lt.irrefl | a (succ b) (succ c) h₁ h₂ := - assert ane0 : a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial), - assert beqc : pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero ane0) h₂), - by rewrite [pow_cancel_left h₁ beqc] + assert a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial), + assert pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂), + by rewrite [pow_cancel_left h₁ this] theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → pow a (succ b) div a = pow a b | a 0 h := by rewrite [pow_succ', pow_zero, mul_one, div_self (pos_of_ne_zero h)] @@ -81,9 +81,9 @@ lemma pow_mod_eq_zero (i : nat) {n : nat} (h : n > 0) : (i^n) mod i = 0 := iff.mp !dvd_iff_mod_eq_zero (dvd_pow i h) lemma pow_dvd_of_pow_succ_dvd {p i n : nat} : p^(succ i) ∣ n → p^i ∣ n := -assume Psuccdvd, -assert Pdvdsucc : p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl, -dvd.trans Pdvdsucc Psuccdvd +suppose p^(succ i) ∣ n, +assert p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl, +dvd.trans `p^i ∣ p^(succ i)` `p^(succ i) ∣ n` lemma dvd_of_pow_succ_dvd_mul_pow {p i n : nat} (Ppos : p > 0) : p^(succ i) ∣ (n * p^i) → p ∣ n := @@ -100,6 +100,7 @@ lemma coprime_pow_right {a b} : ∀ n, coprime b a → coprime b (a^n) end lemma coprime_pow_left {a b} : ∀ n, coprime b a → coprime (b^n) a := -λ n h, coprime_swap (coprime_pow_right n (coprime_swap h)) +take n, suppose coprime b a, +coprime_swap (coprime_pow_right n (coprime_swap this)) end nat