From 7f5caab694e3779546bd3f7062a84e1c96ec8f42 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 4 Jun 2015 19:16:28 -0400 Subject: [PATCH] feat(nat): redefine le and lt in the standard library --- hott/init/nat.hlean | 94 ++++--- library/data/encodable.lean | 2 +- library/data/list/set.lean | 9 +- library/data/nat/bquant.lean | 4 +- library/data/nat/choose.lean | 6 +- library/data/nat/div.lean | 2 +- library/data/nat/order.lean | 55 +--- library/data/nat/sqrt.lean | 12 +- library/init/nat.lean | 289 ++++++++++++++++++-- tests/lean/protected_test.lean | 10 +- tests/lean/protected_test.lean.expected.out | 6 +- tests/lean/run/541a.lean | 2 - tests/lean/run/constr_tac4.lean | 6 +- 13 files changed, 342 insertions(+), 155 deletions(-) diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index a5247c36b..d15e72ed0 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -30,6 +30,7 @@ namespace nat nat.cases_on a zero (λ a₁, a₁) -- add is defined in init.num + definition sub (a b : nat) : nat := nat.rec_on b a (λ b₁ r, pred r) @@ -57,49 +58,52 @@ namespace nat /- properties of inequality -/ - definition le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n + theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n - definition le_succ (n : ℕ) : n ≤ succ n := by repeat constructor + theorem le_succ (n : ℕ) : n ≤ succ n := by repeat constructor - definition pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) + theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) - definition le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := + theorem le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := by induction H2 with n H2 IH;exact H1;exact le.step IH - definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ + theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ - definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H + theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H - definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H + theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H - definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := + theorem succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := by induction H;reflexivity;exact le.step v_0 - definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := + theorem pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := by induction H;reflexivity;cases b;exact v_0;exact le.step v_0 - definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := + theorem le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := pred_le_pred H - definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := + theorem le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := by cases n;exact le.step H;exact succ_le_succ H - definition not_succ_le_self {n : ℕ} : ¬succ n ≤ n := + theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n := by induction n with n IH;all_goals intros;cases a;apply IH;exact le_of_succ_le_succ a - definition zero_le (n : ℕ) : 0 ≤ n := + theorem zero_le (n : ℕ) : 0 ≤ n := by induction n with n IH;apply le.refl;exact le.step IH - definition zero_lt_succ (n : ℕ) : 0 < succ n := + theorem lt.step {n m : ℕ} (H : n < m) : n < succ m := + le.step H + + theorem zero_lt_succ (n : ℕ) : 0 < succ n := by induction n with n IH;apply le.refl;exact le.step IH - definition lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := + theorem lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := le.trans (le.step H1) H2 - definition lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k := + theorem lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k := le.trans (succ_le_succ H1) H2 - definition lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k := + theorem lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k := le.trans H1 H2 theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := @@ -111,7 +115,7 @@ namespace nat { exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}}, end - definition not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero := + theorem not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero := by intro H; cases H theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self @@ -128,7 +132,7 @@ namespace nat theorem lt.asymm {n m : ℕ} (H1 : n < m) (H2 : m < n) : empty := le_lt_antisymm (le_of_lt H1) H2 - theorem lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := + definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := begin revert b H1 H2 H3, induction a with a IH, { intros, cases b, @@ -142,16 +146,16 @@ namespace nat intro H, exact H3 (succ_le_succ H)}} end - definition lt.trichotomy (a b : ℕ) : a < b ⊎ a = b ⊎ b < a := - lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H)) - - theorem lt_or_ge (a b : ℕ) : (a < b) ⊎ (a ≥ b) := - lt.by_cases inl (λH, inr (eq.rec_on H !le.refl)) (λH, inr (le_of_lt H)) + theorem lt.trichotomy (a b : ℕ) : a < b ⊎ a = b ⊎ b < a := + lt.by_cases inl (λH, inr (inl H)) (λH, inr (inr H)) definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := - sum.rec_on (lt_or_ge a b) H1 H2 + lt.by_cases H1 (λH, H2 (le_of_eq H⁻¹)) (λH, H2 (le_of_lt H)) - definition not_lt_zero (a : ℕ) : ¬ a < zero := + theorem lt_or_ge (a b : ℕ) : (a < b) ⊎ (a ≥ b) := + lt_ge_by_cases inl inr + + theorem not_lt_zero (a : ℕ) : ¬ a < zero := by intro H; cases H -- less-than is well-founded @@ -198,49 +202,49 @@ namespace nat definition decidable_gt [instance] : decidable_rel gt := _ definition decidable_ge [instance] : decidable_rel ge := _ - definition eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ⊎ a < b := + theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ⊎ a < b := by cases H with b' H; exact sum.inl rfl; exact sum.inr (succ_le_succ H) - definition le_of_eq_or_lt {a b : ℕ} (H : a = b ⊎ a < b) : a ≤ b := + theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ⊎ a < b) : a ≤ b := by cases H with H H; exact le_of_eq H; exact le_of_lt H - definition eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ⊎ b < a := + theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ⊎ b < a := sum.rec_on (lt.trichotomy a b) (λ hlt, absurd hlt hnlt) (λ h, h) - definition lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b := + theorem lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b := succ_le_succ h - definition lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h + theorem lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h - definition succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h + theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h definition max (a b : ℕ) : ℕ := if a < b then b else a definition min (a b : ℕ) : ℕ := if a < b then a else b - definition max_self (a : ℕ) : max a a = a := + theorem max_self (a : ℕ) : max a a = a := eq.rec_on !if_t_t rfl - definition max_eq_right {a b : ℕ} (H : a < b) : max a b = b := + theorem max_eq_right {a b : ℕ} (H : a < b) : max a b = b := if_pos H - definition max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a := + theorem max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a := if_neg H - definition eq_max_right {a b : ℕ} (H : a < b) : b = max a b := + theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b := eq.rec_on (max_eq_right H) rfl - definition eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b := + theorem eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b := eq.rec_on (max_eq_left H) rfl - definition le_max_left (a b : ℕ) : a ≤ max a b := + 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) - definition le_max_right (a b : ℕ) : b ≤ max a b := + theorem le_max_right (a b : ℕ) : b ≤ max a b := by_cases (λ h : a < b, eq.rec_on (eq_max_right h) !le.refl) (λ h : ¬ a < b, sum.rec_on (eq_or_lt_of_not_lt h) @@ -249,21 +253,21 @@ namespace nat have aux : a = max a b, from eq_max_left (lt.asymm h), eq.rec_on aux (le_of_lt h))) - definition succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := + theorem succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := by induction b with b IH; reflexivity; apply ap pred IH - definition sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := + theorem sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := eq.rec_on (succ_sub_succ_eq_sub a b) rfl - definition zero_sub_eq_zero (a : ℕ) : zero - a = zero := + theorem zero_sub_eq_zero (a : ℕ) : zero - a = zero := nat.rec_on a rfl (λ a₁ (ih : zero - a₁ = zero), ap pred ih) - definition zero_eq_zero_sub (a : ℕ) : zero = zero - a := + theorem zero_eq_zero_sub (a : ℕ) : zero = zero - a := eq.rec_on (zero_sub_eq_zero a) rfl - definition sub_lt {a b : ℕ} : zero < a → zero < b → a - b < a := + theorem sub_lt {a b : ℕ} : zero < a → zero < b → a - b < a := have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from λa h₁, le.rec_on h₁ (λb h₂, le.cases_on h₂ @@ -278,7 +282,7 @@ namespace nat (lt.trans (@ih b₁ bpos) (lt.base a₁)))), λ h₁ h₂, aux h₁ h₂ - definition sub_le (a b : ℕ) : a - b ≤ a := + theorem sub_le (a b : ℕ) : a - b ≤ a := nat.rec_on b (le.refl a) (λ b₁ ih, le.trans !pred_le ih) diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 88b91be5f..97cfe74f7 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -42,7 +42,7 @@ encodable.mk begin cases o with a, begin esimp end, - begin esimp, rewrite [if_neg !succ_ne_zero, pred_succ, encodable.encodek] end + begin esimp, rewrite [if_neg !succ_ne_zero, encodable.encodek] end end) section sum diff --git a/library/data/list/set.lean b/library/data/list/set.lean index 7ac52b396..5527ae934 100644 --- a/library/data/list/set.lean +++ b/library/data/list/set.lean @@ -462,9 +462,12 @@ assume i, mem_cons_of_mem _ i theorem mem_upto_of_lt : ∀ {n i : nat}, i < n → i ∈ upto n | 0 i h := absurd h !not_lt_zero -| (succ n) i h := or.elim (eq_or_lt_of_le h) - (λ ieqn : i = n, by rewrite [ieqn, upto_succ]; exact !mem_cons) - (λ iltn : i < n, mem_upto_succ_of_mem_upto (mem_upto_of_lt iltn)) +| (succ n) i h := +begin + cases h with m h', + { rewrite upto_succ, apply mem_cons}, + { exact mem_upto_succ_of_mem_upto (mem_upto_of_lt h')} +end /- union -/ section union diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 2e3ff1ff3..2d52cca09 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -36,7 +36,7 @@ namespace nat definition not_bex_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : ¬ bex (succ n) P := λ H, obtain (w : nat) (Hw : w < succ n ∧ P w), from H, - and.rec_on Hw (λ hltsn hp, or.rec_on (eq_or_lt_of_le hltsn) + and.rec_on Hw (λ hltsn hp, or.rec_on (eq_or_lt_of_le (le_of_succ_le_succ hltsn)) (λ heq : w = n, absurd (eq.rec_on heq hp) H₂) (λ hltn : w < n, absurd (exists.intro w (and.intro hltn hp)) H₁)) @@ -47,7 +47,7 @@ namespace nat λ x Hlt, H x (lt.step Hlt) definition ball_succ_of_ball {n : nat} {P : nat → Prop} (H₁ : ball n P) (H₂ : P n) : ball (succ n) P := - λ (x : nat) (Hlt : x < succ n), or.elim (eq_or_lt_of_le Hlt) + λ (x : nat) (Hlt : x < succ n), or.elim (eq_or_lt_of_le (le_of_succ_le_succ Hlt)) (λ heq : x = n, eq.rec_on (eq.rec_on heq rfl) H₂) (λ hlt : x < n, H₁ x hlt) diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean index 5f155d919..8100a0f15 100644 --- a/library/data/nat/choose.lean +++ b/library/data/nat/choose.lean @@ -24,7 +24,7 @@ private lemma lbp_zero : lbp 0 := private lemma lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) := λ lx npx y yltsx, - or.elim (eq_or_lt_of_le yltsx) + or.elim (eq_or_lt_of_le (le_of_succ_le_succ yltsx)) (λ yeqx, by substvars; assumption) (λ yltx, lx y yltx) @@ -46,7 +46,7 @@ acc.intro x (λ (y : nat) (l : y ≺ x), by_cases (λ yeqx : y = succ x, by substvars; assumption) (λ ynex : y ≠ succ x, - have ygtsx : succ x < y, from lt_of_le_and_ne (succ_lt_succ ygtx) (ne.symm ynex), + have ygtsx : succ x < y, from lt_of_le_and_ne ygtx (ne.symm ynex), acc.inv h (and.intro ygtsx (and.elim_right l)))) private lemma acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y := @@ -61,7 +61,7 @@ private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gt assert ax : acc gtb x, from acc_of_acc_succ asx, by_cases (λ yeqx : y = x, by substvars; assumption) - (λ ynex : y ≠ x, acc_of_acc_of_lt ax (lt_of_le_and_ne yltsx ynex)) + (λ ynex : y ≠ x, acc_of_acc_of_lt ax (lt_of_le_and_ne (le_of_lt_succ yltsx) ynex)) parameter (ex : ∃ a, p a) parameter [dp : decidable_pred p] diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index e3a476c55..0b03ca7a2 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -442,7 +442,7 @@ have H3 : m * k < (succ (n div k)) * k, from ... = n div k * k + n mod k : eq_div_mul_add_mod ... < n div k * k + k : add_lt_add_left (!mod_lt H1) ... = (succ (n div k)) * k : succ_mul, -lt_of_mul_lt_mul_right H3 +le_of_lt_succ (lt_of_mul_lt_mul_right H3) theorem le_div_iff_mul_le {m n k : ℕ} (H : k > 0) : m ≤ n div k ↔ m * k ≤ n := iff.intro !mul_le_of_le_div (!le_div_of_mul_le H) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 4f81d6e8c..5ccf6a484 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -15,12 +15,6 @@ namespace nat theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n := or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl) -theorem lt.by_cases {a b : ℕ} {P : Prop} - (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := -or.elim !lt.trichotomy - (assume H, H1 H) - (assume H, or.elim H (assume H', H2 H') (assume H', H3 H')) - 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) @@ -55,15 +49,8 @@ theorem le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m := h ▸ le_add_right n k theorem le.elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m := -le.rec_on h - (exists.intro 0 rfl) - (λ m (h : n < m), lt.rec_on h - (exists.intro 1 rfl) - (λ b hlt (ih : ∃ (k : ℕ), n + k = b), - obtain (k : ℕ) (h : n + k = b), from ih, - exists.intro (succ k) (calc - n + succ k = succ (n + k) : add_succ - ... = succ b : h))) +by induction h with m h ih;existsi 0; reflexivity; + cases ih with k H; existsi succ k; exact congr_arg succ H theorem le.total {m n : ℕ} : m ≤ n ∨ n ≤ m := lt.by_cases @@ -124,25 +111,6 @@ lt_of_lt_of_le H2 H3 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 -theorem le.antisymm {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 : add.assoc - ... = m + l : by subst m - ... = n : by subst n - ... = n + 0 : add_zero), -assert L2 : k = 0, from eq_zero_of_add_eq_zero_right L1, -calc - n = n + 0 : add_zero -... = n + k : by subst k -... = m : Hk - -theorem zero_le (n : ℕ) : 0 ≤ n := -le.intro !zero_add - /- nat is an instance of a linearly ordered semiring -/ section migrate_algebra @@ -237,17 +205,6 @@ eq_zero_of_add_eq_zero_right Hk theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n := iff.intro succ_le_of_lt lt_of_succ_le -theorem not_succ_le_zero (n : ℕ) : ¬ succ n ≤ 0 := -(assume H : succ n ≤ 0, - have H2 : succ n = 0, from eq_zero_of_le_zero H, - absurd H2 !succ_ne_zero) - -theorem succ_le_succ {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := -!add_one ▸ !add_one ▸ add_le_add_right H 1 - -theorem le_of_succ_le_succ {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := -le_of_add_le_add_right (by rewrite -add_one at H; assumption) - theorem self_le_succ (n : ℕ) : n ≤ succ n := le.intro !add_one @@ -256,14 +213,6 @@ 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) -theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m := -nat.cases_on n - (assume H : pred 0 ≤ m, !zero_le) - (take n', - assume H : pred (succ n') ≤ m, - have H1 : n' ≤ m, from pred_succ n' ▸ H, - succ_le_succ H1) - 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) diff --git a/library/data/nat/sqrt.lean b/library/data/nat/sqrt.lean index 8b89ba832..4632a9595 100644 --- a/library/data/nat/sqrt.lean +++ b/library/data/nat/sqrt.lean @@ -34,7 +34,7 @@ theorem sqrt_aux_lower : ∀ {s n : nat}, s ≤ n → sqrt_aux s n * sqrt_aux s | (succ s) n h := by_cases (λ h₁ : (succ s)*(succ s) ≤ n, by rewrite [sqrt_aux_succ_of_pos h₁]; exact h₁) (λ h₂ : ¬ (succ s)*(succ s) ≤ n, - assert aux : s ≤ n, from lt.step (lt_of_succ_le h), + assert aux : s ≤ n, from le_of_succ_le h, by rewrite [sqrt_aux_succ_of_neg h₂]; exact (sqrt_aux_lower aux)) theorem sqrt_lower (n : nat) : sqrt n * sqrt n ≤ n := @@ -47,7 +47,7 @@ theorem sqrt_aux_upper : ∀ {s n : nat}, n ≤ s*s + s + s → n ≤ sqrt_aux s by rewrite [sqrt_aux_succ_of_pos h₁]; exact h) (λ h₂ : ¬ (succ s)*(succ s) ≤ n, assert h₃ : n < (succ s) * (succ s), from lt_of_not_ge h₂, - assert h₄ : n ≤ s * s + s + s, by rewrite [succ_mul_succ_eq at h₃]; exact h₃, + assert h₄ : n ≤ s * s + s + s, by rewrite [succ_mul_succ_eq at h₃]; exact le_of_lt_succ h₃, by rewrite [sqrt_aux_succ_of_neg h₂]; exact (sqrt_aux_upper h₄)) theorem sqrt_upper (n : nat) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n := @@ -68,7 +68,7 @@ theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n | (succ s) h₂ := by_cases (λ hl : (succ s)*(succ s) ≤ n*n + k, have l₁ : n*n + k ≤ n*n + n + n, from by rewrite [add.assoc]; exact (add_le_add_left h₁ (n*n)), - assert l₂ : n*n + k < n*n + n + n + 1, from l₁, + assert l₂ : n*n + k < n*n + n + n + 1, from lt_succ_of_le l₁, have l₃ : n*n + k < (succ n)*(succ n), by rewrite [-succ_mul_succ_eq at l₂]; exact l₂, assert l₄ : (succ s)*(succ s) < (succ n)*(succ n), from lt_of_le_of_lt hl l₃, have ng : ¬ succ s > (succ n), from @@ -79,7 +79,7 @@ theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n have ssnesn : succ s ≠ succ n, from assume sseqsn : succ s = succ n, by rewrite [sseqsn at l₄]; exact (absurd l₄ !lt.irrefl), - have sslen : succ s ≤ n, from lt_of_le_and_ne sslesn ssnesn, + have sslen : s < n, from lt_of_succ_lt_succ (lt_of_le_and_ne sslesn ssnesn), assert sseqn : succ s = n, from le.antisymm sslen h₂, by rewrite [sqrt_aux_succ_of_pos hl]; exact sseqn) (λ hg : ¬ (succ s)*(succ s) ≤ n*n + k, @@ -88,8 +88,8 @@ theorem sqrt_aux_offset_eq {n k : nat} (h₁ : k ≤ n + n) : ∀ {s}, s ≥ n have p : n*n ≤ n*n + k, from !le_add_right, have n : ¬ n*n ≤ n*n + k, by rewrite [-neqss at hg]; exact hg, absurd p n) - (λ sgen : s ≥ n, - by rewrite [sqrt_aux_succ_of_neg hg]; exact (sqrt_aux_offset_eq sgen))) + (λ sgen : succ s > n, + by rewrite [sqrt_aux_succ_of_neg hg]; exact (sqrt_aux_offset_eq (le_of_lt_succ sgen)))) theorem sqrt_offset_eq {n k : nat} : k ≤ n + n → sqrt (n*n + k) = n := assume h, diff --git a/library/init/nat.lean b/library/init/nat.lean index 122ee193b..89357b937 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -6,25 +6,43 @@ Authors: Floris van Doorn, Leonardo de Moura prelude import init.wf init.tactic init.num -open eq.ops decidable +open eq.ops decidable or namespace nat notation `ℕ` := nat - inductive lt (a : nat) : nat → Prop := - | base : lt a (succ a) - | step : Π {b}, lt a b → lt a (succ b) + /- basic definitions on natural numbers -/ + inductive le (a : ℕ) : ℕ → Prop := + | refl : le a a + | step : Π {b}, le a b → le a (succ b) - notation a < b := lt a b + infix `≤` := le + attribute le.refl [refl] - definition le [reducible] (a b : nat) : Prop := a < succ b + definition lt [reducible] (n m : ℕ) := succ n ≤ m + definition ge [reducible] (n m : ℕ) := m ≤ n + definition gt [reducible] (n m : ℕ) := succ m ≤ n + infix `<` := lt + infix `≥` := ge + infix `>` := gt - notation a <= b := le a b - notation a ≤ b := le a b - - definition pred (a : nat) : nat := + definition pred [unfold-c 1] (a : nat) : nat := nat.cases_on a zero (λ a₁, a₁) + -- add is defined in init.num + + definition sub (a b : nat) : nat := + nat.rec_on b a (λ b₁ r, pred r) + + definition mul (a b : nat) : nat := + nat.rec_on b zero (λ b₁ r, r + a) + + notation a - b := sub a b + notation a * b := mul a b + + + /- properties of ℕ -/ + protected definition is_inhabited [instance] : inhabited nat := inhabited.mk zero @@ -35,27 +53,242 @@ namespace nat | has_decidable_eq (succ x) (succ y) := match has_decidable_eq x y with | inl xeqy := inl (by rewrite xeqy) - | inr xney := inr (by intro h; injection h; contradiction) + | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney) end + /- properties of inequality -/ + + theorem le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := p ▸ le.refl n + + theorem le_succ (n : ℕ) : n ≤ succ n := by repeat constructor + + theorem pred_le (n : ℕ) : pred n ≤ n := by cases n;all_goals (repeat constructor) + + theorem le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := + by induction H2 with n H2 IH;exact H1;exact le.step IH + + theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ + + theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := le.trans !le_succ H + + theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H + + theorem succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := + by induction H;reflexivity;exact le.step v_0 + + theorem pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := + by induction H;reflexivity;cases b;exact v_0;exact le.step v_0 + + theorem le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := + pred_le_pred H + + theorem le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := + by cases n;exact le.step H;exact succ_le_succ H + + theorem not_succ_le_self {n : ℕ} : ¬succ n ≤ n := + by induction n with n IH;all_goals intros;cases a;apply IH;exact le_of_succ_le_succ a + + theorem zero_le (n : ℕ) : 0 ≤ n := + by induction n with n IH;apply le.refl;exact le.step IH + + theorem lt.step {n m : ℕ} (H : n < m) : n < succ m := + le.step H + + theorem zero_lt_succ (n : ℕ) : 0 < succ n := + by induction n with n IH;apply le.refl;exact le.step IH + + theorem lt.trans [trans] {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k := + le.trans (le.step H1) H2 + + theorem lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) (H2 : m < k) : n < k := + le.trans (succ_le_succ H1) H2 + + theorem lt_of_lt_of_le [trans] {n m k : ℕ} (H1 : n < m) (H2 : m ≤ k) : n < k := + le.trans H1 H2 + + theorem le.antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := + begin + cases H1 with m' H1', + { reflexivity}, + { cases H2 with n' H2', + { reflexivity}, + { exfalso, apply not_succ_le_self, exact lt.trans H1' H2'}}, + end + + theorem not_succ_le_zero (n : ℕ) : ¬succ n ≤ zero := + by intro H; cases H + + theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self + + theorem self_lt_succ (n : ℕ) : n < succ n := !le.refl + theorem lt.base (n : ℕ) : n < succ n := !le.refl + + theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : false := + !lt.irrefl (lt_of_le_of_lt H1 H2) + + theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : false := + le_lt_antisymm H2 H1 + + theorem lt.asymm {n m : ℕ} (H1 : n < m) (H2 : m < n) : false := + le_lt_antisymm (le_of_lt H1) H2 + + definition lt.by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P := + begin + revert b H1 H2 H3, induction a with a IH, + { intros, cases b, + exact H2 rfl, + exact H1 !zero_lt_succ}, + { intros, cases b with b, + exact H3 !zero_lt_succ, + { apply IH, + intro H, exact H1 (succ_le_succ H), + intro H, exact H2 (congr rfl H), + intro H, exact H3 (succ_le_succ H)}} + end + + theorem lt.trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a := + lt.by_cases (λH, inl H) (λH, inr (inl H)) (λH, inr (inr H)) + + definition lt_ge_by_cases {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a ≥ b → P) : P := + lt.by_cases H1 (λH, H2 (le_of_eq H⁻¹)) (λH, H2 (le_of_lt H)) + + theorem lt_or_ge (a b : ℕ) : (a < b) ∨ (a ≥ b) := + lt_ge_by_cases inl inr + + definition not_lt_zero (a : ℕ) : ¬ a < zero := + by intro H; cases H + -- less-than is well-founded - theorem lt.wf [instance] : well_founded lt := - well_founded.intro (λn, nat.rec_on n - (acc.intro zero (λ (y : nat) (hlt : y < zero), - have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from - λ n₁ hlt, nat.lt.cases_on hlt - (by contradiction) - (by contradiction), - aux hlt rfl)) - (λ (n : nat) (ih : acc lt n), - acc.intro (succ n) (λ (m : nat) (hlt : m < succ n), - have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from - λ n₁ hlt, nat.lt.cases_on hlt - (λ (sn_eq_sm : succ n = succ m), - by injection sn_eq_sm with neqm; rewrite neqm at ih; exact ih) - (λ b (hlt : m < b) (sn_eq_sb : succ n = succ b), - by injection sn_eq_sb with neqb; rewrite neqb at ih; exact acc.inv ih hlt), - aux hlt rfl))) + definition lt.wf [instance] : well_founded lt := + begin + constructor, intro n, induction n with n IH, + { constructor, intros n H, exfalso, exact !not_lt_zero H}, + { constructor, intros m H, + assert aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, + { intros n₁ hlt, induction hlt, + { intro p, injection p with q, exact q ▸ IH}, + { intro p, injection p with q, exact (acc.inv (q ▸ IH) a)}}, + apply aux H rfl}, + end + + definition measure {A : Type} (f : A → ℕ) : A → A → Prop := + inv_image lt f + + definition measure.wf {A : Type} (f : A → ℕ) : well_founded (measure f) := + inv_image.wf f lt.wf + + theorem succ_lt_succ {a b : ℕ} (H : a < b) : succ a < succ b := + succ_le_succ H + + theorem lt_of_succ_lt {a b : ℕ} (H : succ a < b) : a < b := + le_of_succ_le H + + theorem lt_of_succ_lt_succ {a b : ℕ} (H : succ a < succ b) : a < b := + le_of_succ_le_succ H + + definition decidable_le [instance] : decidable_rel le := + begin + intros n, induction n with n IH, + { intro m, left, apply zero_le}, + { intro m, cases m with m, + { right, apply not_succ_le_zero}, + { let H := IH m, clear IH, + cases H with H H, + left, exact succ_le_succ H, + right, intro H2, exact H (le_of_succ_le_succ H2)}} + end + + definition decidable_lt [instance] : decidable_rel lt := _ + definition decidable_gt [instance] : decidable_rel gt := _ + definition decidable_ge [instance] : decidable_rel ge := _ + + theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b := + by cases H with b' H; exact inl rfl; exact inr (succ_le_succ H) + + theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b := + by cases H with H H; exact le_of_eq H; exact le_of_lt H + + theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a := + or.rec_on (lt.trichotomy a b) + (λ hlt, absurd hlt hnlt) + (λ h, h) + + theorem lt_succ_of_le {a b : ℕ} (h : a ≤ b) : a < succ b := + succ_le_succ h + + theorem lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h + + theorem succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h + + definition max (a b : ℕ) : ℕ := if a < b then b else a + definition min (a b : ℕ) : ℕ := if a < b then a else b + + theorem max_self (a : ℕ) : max a a = a := + eq.rec_on !if_t_t rfl + + theorem max_eq_right {a b : ℕ} (H : a < b) : max a b = b := + if_pos H + + theorem max_eq_left {a b : ℕ} (H : ¬ a < b) : max a b = a := + if_neg H + + theorem eq_max_right {a b : ℕ} (H : a < b) : b = max a b := + eq.rec_on (max_eq_right H) rfl + + theorem eq_max_left {a b : ℕ} (H : ¬ a < b) : a = max a b := + eq.rec_on (max_eq_left H) rfl + + 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) + + theorem le_max_right (a b : ℕ) : b ≤ max a b := + by_cases + (λ h : a < b, eq.rec_on (eq_max_right h) !le.refl) + (λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h) + (λ heq, eq.rec_on heq (eq.rec_on (eq.symm (max_self a)) !le.refl)) + (λ h : b < a, + have aux : a = max a b, from eq_max_left (lt.asymm h), + eq.rec_on aux (le_of_lt h))) + + theorem succ_sub_succ_eq_sub (a b : ℕ) : succ a - succ b = a - b := + by induction b with b IH;reflexivity; apply congr (eq.refl pred) IH + + theorem sub_eq_succ_sub_succ (a b : ℕ) : a - b = succ a - succ b := + eq.rec_on (succ_sub_succ_eq_sub a b) rfl + + theorem zero_sub_eq_zero (a : ℕ) : zero - a = zero := + nat.rec_on a + rfl + (λ a₁ (ih : zero - a₁ = zero), congr (eq.refl pred) ih) + + theorem zero_eq_zero_sub (a : ℕ) : zero = zero - a := + eq.rec_on (zero_sub_eq_zero a) rfl + + theorem sub_lt {a b : ℕ} : zero < a → zero < b → a - b < a := + have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from + λa h₁, le.rec_on h₁ + (λb h₂, le.cases_on h₂ + (lt.base zero) + (λ b₁ bpos, + eq.rec_on (sub_eq_succ_sub_succ zero b₁) + (eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero)))) + (λa₁ apos ih b h₂, le.cases_on h₂ + (lt.base a₁) + (λ b₁ bpos, + eq.rec_on (sub_eq_succ_sub_succ a₁ b₁) + (lt.trans (@ih b₁ bpos) (lt.base a₁)))), + λ h₁ h₂, aux h₁ h₂ + + theorem sub_le (a b : ℕ) : a - b ≤ a := + nat.rec_on b + (le.refl a) + (λ b₁ ih, le.trans !pred_le ih) + +end nat + exit + definition measure {A : Type} (f : A → nat) : A → A → Prop := inv_image lt f diff --git a/tests/lean/protected_test.lean b/tests/lean/protected_test.lean index d97d0363b..20f8757de 100644 --- a/tests/lean/protected_test.lean +++ b/tests/lean/protected_test.lean @@ -2,10 +2,10 @@ namespace nat check induction_on -- ERROR check rec_on -- ERROR check nat.induction_on - check lt.rec_on -- OK - check nat.lt.rec_on - namespace lt + check le.rec_on -- OK + check nat.le.rec_on + namespace le check rec_on -- ERROR - check lt.rec_on - end lt + check le.rec_on + end le end nat diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out index fdab38648..f2ed48d97 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 -lt.rec_on : ?a < ?a_1 → ?C (succ ?a) → (∀ {b : ℕ}, ?a < b → ?C b → ?C (succ b)) → ?C ?a_1 -lt.rec_on : ?a < ?a_1 → ?C (succ ?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 : ?a ≤ ?a_1 → ?C ?a → (∀ {b : ℕ}, ?a ≤ b → ?C b → ?C (succ b)) → ?C ?a_1 protected_test.lean:8:10: error: unknown identifier 'rec_on' -lt.rec_on : ?a < ?a_1 → ?C (succ ?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 \ No newline at end of file diff --git a/tests/lean/run/541a.lean b/tests/lean/run/541a.lean index 83623adce..4cce67376 100644 --- a/tests/lean/run/541a.lean +++ b/tests/lean/run/541a.lean @@ -1,8 +1,6 @@ import data.list data.nat open nat list eq.ops -theorem nat.le_of_eq {x y : ℕ} (H : x = y) : x ≤ y := H ▸ !le.refl - section variable {Q : Type} diff --git a/tests/lean/run/constr_tac4.lean b/tests/lean/run/constr_tac4.lean index 8aa792cc6..ad18713d7 100644 --- a/tests/lean/run/constr_tac4.lean +++ b/tests/lean/run/constr_tac4.lean @@ -4,17 +4,17 @@ open nat definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c := have aux : a < b → a < c, from - lt.rec_on H₂ + le.rec_on H₂ (λ h₁, lt.step h₁) (λ b₁ bb₁ ih h₁, by constructor; exact ih h₁), aux H₁ definition succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b := -lt.rec_on H +le.rec_on H (by constructor) (λ b hlt ih, lt.trans ih (by constructor)) definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b := -lt.rec_on H +le.rec_on H (by constructor; constructor) (λ b h ih, by constructor; exact ih)