Revert 'chore(library/init/data/nat): backport Nat.le from Lean4 (#603)'

library/init/data/nat/basic.lean

@@ -10,18 +10,15 @@ notation `ℕ` := nat
 
 namespace nat
 
-protected def ble : ℕ → ℕ → bool
-| 0     0     := tt
-| 0     (m+1) := tt
-| (n+1) 0     := ff
-| (n+1) (m+1) := ble n m
-
-protected def le (n m : ℕ) : Prop := nat.ble n m = true
-
-@[reducible] protected def lt (n m : ℕ) := nat.le (succ n) m
+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.le⟩
+⟨nat.less_than_or_equal⟩
+
+@[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⟩
@@ -70,20 +67,18 @@ rfl
 
 /- properties of inequality -/
 
-@[refl] protected lemma le_refl : ∀ n : ℕ, n ≤ n
-| 0     := rfl
-| (n+1) := le_refl n
+@[refl] protected lemma le_refl (a : ℕ) : a ≤ a :=
+less_than_or_equal.refl
 
-lemma le_succ : ∀ n : ℕ, n ≤ succ n
-| 0     := rfl
-| (n+1) := le_succ n
+lemma le_succ (n : ℕ) : n ≤ succ n :=
+less_than_or_equal.step (nat.le_refl n)
 
 lemma succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
-λ h, h
+λ h, less_than_or_equal.rec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h
 
 protected lemma zero_le : ∀ (n : ℕ), 0 ≤ n
-| 0     := rfl
-| (n+1) := rfl
+| 0     := nat.le_refl 0
+| (n+1) := less_than_or_equal.step (zero_le n)
 
 lemma zero_lt_succ (n : ℕ) : 0 < succ n :=
 succ_le_succ n.zero_le
@@ -95,11 +90,10 @@ lemma not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false
 
 protected lemma not_lt_zero (a : ℕ) : ¬ a < 0 := not_succ_le_zero a
 
-lemma pred_le_pred : ∀ {n m : ℕ}, n ≤ m → pred n ≤ pred m
-| 0     0     h := rfl
-| 0     1     h := rfl
-| 0     (m+2) h := rfl
-| (n+1) (m+1) h := h
+lemma pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
+λ h, less_than_or_equal.rec_on h
+  (nat.le_refl (pred 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
@@ -116,16 +110,8 @@ instance decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
 instance decidable_lt : ∀ a b : ℕ, decidable (a < b) :=
 λ a b, nat.decidable_le (succ a) b
 
-lemma succ_lt_succ {n m : ℕ} : n < m → succ n < succ m :=
-λ h, h
-
-protected lemma eq_or_lt_of_le : ∀ {a b : ℕ} (h : a ≤ b), a = b ∨ a < b
-| 0     0     h := or.inl rfl
-| 0     (b+1) h := or.inr (zero_lt_succ b)
-| (a+1) (b+1) h := match @eq_or_lt_of_le a b h with
-  | or.inl w := or.inl (congr_arg nat.succ w)
-  | or.inr w := or.inr (succ_lt_succ w)
-  end
+protected lemma eq_or_lt_of_le {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b :=
+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
@@ -141,28 +127,16 @@ lemma not_succ_le_self : ∀ n : ℕ, ¬succ n ≤ n :=
 protected lemma lt_irrefl (n : ℕ) : ¬n < n :=
 not_succ_le_self n
 
-protected lemma le_trans : ∀ {n m k : ℕ}, n ≤ m → m ≤ k → n ≤ k
-| 0     0     0     _ _ := rfl
-| 0     0     (k+1) _ _ := rfl
-| 0     (m+1) (k+1) _ _ := rfl
-| (n+1) (m+1) (k+1) h₁ h₂ := @le_trans n m k h₁ h₂
+protected lemma le_trans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k :=
+less_than_or_equal.rec h1 (λ p h2, less_than_or_equal.step)
 
 lemma pred_le : ∀ (n : ℕ), pred n ≤ n
-| 0     := rfl
-| 1     := rfl
-| (n+2) := pred_le (n+1)
-
-protected lemma eq_zero_of_le_zero : ∀ {n : ℕ}, n ≤ 0 → n = 0
-| 0 _ := rfl
-
-lemma le_zero_iff {n : ℕ} : n ≤ 0 ↔ n = 0 :=
-⟨λ h, nat.eq_zero_of_le_zero h, λ h, h ▸ nat.le_refl n⟩
-
-attribute [irreducible] nat.le
+| 0        := less_than_or_equal.refl
+| (succ a) := less_than_or_equal.step less_than_or_equal.refl
 
 lemma pred_lt : ∀ {n : ℕ}, n ≠ 0 → pred n < n
 | 0        h := absurd rfl h
-| (succ a) h := lt_succ_of_le (nat.le_refl _)
+| (succ a) h := lt_succ_of_le less_than_or_equal.refl
 
 protected 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/bitwise.lean

@@ -168,7 +168,6 @@ lemma shiftr_add (m n) : ∀ k, shiftr m (n + k) = shiftr (shiftr m n) k
 
 lemma shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = shiftr (shiftl' b m n) k
 | n     0     h := rfl
-| 0     (k+1) h := by cases nat.not_succ_le_zero _ h
 | (n+1) (k+1) h := begin
   simp [shiftl'], rw [nat.add_comm, shiftr_add],
   simp [shiftr, div2_bit],

library/init/data/nat/lemmas.lean

@@ -114,7 +114,7 @@ by rw [nat.mul_comm, nat.mul_one]
 /- properties of inequality -/
 
 protected lemma le_of_eq {n m : ℕ} (p : n = m) : n ≤ m :=
-p ▸ nat.le_refl n
+p ▸ less_than_or_equal.refl
 
 lemma le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
 nat.le_trans h (le_succ m)
@@ -125,8 +125,7 @@ nat.le_trans (le_succ n) h
 protected lemma le_of_lt {n m : ℕ} (h : n < m) : n ≤ m :=
 le_of_succ_le h
 
-lemma lt.step {n m : ℕ} : n < m → n < succ m :=
-λ h, nat.le_trans h (le_succ _)
+lemma lt.step {n m : ℕ} : n < m → n < succ m := less_than_or_equal.step
 
 protected lemma eq_zero_or_pos (n : ℕ) : n = 0 ∨ 0 < n :=
 by {cases n, exact or.inl rfl, exact or.inr (succ_pos _)}
@@ -135,7 +134,7 @@ protected lemma pos_of_ne_zero {n : nat} : n ≠ 0 → 0 < n :=
 or.resolve_left n.eq_zero_or_pos
 
 protected lemma lt_trans {n m k : ℕ} (h₁ : n < m) : m < k → n < k :=
-nat.le_trans h₁.step
+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₁)
@@ -144,12 +143,8 @@ lemma lt.base (n : ℕ) : n < succ n := nat.le_refl (succ n)
 
 lemma lt_succ_self (n : ℕ) : n < succ n := lt.base n
 
-protected lemma le_antisymm : ∀ {n m : ℕ}, n ≤ m → m ≤ n → n = m
-| 0     0     _  _  := rfl
-| 0     (m+1) _  h₂ := by cases nat.eq_zero_of_le_zero h₂
-| (n+1) 0     h₁ _  := by cases nat.eq_zero_of_le_zero h₁
-| (n+1) (m+1) h₁ h₂ := congr_arg nat.succ
-    (@le_antisymm n m (nat.le_of_succ_le_succ h₁) (nat.le_of_succ_le_succ h₂))
+protected lemma le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m :=
+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))
 
 protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ b ≤ a
 | a 0     := or.inr a.zero_le
@@ -174,7 +169,7 @@ protected lemma lt_iff_le_not_le {m n : ℕ} : m < n ↔ (m ≤ n ∧ ¬ n ≤ m
  λ ⟨hmn, hnm⟩, nat.lt_of_le_and_ne hmn (λ heq, hnm (heq ▸ nat.le_refl _))⟩
 
 instance : linear_order ℕ :=
-{ le := nat.le,
+{ le := nat.less_than_or_equal,
   le_refl := @nat.le_refl,
   le_trans := @nat.le_trans,
   le_antisymm := @nat.le_antisymm,
@@ -185,24 +180,18 @@ instance : linear_order ℕ :=
   decidable_le               := nat.decidable_le,
   decidable_eq               := nat.decidable_eq }
 
+protected lemma eq_zero_of_le_zero {n : nat} (h : n ≤ 0) : n = 0 :=
+le_antisymm h n.zero_le
+
+lemma succ_lt_succ {a b : ℕ} : a < b → succ a < succ b :=
+succ_le_succ
+
 lemma lt_of_succ_lt {a b : ℕ} : succ a < b → a < b :=
 le_of_succ_le
 
 lemma lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b :=
 le_of_succ_le_succ
 
-lemma lt_succ_iff_eq_or_lt {n m : ℕ} : n < m + 1 ↔ n = m ∨ n < m :=
-⟨λ h, begin
-    cases nat.eq_or_lt_of_le h with h h,
-    { left, cases h, refl, },
-    { right, exact lt_of_succ_lt_succ h, },
-  end,
- λ h, begin
-    cases h,
-    { subst h, exact lt_succ_self _, },
-    { exact lt_trans h (lt_succ_self _) },
-  end⟩
-
 lemma pred_lt_pred : ∀ {n m : ℕ}, n ≠ 0 → n < m → pred n < pred m
 | 0         _       h₁ h := absurd rfl h₁
 | n         0       h₁ h := absurd h n.not_lt_zero
@@ -212,23 +201,6 @@ lemma lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h
 
 lemma succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h
 
-lemma le_of_lt_succ {m n : nat} : m < succ n → m ≤ n :=
-le_of_succ_le_succ
-
-protected def le.induction_on {a : ℕ} {motive : Π b, a ≤ b → Sort*}
-  {b : ℕ} (k : a ≤ b) (h : motive a (le_refl a))
-  (w : ∀ {b : ℕ} (k : a ≤ b),
-    motive b k → motive (b+1) (le_trans k (nat.le_succ b))) :
-  motive b k :=
-begin
-  induction b with b ih,
-  { cases nat.le_zero_iff.mp k, assumption, },
-  { by_cases k' : a = b + 1,
-    { subst k', assumption, },
-    { exact w (nat.le_of_lt_succ ((nat.eq_or_lt_of_le k).resolve_left k'))
-        (ih _) } }
-end
-
 protected lemma le_add_right : ∀ (n k : ℕ), n ≤ n + k
 | n 0     := nat.le_refl n
 | n (k+1) := le_succ_of_le (le_add_right n k)
@@ -237,10 +209,10 @@ protected lemma le_add_left (n m : ℕ): n ≤ m + n :=
 nat.add_comm n m ▸ n.le_add_right m
 
 lemma le.dest : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m
-| 0 m h := ⟨m, nat.zero_add _⟩
-| (n+1) 0 h := by cases nat.le_zero_iff.mp h
-| (n+1) (m+1) h := match @le.dest n m (nat.le_of_succ_le_succ h) with
-  | ⟨w, hw⟩ := ⟨w, by rw [←hw, nat.add_assoc, nat.add_comm 1 w, nat.add_assoc]⟩
+| n _ less_than_or_equal.refl := ⟨0, rfl⟩
+| n _ (less_than_or_equal.step h) :=
+  match le.dest h with
+  | ⟨w, hw⟩ := ⟨succ w, hw ▸ add_succ n w⟩
   end
 
 protected lemma le.intro {n m k : ℕ} (h : n + k = m) : n ≤ m :=
@@ -326,6 +298,9 @@ not_lt.1
    have h2 : c * b < c * a, from nat.mul_lt_mul_of_pos_left h1 hc,
    not_le_of_gt h2 h)
 
+lemma le_of_lt_succ {m n : nat} : m < succ n → m ≤ n :=
+le_of_succ_le_succ
+
 protected theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : 0 < n) (H : n * m = n * k) : m = k :=
 le_antisymm (nat.le_of_mul_le_mul_left (le_of_eq H) Hn)
             (nat.le_of_mul_le_mul_left (le_of_eq H.symm) Hn)
@@ -645,10 +620,9 @@ private lemma mod_core_congr {x y f1 f2} (h1 : x ≤ f1) (h2 : x ≤ f2) :
   nat.mod_core y f1 x = nat.mod_core y f2 x :=
 begin
   cases y, { cases f1; cases f2; refl },
-  induction f1 with f1 ih generalizing x f2,
-    { cases nat.le_zero_iff.mp h1, cases f2; refl },
+  induction f1 with f1 ih generalizing x f2, { cases h1, cases f2; refl },
   cases x, { cases f1; cases f2; refl },
-  cases f2, { cases not_succ_le_zero _ h2 },
+  cases f2, { cases h2 },
   refine if_congr iff.rfl _ rfl,
   simp only [succ_sub_succ],
   exact ih
@@ -724,10 +698,9 @@ private lemma div_core_congr {x y f1 f2} (h1 : x ≤ f1) (h2 : x ≤ f2) :
   nat.div_core y f1 x = nat.div_core y f2 x :=
 begin
   cases y, { cases f1; cases f2; refl },
-  induction f1 with f1 ih generalizing x f2,
-    { cases nat.le_zero_iff.mp h1, cases f2; refl },
+  induction f1 with f1 ih generalizing x f2, { cases h1, cases f2; refl },
   cases x, { cases f1; cases f2; refl },
-  cases f2, { cases not_succ_le_zero _ h2 },
+  cases f2, { cases h2 },
   refine if_congr iff.rfl _ rfl,
   simp only [succ_sub_succ],
   refine congr_arg (+1) _,
@@ -906,7 +879,7 @@ theorem eq_zero_of_mul_eq_zero : ∀ {n m : ℕ}, n * m = 0 → n = 0 ∨ m = 0
 /- properties of inequality -/
 
 theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
-nat.cases_on n le_succ_of_le (λ a, succ_le_succ)
+nat.cases_on n less_than_or_equal.step (λ a, succ_le_succ)
 
 theorem le_lt_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) : false :=
 nat.lt_irrefl n (nat.lt_of_le_of_lt h₁ h₂)
@@ -938,11 +911,7 @@ lemma one_pos : 0 < 1 := nat.zero_lt_one
 /- subtraction -/
 
 protected theorem sub_le_sub_left {n m : ℕ} (k) (h : n ≤ m) : k - m ≤ k - n :=
-begin
-  apply nat.le.induction_on h,
-  { refl, },
-  { intros m h ih, exact le_trans (pred_le _) ih }
-end
+by induction h; [refl, exact le_trans (pred_le _) h_ih]
 
 theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k :=
 by rw [nat.sub_sub, nat.sub_sub, add_succ, succ_sub_succ]

src/library/comp_val.cpp

@@ -155,7 +155,7 @@ optional<expr> mk_is_valid_char_proof(expr const & v) {
 
 optional<expr> mk_char_val_ne_proof(expr const & a, expr const & b) {
     if (is_app_of(a, get_char_of_nat_name(), 1) &&
-        is_app_of(b, get_char_of_nat_name(), 1)) {
+        is_app_of(a, get_char_of_nat_name(), 1)) {
         expr const & v_a = app_arg(a);
         expr const & v_b = app_arg(b);
         if (auto h_1 = mk_nat_val_ne_proof(v_a, v_b)) {

tests/lean/protected_test.lean

@@ -1,7 +1,10 @@
 namespace nat
   #check induction_on      -- ERROR
   #check rec_on            -- ERROR
+  #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_or_equal.rec_on
   end le
 end nat

tests/lean/protected_test.lean.expected.out

@@ -1,3 +1,12 @@
 protected_test.lean:2:9: error: unknown identifier 'induction_on'
 protected_test.lean:3:9: error: unknown identifier 'rec_on'
-protected_test.lean:5:11: error: unknown identifier 'rec_on'
+less_than_or_equal.rec_on :
+  ?M_1.less_than_or_equal ?M_3 →
+  ?M_2 ?M_1 → (∀ {b : ℕ}, ?M_1.less_than_or_equal b → ?M_2 b → ?M_2 b.succ) → ?M_2 ?M_3
+less_than_or_equal.rec_on :
+  ?M_1.less_than_or_equal ?M_3 →
+  ?M_2 ?M_1 → (∀ {b : ℕ}, ?M_1.less_than_or_equal b → ?M_2 b → ?M_2 b.succ) → ?M_2 ?M_3
+protected_test.lean:7:11: error: unknown identifier 'rec_on'
+less_than_or_equal.rec_on :
+  ?M_1.less_than_or_equal ?M_3 →
+  ?M_2 ?M_1 → (∀ {b : ℕ}, ?M_1.less_than_or_equal b → ?M_2 b → ?M_2 b.succ) → ?M_2 ?M_3

tests/lean/run/1728.lean

@@ -19,7 +19,7 @@ instance empty_is_Finite : Finite empty := {
                  intros,
                  induction v,
                  trace_state,
-                 cases nat.not_lt_zero _ v_property,
+                 cases v_property,
                  repeat {admit}
               end
 }

tests/lean/run/empty_match.lean

@@ -1,8 +1,8 @@
 open nat
 
-definition not_false' (a : nat) : ¬ false :=
-assume H : false,
+definition not_lt_zero (a : nat) : ¬ a < 0 :=
+assume H : a < 0,
 match H with
 end
 
-#check _root_.not_false'
+#check _root_.not_lt_zero

tests/lean/run/exhaustive_vm_impl_test.lean

@@ -2,7 +2,7 @@ instance my_pow : has_pow ℕ ℕ :=
 ⟨λ x n, nat.rec_on n 1 (λ _ ih, ih * x)⟩
 
 instance nat.decidable_ball (p : ℕ → Prop) [∀ i, decidable (p i)] : ∀ n, decidable (∀ x < n, p x)
-| 0 := decidable.is_true begin intros n h, cases nat.not_lt_zero _ h end
+| 0 := decidable.is_true begin intros n h, cases h end
 | (n+1) :=
     match nat.decidable_ball n with
     | (decidable.is_false h) :=
@@ -15,16 +15,15 @@ instance nat.decidable_ball (p : ℕ → Prop) [∀ i, decidable (p i)] : ∀ n,
     | (decidable.is_true h) :=
         if h' : p n then
             decidable.is_true begin
-                intros x hx,
-                cases nat.lt_succ_iff_eq_or_lt.mp hx with h₁ h₂,
-                { exact h₁.symm ▸ h', },
-                { exact h _ h₂, },
+                intros x hx, cases hx,
+                {assumption},
+                {apply h, assumption},
             end
         else
             decidable.is_false begin
                intro hpx,
                apply h', apply hpx,
-               apply nat.lt_succ_self,
+               constructor,
             end
     end