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

@@ -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₁)))

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

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

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