From c8b7816d5a09e327bdb6421fa80d7595227e4ced Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Mon, 2 Aug 2021 12:31:20 +0000 Subject: [PATCH] feat(algebra/ordered_monoid): add_eq_bot_iff (#8474) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit bot addition is saturating on the bottom. On the way, typeclass arguments were relaxed to just `[add_semigroup α]`, and helper simp lemmas added for `bot`. The iff lemma added (`add_eq_bot`) is not exactly according to the naming convention, but matches the top lemma and related ones in the naming style, so the style is kept consistent. There is an API proof available, but the defeq proof (using the top equivalent) was used based on suggestions. --- src/algebra/ordered_monoid.lean | 8 ++++++-- src/order/bounded_lattice.lean | 3 +++ 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean index 36a0f49c65bc9..94d1567cd0a1f 100644 --- a/src/algebra/ordered_monoid.lean +++ b/src/algebra/ordered_monoid.lean @@ -494,9 +494,13 @@ by norm_cast lemma coe_bit1 [add_semigroup α] [has_one α] {a : α} : ((bit1 a : α) : with_bot α) = bit1 a := by norm_cast -@[simp] lemma bot_add [ordered_add_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl +@[simp] lemma bot_add [add_semigroup α] (a : with_bot α) : ⊥ + a = ⊥ := rfl -@[simp] lemma add_bot [ordered_add_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl +@[simp] lemma add_bot [add_semigroup α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl + +@[simp] lemma add_eq_bot [add_semigroup α] {m n : with_bot α} : + m + n = ⊥ ↔ m = ⊥ ∨ n = ⊥ := +with_top.add_eq_top end with_bot diff --git a/src/order/bounded_lattice.lean b/src/order/bounded_lattice.lean index 771c1ef34fab8..aadf72ced9d33 100644 --- a/src/order/bounded_lattice.lean +++ b/src/order/bounded_lattice.lean @@ -449,6 +449,9 @@ instance : inhabited (with_bot α) := ⟨⊥⟩ lemma none_eq_bot : (none : with_bot α) = (⊥ : with_bot α) := rfl lemma some_eq_coe (a : α) : (some a : with_bot α) = (↑a : with_bot α) := rfl +@[simp] theorem bot_ne_coe (a : α) : ⊥ ≠ (a : with_bot α) . +@[simp] theorem coe_ne_bot (a : α) : (a : with_bot α) ≠ ⊥ . + /-- Recursor for `with_bot` using the preferred forms `⊥` and `↑a`. -/ @[elab_as_eliminator] def rec_bot_coe {C : with_bot α → Sort*} (h₁ : C ⊥) (h₂ : Π (a : α), C a) :