Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore(WithTop): less abuse of defeq to Option _ #9986

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(WithTop): less abuse of defeq to Option _ #9986

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 8 additions & 18 deletions Mathlib/Algebra/Order/Monoid/WithTop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,22 +155,19 @@ theorem add_lt_top [LT α] {a b : WithTop α} : a + b < ⊤ ↔ a < ⊤ ∧ b <

theorem add_eq_coe :
∀ {a b : WithTop α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
| none, b, c => by simp [none_eq_top]
| Option.some a, none, c => by simp [none_eq_top]
| Option.some a, Option.some b, c =>
by simp only [some_eq_coe, ← coe_add, coe_eq_coe, exists_and_left, exists_eq_left]
| ⊤, b, c => by simp
| some a, ⊤, c => by simp
| some a, some b, c => by norm_cast; simp
#align with_top.add_eq_coe WithTop.add_eq_coe

-- Porting note: simp can already prove this.
-- @[simp]
theorem add_coe_eq_top_iff {x : WithTop α} {y : α} : x + y = ⊤ ↔ x = ⊤ := by
induction x using WithTop.recTopCoe <;> simp [← coe_add]
theorem add_coe_eq_top_iff {x : WithTop α} {y : α} : x + y = ⊤ ↔ x = ⊤ := by simp
#align with_top.add_coe_eq_top_iff WithTop.add_coe_eq_top_iff

-- Porting note: simp can already prove this.
-- @[simp]
theorem coe_add_eq_top_iff {y : WithTop α} : ↑x + y = ⊤ ↔ y = ⊤ := by
induction y using WithTop.recTopCoe <;> simp [← coe_add]
theorem coe_add_eq_top_iff {y : WithTop α} : ↑x + y = ⊤ ↔ y = ⊤ := by simp
#align with_top.coe_add_eq_top_iff WithTop.coe_add_eq_top_iff

theorem add_right_cancel_iff [IsRightCancelAdd α] (ha : a ≠ ⊤) : b + a = c + a ↔ b = c := by
Expand Down Expand Up @@ -364,8 +361,7 @@ instance addMonoidWithOne : AddMonoidWithOne (WithTop α) :=
rw [Nat.cast_zero, WithTop.coe_zero],
natCast_succ := fun n => by
simp only -- Porting note: Had to add this...?
rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one]
}
rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one] }

@[simp, norm_cast] lemma coe_nat (n : ℕ) : ((n : α) : WithTop α) = n := rfl
#align with_top.coe_nat WithTop.coe_nat
Expand All @@ -385,14 +381,8 @@ instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α) :=
instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α) :=
{ WithTop.addMonoidWithOne, WithTop.addCommMonoid with }

instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α) :=
{ WithTop.partialOrder, WithTop.addCommMonoid with
add_le_add_left := by
rintro a b h (_ | c); · simp [none_eq_top]
rcases b with (_ | b); · simp [none_eq_top]
rcases le_coe_iff.1 h with ⟨a, rfl, _⟩
simp only [some_eq_coe, ← coe_add, coe_le_coe] at h ⊢
exact add_le_add_left h c }
instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α) where
add_le_add_left _ _ := add_le_add_left

instance linearOrderedAddCommMonoidWithTop [LinearOrderedAddCommMonoid α] :
LinearOrderedAddCommMonoidWithTop (WithTop α) :=
Expand Down
44 changes: 19 additions & 25 deletions Mathlib/Order/WithBot.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,8 +96,8 @@ theorem coe_ne_bot : (a : WithBot α) ≠ ⊥ :=
/-- Recursor for `WithBot` using the preferred forms `⊥` and `↑a`. -/
@[elab_as_elim]
def recBotCoe {C : WithBot α → Sort*} (bot : C ⊥) (coe : ∀ a : α, C a) : ∀ n : WithBot α, C n
| none => bot
| Option.some a => coe a
| ⊥ => bot
| (a : α) => coe a
#align with_bot.rec_bot_coe WithBot.recBotCoe

@[simp]
Expand Down Expand Up @@ -239,18 +239,18 @@ theorem coe_le : ∀ {o : Option α}, b ∈ o → ((a : WithBot α) ≤ o ↔ a
#align with_bot.coe_le WithBot.coe_le

theorem coe_le_iff : ∀ {x : WithBot α}, (a : WithBot α) ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b
| Option.some x => by simp [some_eq_coe]
| none => iff_of_false (not_coe_le_bot _) <| by simp [none_eq_bot]
| (x : α) => by simp
| ⊥ => iff_of_false (not_coe_le_bot _) <| by simp
#align with_bot.coe_le_iff WithBot.coe_le_iff

theorem le_coe_iff : ∀ {x : WithBot α}, x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b
| Option.some b => by simp [some_eq_coe, coe_eq_coe]
| none => by simp [none_eq_bot]
| (b : α) => by simp
| ⊥ => by simp
#align with_bot.le_coe_iff WithBot.le_coe_iff

protected theorem _root_.IsMax.withBot (h : IsMax a) : IsMax (a : WithBot α)
| none, _ => bot_le
| Option.some _, hb => some_le_some.2 <| h <| some_le_some.1 hb
| ⊥, _ => bot_le
| (_ : α), hb => some_le_some.2 <| h <| some_le_some.1 hb
#align is_max.with_bot IsMax.withBot

theorem le_unbot_iff {a : α} {b : WithBot α} (h : b ≠ ⊥) :
Expand Down Expand Up @@ -305,13 +305,13 @@ theorem not_lt_none (a : WithBot α) : ¬@LT.lt (WithBot α) _ a none :=
#align with_bot.not_lt_none WithBot.not_lt_none

theorem lt_iff_exists_coe : ∀ {a b : WithBot α}, a < b ↔ ∃ p : α, b = p ∧ a < p
| a, Option.some b => by simp [some_eq_coe, coe_eq_coe]
| a, none => iff_of_false (not_lt_none _) <| by simp [none_eq_bot]
| a, some b => by simp [coe_eq_coe]
| a, ⊥ => iff_of_false (not_lt_none _) <| by simp
#align with_bot.lt_iff_exists_coe WithBot.lt_iff_exists_coe

theorem lt_coe_iff : ∀ {x : WithBot α}, x < b ↔ ∀ a : α, x = ↑a → a < b
| Option.some b => by simp [some_eq_coe, coe_eq_coe, coe_lt_coe]
| none => by simp [none_eq_bot, bot_lt_coe]
theorem lt_coe_iff : ∀ {x : WithBot α}, x < b ↔ ∀ a : α, x = a → a < b
| (_ : α) => by simp
| ⊥ => by simp [bot_lt_coe]
#align with_bot.lt_coe_iff WithBot.lt_coe_iff

/-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
Expand Down Expand Up @@ -1300,25 +1300,19 @@ instance instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithTop

instance trichotomous.lt [Preorder α] [IsTrichotomous α (· < ·)] :
IsTrichotomous (WithTop α) (· < ·) :=
⟨by
rintro (a | a) (b | b)
· simp
· simp
· simp
· simpa [some_eq_coe, IsTrichotomous, coe_eq_coe] using @trichotomous α (· < ·) _ a b⟩
⟨fun
| (a : α), (b : α) => by simp [trichotomous]
| ⊤, (b : α) => by simp
| (a : α), ⊤ => by simp
| ⊤, ⊤ => by simp⟩
#align with_top.trichotomous.lt WithTop.trichotomous.lt

instance IsWellOrder.lt [Preorder α] [IsWellOrder α (· < ·)] : IsWellOrder (WithTop α) (· < ·) where
#align with_top.is_well_order.lt WithTop.IsWellOrder.lt

instance trichotomous.gt [Preorder α] [IsTrichotomous α (· > ·)] :
IsTrichotomous (WithTop α) (· > ·) :=
⟨by
rintro (a | a) (b | b)
· simp
· simp
· simp
· simpa [some_eq_coe, IsTrichotomous, coe_eq_coe] using @trichotomous α (· > ·) _ a b⟩
have : IsTrichotomous α (· < ·) := .swap _; .swap _
#align with_top.trichotomous.gt WithTop.trichotomous.gt

instance IsWellOrder.gt [Preorder α] [IsWellOrder α (· > ·)] : IsWellOrder (WithTop α) (· > ·) where
Expand Down
Loading