From e9f8f9e5d784f5236bd723050ea829eed36bb969 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Nov 2016 17:52:55 -0800 Subject: [PATCH] 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 | 29 ++++++++++--------- library/init/nat_lemmas.lean | 16 +++++----- tests/lean/concrete_instance.lean | 4 +-- .../lean/concrete_instance.lean.expected.out | 4 --- tests/lean/protected_test.lean | 6 ++-- tests/lean/protected_test.lean.expected.out | 9 ++++-- 6 files changed, 35 insertions(+), 33 deletions(-) diff --git a/library/init/nat.lean b/library/init/nat.lean index 43eefee374..cc150f4113 100644 --- a/library/init/nat.lean +++ b/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₁))) diff --git a/library/init/nat_lemmas.lean b/library/init/nat_lemmas.lean index bb676267c1..6ae5fb3d61 100644 --- a/library/init/nat_lemmas.lean +++ 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 diff --git a/tests/lean/concrete_instance.lean b/tests/lean/concrete_instance.lean index cee0ce86af..75803f560d 100644 --- a/tests/lean/concrete_instance.lean +++ b/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 diff --git a/tests/lean/concrete_instance.lean.expected.out b/tests/lean/concrete_instance.lean.expected.out index d96e46aae7..12f9eed8ea 100644 --- a/tests/lean/concrete_instance.lean.expected.out +++ 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 diff --git a/tests/lean/protected_test.lean b/tests/lean/protected_test.lean index 20f8757dea..e7e93c0c8e 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 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 diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out index 9d307bb989..a6bb326453 100644 --- a/tests/lean/protected_test.lean.expected.out +++ b/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