From d0c86f13bb75933d91e5c195d99f2bdc7ef1bc32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Jan 2017 17:47:49 -0800 Subject: [PATCH] chore(library/init/data/nat): rename nat.less_than to nat.less_than_or_equal as suggested by Rob --- library/init/data/nat/basic.lean | 32 ++++++++++----------- library/init/data/nat/lemmas.lean | 16 +++++------ tests/lean/protected_test.lean | 6 ++-- tests/lean/protected_test.lean.expected.out | 15 ++++++---- 4 files changed, 36 insertions(+), 33 deletions(-) diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index a2d2d7b0a3..fb6d3dbec2 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -10,15 +10,15 @@ notation `ℕ` := nat namespace nat -inductive less_than (a : ℕ) : ℕ → Prop -| refl : less_than a -| step : Π {b}, less_than b → less_than (succ b) +inductive less_than_or_equal (a : ℕ) : ℕ → Prop +| refl : less_than_or_equal a +| step : Π {b}, less_than_or_equal b → less_than_or_equal (succ b) instance : has_le ℕ := -⟨nat.less_than⟩ +⟨nat.less_than_or_equal⟩ -@[reducible] protected def le (n m : ℕ) := nat.less_than n m -@[reducible] protected def lt (n m : ℕ) := nat.less_than (succ n) m +@[reducible] protected def le (n m : ℕ) := nat.less_than_or_equal n m +@[reducible] protected def lt (n m : ℕ) := nat.less_than_or_equal (succ n) m instance : has_lt ℕ := ⟨nat.lt⟩ @@ -64,17 +64,17 @@ rfl /- properties of inequality -/ @[refl] protected def le_refl : ∀ a : ℕ, a ≤ a := -less_than.refl +less_than_or_equal.refl lemma le_succ (n : ℕ) : n ≤ succ n := -less_than.step (nat.le_refl n) +less_than_or_equal.step (nat.le_refl n) lemma succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := -λ h, less_than.rec (nat.le_refl (succ n)) (λ a b, less_than.step) h +λ h, less_than_or_equal.rec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h lemma zero_le : ∀ (n : ℕ), 0 ≤ n | 0 := nat.le_refl 0 -| (n+1) := less_than.step (zero_le n) +| (n+1) := less_than_or_equal.step (zero_le n) lemma zero_lt_succ (n : ℕ) : 0 < succ n := succ_le_succ (zero_le n) @@ -87,9 +87,9 @@ lemma not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false lemma not_lt_zero (a : ℕ) : ¬ a < 0 := not_succ_le_zero a lemma pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m := -λ h, less_than.rec_on h +λ h, less_than_or_equal.rec_on h (nat.le_refl (pred n)) - (λ n, nat.rec (λ a b, b) (λ a b c, less_than.step) n) + (λ n, nat.rec (λ a b, b) (λ a b c, less_than_or_equal.step) n) lemma le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m := pred_le_pred @@ -107,7 +107,7 @@ instance decidable_lt : ∀ a b : ℕ, decidable (a < b) := λ a b, nat.decidable_le (succ a) b protected lemma eq_or_lt_of_le {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b := -less_than.cases_on h (or.inl rfl) (λ n h, or.inr (succ_le_succ h)) +less_than_or_equal.cases_on h (or.inl rfl) (λ n h, or.inr (succ_le_succ h)) lemma lt_succ_of_le {a b : ℕ} : a ≤ b → a < succ b := succ_le_succ @@ -124,11 +124,11 @@ protected lemma lt_irrefl (n : ℕ) : ¬n < n := not_succ_le_self n protected lemma le_trans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k := -less_than.rec h1 (λ p h2, less_than.step) +less_than_or_equal.rec h1 (λ p h2, less_than_or_equal.step) lemma pred_le : ∀ (n : ℕ), pred n ≤ n -| 0 := less_than.refl 0 -| (succ a) := less_than.step (less_than.refl a) +| 0 := less_than_or_equal.refl 0 +| (succ a) := less_than_or_equal.step (less_than_or_equal.refl a) lemma sub_le (a b : ℕ) : a - b ≤ a := nat.rec_on b (nat.le_refl (a - 0)) (λ b₁, nat.le_trans (pred_le (a - b₁))) diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index ae1a88b314..97270240bd 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -156,7 +156,7 @@ instance : comm_semiring nat := /- properties of inequality -/ protected lemma le_of_eq {n m : ℕ} (p : n = m) : n ≤ m := -p ▸ less_than.refl n +p ▸ less_than_or_equal.refl n lemma le_succ_iff_true (n : ℕ) : n ≤ succ n ↔ true := iff_true_intro (le_succ n) @@ -174,7 +174,7 @@ protected lemma le_of_lt {n m : ℕ} (h : n < m) : n ≤ m := le_of_succ_le h lemma le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m := -nat.cases_on n less_than.step (λ a, succ_le_succ) +nat.cases_on n less_than_or_equal.step (λ a, succ_le_succ) lemma succ_le_zero_iff_false (n : ℕ) : succ n ≤ 0 ↔ false := iff_false_intro (not_succ_le_zero n) @@ -185,7 +185,7 @@ iff_false_intro (not_succ_le_self n) lemma zero_le_iff_true (n : ℕ) : 0 ≤ n ↔ true := iff_true_intro (zero_le n) -def lt.step {n m : ℕ} : n < m → n < succ m := less_than.step +def lt.step {n m : ℕ} : n < m → n < succ m := less_than_or_equal.step lemma zero_lt_succ_iff_true (n : ℕ) : 0 < succ n ↔ true := iff_true_intro (zero_lt_succ n) @@ -196,7 +196,7 @@ protected lemma pos_of_ne_zero {n : nat} (h : n ≠ 0) : n > 0 := begin cases n, contradiction, apply succ_pos end protected lemma lt_trans {n m k : ℕ} (h₁ : n < m) : m < k → n < k := -nat.le_trans (less_than.step h₁) +nat.le_trans (less_than_or_equal.step h₁) protected lemma lt_of_le_of_lt {n m k : ℕ} (h₁ : n ≤ m) : m < k → n < k := nat.le_trans (succ_le_succ h₁) @@ -219,10 +219,10 @@ lemma le_lt_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) : false := nat.lt_irrefl n (nat.lt_of_le_of_lt h₁ h₂) protected lemma le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m := -less_than.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n)) +less_than_or_equal.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n)) instance : weak_order ℕ := -⟨@nat.less_than, @nat.le_refl, @nat.le_trans, @nat.le_antisymm⟩ +⟨@nat.less_than_or_equal, @nat.le_refl, @nat.le_trans, @nat.le_antisymm⟩ lemma lt_le_antisymm {n m : ℕ} (h₁ : n < m) (h₂ : m ≤ n) : false := le_lt_antisymm h₂ h₁ @@ -285,8 +285,8 @@ lemma le_add_left (n m : ℕ): n ≤ m + n := nat.add_comm n m ▸ le_add_right n m lemma le.dest : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m -| n .n (less_than.refl .n) := ⟨0, rfl⟩ -| n .(succ m) (@less_than.step .n m h) := +| n .n (less_than_or_equal.refl .n) := ⟨0, rfl⟩ +| n .(succ m) (@less_than_or_equal.step .n m h) := match le.dest h with | ⟨w, hw⟩ := ⟨succ w, hw ▸ add_succ n w⟩ end diff --git a/tests/lean/protected_test.lean b/tests/lean/protected_test.lean index e7e93c0c8e..cf50ccde18 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 less_than.rec_on -- OK - check nat.less_than.rec_on + check less_than_or_equal.rec_on -- OK + check nat.less_than_or_equal.rec_on namespace le check rec_on -- ERROR - check less_than.rec_on + check less_than_or_equal.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 a6bb326453..88459e2aa0 100644 --- a/tests/lean/protected_test.lean.expected.out +++ b/tests/lean/protected_test.lean.expected.out @@ -1,10 +1,13 @@ protected_test.lean:2:8: error: unknown identifier 'induction_on' protected_test.lean:3:8: error: unknown identifier 'rec_on' nat.induction_on : ∀ (n : ℕ), ?M_1 0 → (∀ (a : ℕ), ?M_1 a → ?M_1 (succ a)) → ?M_1 n -less_than.rec_on : - less_than ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, less_than ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 -less_than.rec_on : - less_than ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, less_than ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 +less_than_or_equal.rec_on : + less_than_or_equal ?M_1 ?M_3 → + ?M_2 ?M_1 → (∀ {b : ℕ}, less_than_or_equal ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 +less_than_or_equal.rec_on : + less_than_or_equal ?M_1 ?M_3 → + ?M_2 ?M_1 → (∀ {b : ℕ}, less_than_or_equal ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 protected_test.lean:8:10: error: unknown identifier 'rec_on' -less_than.rec_on : - less_than ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, less_than ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 +less_than_or_equal.rec_on : + less_than_or_equal ?M_1 ?M_3 → + ?M_2 ?M_1 → (∀ {b : ℕ}, less_than_or_equal ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3