refactor(library/nat): rename nat.le to nat.less_than

Motivation: avoid overload when we use `open nat`.

Unfortunately, we currently do not allow users to mark inductive datatype
declarations as protected.

library/init/nat.lean

@@ -11,13 +11,14 @@ notation `ℕ` := nat
 
 namespace nat
 
-inductive le (a : ℕ) : ℕ → Prop
-| nat_refl : le a    -- use nat_refl to avoid overloading le.refl
-| step : Π {b}, le b → le (succ b)
+inductive less_than (a : ℕ) : ℕ → Prop
+| refl : less_than a
+| step : Π {b}, less_than b → less_than (succ b)
 
 instance : has_le ℕ :=
-⟨nat.le⟩
+⟨nat.less_than⟩
 
+@[reducible] protected def le (n m : ℕ) := n ≤ m
 @[reducible] protected def lt (n m : ℕ) := succ n ≤ m
 
 instance : has_lt ℕ :=
@@ -61,17 +62,17 @@ instance : inhabited ℕ :=
 /- properties of inequality -/
 
 @[refl] protected def le_refl : ∀ a : ℕ, a ≤ a :=
-le.nat_refl
+less_than.refl
 
 lemma le_succ (n : ℕ) : n ≤ succ n :=
-le.step (nat.le_refl n)
+less_than.step (nat.le_refl n)
 
 lemma succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
-λ h, le.rec (nat.le_refl (succ n)) (λ a b, le.step) h
+λ h, less_than.rec (nat.le_refl (succ n)) (λ a b, less_than.step) h
 
 lemma zero_le : ∀ (n : ℕ), 0 ≤ n
 | 0     := nat.le_refl 0
-| (n+1) := le.step (zero_le n)
+| (n+1) := less_than.step (zero_le n)
 
 lemma zero_lt_succ (n : ℕ) : 0 < succ n :=
 succ_le_succ (zero_le n)
@@ -82,7 +83,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, le.rec (nat.le_refl (pred n)) (λ n, nat.rec (λ a b, b) (λ a b c, le.step) n) h
+λ h, less_than.rec_on h
+  (nat.le_refl (pred n))
+  (λ n, nat.rec (λ a b, b) (λ a b c, less_than.step) n)
 
 lemma le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m :=
 pred_le_pred
@@ -100,7 +103,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 :=
-le.cases_on h (or.inl rfl) (λ n h, or.inr (succ_le_succ h))
+less_than.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
@@ -117,11 +120,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 :=
-le.rec h1 (λ p h2, le.step)
+less_than.rec h1 (λ p h2, less_than.step)
 
 lemma pred_le : ∀ (n : ℕ), pred n ≤ n
-| 0        := le.nat_refl 0
-| (succ a) := le.step (le.nat_refl a)
+| 0        := less_than.refl 0
+| (succ a) := less_than.step (less_than.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/nat_lemmas.lean

@@ -155,7 +155,7 @@ instance : comm_semiring nat :=
 /- properties of inequality -/
 
 protected lemma le_of_eq {n m : ℕ} (p : n = m) : n ≤ m :=
-p ▸ le.nat_refl n
+p ▸ less_than.refl n
 
 lemma le_succ_iff_true (n : ℕ) : n ≤ succ n ↔ true :=
 iff_true_intro (le_succ n)
@@ -173,7 +173,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 le.step (λ a, succ_le_succ)
+nat.cases_on n less_than.step (λ a, succ_le_succ)
 
 lemma succ_le_zero_iff_false (n : ℕ) : succ n ≤ 0 ↔ false :=
 iff_false_intro (not_succ_le_zero n)
@@ -184,13 +184,13 @@ 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 := le.step
+def lt.step {n m : ℕ} : n < m → n < succ m := less_than.step
 
 lemma zero_lt_succ_iff_true (n : ℕ) : 0 < succ n ↔ true :=
 iff_true_intro (zero_lt_succ n)
 
 protected lemma lt_trans {n m k : ℕ} (h₁ : n < m) : m < k → n < k :=
-nat.le_trans (le.step h₁)
+nat.le_trans (less_than.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₁)
@@ -209,10 +209,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 :=
-le.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n))
+less_than.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.le, @nat.le_refl, @nat.le_trans, @nat.le_antisymm ⟩
+⟨@nat.less_than, @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₁
@@ -275,8 +275,8 @@ lemma le_add_left (n m : ℕ): n ≤ m + n :=
 nat.add_comm n m ▸ le_add_right n m
 
 lemma le.elim : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m
-| n .n        (le.nat_refl .n)  := ⟨0, rfl⟩
-| n .(succ m) (@le.step .n m h) :=
+| n .n        (less_than.refl .n)  := ⟨0, rfl⟩
+| n .(succ m) (@less_than.step .n m h) :=
   match le.elim h with
   | ⟨w, hw⟩ := ⟨succ w, hw ▸ add_succ n w⟩
   end

tests/lean/concrete_instance.lean

@@ -5,8 +5,8 @@ set_option pp.all true
 check a * b
 check a + b
 
-instance : semigroup nat := sorry
-instance : add_semigroup nat := sorry
+-- instance : semigroup nat := sorry
+-- instance : add_semigroup nat := sorry
 
 check a * b
 check a + b

tests/lean/concrete_instance.lean.expected.out

@@ -1,8 +1,4 @@
 @mul.{1} nat nat.has_mul a b : nat
 @add.{1} nat nat.has_add a b : nat
-concrete_instance.lean:8:9: warning: failed to generate bytecode for 'nat.semigroup'
-code generation failed, VM does not have code for 'sorry'
-concrete_instance.lean:9:9: warning: failed to generate bytecode for 'nat.add_semigroup'
-code generation failed, VM does not have code for 'sorry'
 @mul.{1} nat nat.has_mul a b : nat
 @add.{1} nat nat.has_add a b : nat

tests/lean/protected_test.lean

@@ -2,10 +2,10 @@ namespace nat
   check induction_on      -- ERROR
   check rec_on            -- ERROR
   check nat.induction_on
-  check le.rec_on         -- OK
-  check nat.le.rec_on
+  check less_than.rec_on         -- OK
+  check nat.less_than.rec_on
   namespace le
     check rec_on          -- ERROR
-    check le.rec_on
+    check less_than.rec_on
   end le
 end nat

tests/lean/protected_test.lean.expected.out

@@ -1,7 +1,10 @@
 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
-le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3
-le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, le ?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.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
 protected_test.lean:8:10: error: unknown identifier 'rec_on'
-le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, le ?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