From 22011dcde4adf0aa70a083476254175f28773713 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 2 Aug 2017 15:25:38 +0100 Subject: [PATCH] chore(init/algebra/order): typo Thanks to @fpvandoorn for proof-reading! --- doc/changes.md | 2 +- library/init/algebra/order.lean | 56 +++++++++++++++--------------- tests/lean/run/order_defaults.lean | 2 +- 3 files changed, 30 insertions(+), 30 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index 7b57829dad..b821b0c09f 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -107,7 +107,7 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ most things that were once imported by this are now imported by default. * The type classes for orders have been refactored to combine both the `(<)` - and `(≤)` operations. The new classes are `pre_order`, `partial_order`, and + and `(≤)` operations. The new classes are `preorder`, `partial_order`, and `linear_order`. The `partial_order` class corresponds to `weak_order`, `strict_order`, `order_pair`, and `strong_order_pair`. The `linear_order` class corresponds to `linear_order_pair`, and `linear_strong_order_pair`. diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean index a1bcda663e..1cdd68f4e4 100644 --- a/library/init/algebra/order.lean +++ b/library/init/algebra/order.lean @@ -15,43 +15,43 @@ universe u variables {α : Type u} set_option auto_param.check_exists false -class pre_order (α : Type u) extends has_le α, has_lt α := +class preorder (α : Type u) extends has_le α, has_lt α := (le_refl : ∀ a : α, a ≤ a) (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c) (lt := λ a b, a ≤ b ∧ ¬ b ≤ a) (lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac) -class partial_order (α : Type u) extends pre_order α := +class partial_order (α : Type u) extends preorder α := (le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b) class linear_order (α : Type u) extends partial_order α := (le_total : ∀ a b : α, a ≤ b ∨ b ≤ a) -@[refl] lemma le_refl [pre_order α] : ∀ a : α, a ≤ a := -pre_order.le_refl +@[refl] lemma le_refl [preorder α] : ∀ a : α, a ≤ a := +preorder.le_refl -@[trans] lemma le_trans [pre_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c := -pre_order.le_trans +@[trans] lemma le_trans [preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c := +preorder.le_trans -lemma lt_iff_le_not_le [pre_order α] : ∀ {a b : α}, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := -pre_order.lt_iff_le_not_le _ +lemma lt_iff_le_not_le [preorder α] : ∀ {a b : α}, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := +preorder.lt_iff_le_not_le _ -lemma lt_of_le_not_le [pre_order α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b +lemma lt_of_le_not_le [preorder α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b | a b hab hba := lt_iff_le_not_le.mpr ⟨hab, hba⟩ -lemma le_not_le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a +lemma le_not_le_of_lt [preorder α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a | a b hab := lt_iff_le_not_le.mp hab lemma le_antisymm [partial_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b := partial_order.le_antisymm -lemma le_of_eq [pre_order α] {a b : α} : a = b → a ≤ b := +lemma le_of_eq [preorder α] {a b : α} : a = b → a ≤ b := λ h, h ▸ le_refl a lemma le_antisymm_iff [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a := ⟨λe, ⟨le_of_eq e, le_of_eq e.symm⟩, λ⟨h1, h2⟩, le_antisymm h1 h2⟩ -@[trans] lemma ge_trans [pre_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c := +@[trans] lemma ge_trans [preorder α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c := λ a b c h₁ h₂, le_trans h₂ h₁ lemma le_total [linear_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a := @@ -63,15 +63,15 @@ or.resolve_left (le_total b a) lemma le_of_not_le [linear_order α] {a b : α} : ¬ a ≤ b → b ≤ a := or.resolve_left (le_total a b) -lemma lt_irrefl [pre_order α] : ∀ a : α, ¬ a < a +lemma lt_irrefl [preorder α] : ∀ a : α, ¬ a < a | a haa := match le_not_le_of_lt haa with | ⟨h1, h2⟩ := false.rec _ (h2 h1) end -lemma gt_irrefl [pre_order α] : ∀ a : α, ¬ a > a := +lemma gt_irrefl [preorder α] : ∀ a : α, ¬ a > a := lt_irrefl -@[trans] lemma lt_trans [pre_order α] : ∀ {a b c : α}, a < b → b < c → a < c +@[trans] lemma lt_trans [preorder α] : ∀ {a b c : α}, a < b → b < c → a < c | a b c hab hbc := match le_not_le_of_lt hab, le_not_le_of_lt hbc with | ⟨hab, hba⟩, ⟨hbc, hcb⟩ := lt_of_le_not_le (le_trans hab hbc) (λ hca, hcb (le_trans hca hab)) @@ -79,46 +79,46 @@ lt_irrefl def lt.trans := @lt_trans -@[trans] lemma gt_trans [pre_order α] : ∀ {a b c : α}, a > b → b > c → a > c := +@[trans] lemma gt_trans [preorder α] : ∀ {a b c : α}, a > b → b > c → a > c := λ a b c h₁ h₂, lt_trans h₂ h₁ def gt.trans := @gt_trans -lemma ne_of_lt [pre_order α] {a b : α} (h : a < b) : a ≠ b := +lemma ne_of_lt [preorder α] {a b : α} (h : a < b) : a ≠ b := λ he, absurd h (he ▸ lt_irrefl a) -lemma ne_of_gt [pre_order α] {a b : α} (h : a > b) : a ≠ b := +lemma ne_of_gt [preorder α] {a b : α} (h : a > b) : a ≠ b := λ he, absurd h (he ▸ lt_irrefl a) -lemma lt_asymm [pre_order α] {a b : α} (h : a < b) : ¬ b < a := +lemma lt_asymm [preorder α] {a b : α} (h : a < b) : ¬ b < a := λ h1 : b < a, lt_irrefl a (lt_trans h h1) lemma not_lt_of_gt [linear_order α] {a b : α} (h : a > b) : ¬ a < b := lt_asymm h -lemma le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b +lemma le_of_lt [preorder α] : ∀ {a b : α}, a < b → a ≤ b | a b hab := (le_not_le_of_lt hab).left -@[trans] lemma lt_of_lt_of_le [pre_order α] : ∀ {a b c : α}, a < b → b ≤ c → a < c +@[trans] lemma lt_of_lt_of_le [preorder α] : ∀ {a b c : α}, a < b → b ≤ c → a < c | a b c hab hbc := let ⟨hab, hba⟩ := le_not_le_of_lt hab in lt_of_le_not_le (le_trans hab hbc) $ λ hca, hba (le_trans hbc hca) -@[trans] lemma lt_of_le_of_lt [pre_order α] : ∀ {a b c : α}, a ≤ b → b < c → a < c +@[trans] lemma lt_of_le_of_lt [preorder α] : ∀ {a b c : α}, a ≤ b → b < c → a < c | a b c hab hbc := let ⟨hbc, hcb⟩ := le_not_le_of_lt hbc in lt_of_le_not_le (le_trans hab hbc) $ λ hca, hcb (le_trans hca hab) -@[trans] lemma gt_of_gt_of_ge [pre_order α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c := +@[trans] lemma gt_of_gt_of_ge [preorder α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c := lt_of_le_of_lt h₂ h₁ -@[trans] lemma gt_of_ge_of_gt [pre_order α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c := +@[trans] lemma gt_of_ge_of_gt [preorder α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c := lt_of_lt_of_le h₂ h₁ -lemma not_le_of_gt [pre_order α] {a b : α} (h : a > b) : ¬ a ≤ b := +lemma not_le_of_gt [preorder α] {a b : α} (h : a > b) : ¬ a ≤ b := (le_not_le_of_lt h).right -lemma not_lt_of_ge [pre_order α] {a b : α} (h : a ≥ b) : ¬ a < b := +lemma not_lt_of_ge [preorder α] {a b : α} (h : a ≥ b) : ¬ a < b := λ hab, not_le_of_gt hab h lemma lt_or_eq_of_le [partial_order α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b @@ -176,7 +176,7 @@ match lt_trichotomy a b with | or.inr (or.inr hgt) := or.inr hgt end -lemma le_of_eq_or_lt [pre_order α] {a b : α} (h : a = b ∨ a < b) : a ≤ b := +lemma le_of_eq_or_lt [preorder α] {a b : α} (h : a = b ∨ a < b) : a ≤ b := or.elim h le_of_eq le_of_lt lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b := @@ -185,7 +185,7 @@ lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b lemma lt_iff_not_ge [linear_order α] (x y : α) : x < y ↔ ¬ x ≥ y := ⟨not_le_of_gt, lt_of_not_ge⟩ -instance decidable_lt_of_decidable_le [pre_order α] +instance decidable_lt_of_decidable_le [preorder α] [decidable_rel ((≤) : α → α → Prop)] : decidable_rel ((<) : α → α → Prop) | a b := diff --git a/tests/lean/run/order_defaults.lean b/tests/lean/run/order_defaults.lean index 420e361bea..97bcbab9b3 100644 --- a/tests/lean/run/order_defaults.lean +++ b/tests/lean/run/order_defaults.lean @@ -1,4 +1,4 @@ -example : pre_order unit := { +example : preorder unit := { le := λ _ _, true, le_refl := λ _, trivial, le_trans := λ _ _ _ _ _, trivial,