Zulip Chat Archive

Stream: general

Topic: Finding the correct order instance


Yaël Dillies (Jun 22 2021 at 21:25):

Here's a goal I'm encountering.

α: Type u_1
_inst_1: decidable_eq α
_inst_2: some_order_instance α
a c x: α
hx: a + c  x
  (y : α), c + y = x

What should be some_order_instance? The rest of the proof requires at least ordered_cancel_add_comm_monoid α.

Heather Macbeth (Jun 22 2021 at 21:29):

Maybe docs#has_exists_add_of_le?

Yaël Dillies (Jun 22 2021 at 21:31):

But then how do I prove c ≤ x? I don't know that a + c ≤ c.

Eric Wieser (Jun 22 2021 at 21:32):

I think that + add_comm_group is enough

Yaël Dillies (Jun 22 2021 at 21:33):

Yeah but then it doesn't apply to ℕ... This is related to my locally_finite_order PR btw

Yaël Dillies (Jun 22 2021 at 21:35):

I guess @Damiano Testa will either know the instance or tell me it doesn't exist.

Yaël Dillies (Jun 22 2021 at 21:36):

Ahah, isn't it related to the monus that I was talking about with Scott?

Eric Wieser (Jun 22 2021 at 21:36):

exists_add_of_le gives ∃ z, a + c + z = x, and a suitable obtain and add_comm makes your goal ∃ y, c + y = c + z + a?

Yaël Dillies (Jun 22 2021 at 21:37):

Oh, of course :grinning:

Yaël Dillies (Jun 22 2021 at 21:37):

This is me after 12h of ECM talks.

Yaël Dillies (Jun 22 2021 at 21:43):

And indeed the next lemma on my list requires the monus...
lemma image_sub (a b c : α) (h : a ≤ c) : (Ico a b).image (λ x, x - c) = Ico (a - c) (b - c) :=

Yaël Dillies (Jun 22 2021 at 21:44):

aka x ≤ y → y - x + x = y

Heather Macbeth (Jun 22 2021 at 21:57):

@Yaël Dillies, have you seen the series of lemmas about intervals which inspired @Peter Nelson to define docs#exists_add_of_le? See docs#set.Icc_add_bij and following.

Damiano Testa (Jun 23 2021 at 02:28):

Yaël, I am late to this, but reduing the assumptions on has_exists_mul/add_of_le is on my todo list. For this to be effective, it might also be useful to have a typeclass asserting that the unit of a binary operation is the bottom of an order relation. Below is what I have in mind: the first part works with the current typeclasses, the second one is an attempt with the new ones.

import algebra.ordered_monoid

variable {α : Type*}

/-  What is in this section should be available after the `ordered` refactor. -/
section

@[to_additive] lemma le_mul_self' [mul_one_class α] [preorder α]
  [covariant_class α α (function.swap (*)) ()] {a b : α} (b1 : 1  b) : a  b * a :=
calc  a = 1 * a : (one_mul a).symm
    ...  b * a : mul_le_mul_right' b1 _

@[to_additive] lemma yael_mul [ordered_comm_monoid α] [has_exists_mul_of_le α] {a c x : α}
  (a1 : 1  a) (hx : a * c  x) :
   (y : α), c * y = x :=
suffices h :  (y : α), x = c * y, by { simp_rw eq_comm, exact h },
exists_mul_of_le (trans (le_mul_self' a1) hx)

end

/-  In the `new` namespace is something that I am thinking about for `has_exists_mul_of_le`. -/
namespace new
variable (α)

/--  `0` is a bottom element. -/
class has_zero_le [has_add α] [has_zero α] [has_le α] : Prop :=
(zero_le :  a : α, 0  a)

/--  `1` is a bottom element. -/
class has_one_le [has_mul α] [has_one α] [has_le α] : Prop :=
(one_le :  a : α, 1  a)

attribute [to_additive has_zero_le] has_one_le

/--  The `has_exists_add_of_le` typeclass with fewer assumptions. -/
class has_exists_add_of_le' [has_add α] [has_le α] : Prop :=
(exists_add_of_le :  {a b : α}, a  b   (c : α), b = a + c)

/--  The `has_exists_mul_of_le` typeclass with fewer assumptions. -/
class has_exists_mul_of_le' [has_mul α] [has_le α] : Prop :=
(exists_mul_of_le :  {a b : α}, a  b   (c : α), b = a * c)

attribute [to_additive] has_exists_mul_of_le'

variable {α}

@[to_additive] lemma le_mul_self' [mul_one_class α] [preorder α] [has_one_le α]
  [covariant_class α α (function.swap (*)) ()] (a b : α) : a  b * a :=
calc  a = 1 * a : (one_mul a).symm
    ...  b * a : mul_le_mul_right' (has_one_le.one_le b) _

@[to_additive] lemma yael_mul [mul_one_class α] [preorder α] [has_one_le α]
  [covariant_class α α (function.swap (*)) ()] [has_exists_mul_of_le' α]
  {a c x : α} (hx : a * c  x) :
   (y : α), c * y = x :=
suffices h :  (y : α), x = c * y, by { simp_rw eq_comm, exact h },
has_exists_mul_of_le'.exists_mul_of_le (trans (le_mul_self' c a) hx)

end new

Eric Wieser (Jun 23 2021 at 07:11):

I can't help but feel relaxing these to has_le is asking for trouble

Eric Wieser (Jun 23 2021 at 07:14):

The obvious phrasing to me for has_zero_le uses docs#order_bot

class zero_eq_bot (α) [order_bot α] [has_zero α] :=
(eq : (0 : α) = )

Damiano Testa (Jun 23 2021 at 10:49):

Fair enough and, admittedly, I do not really have applications for this in the case in which the relation isn't, say, transitive. Thus, the extra assumptions are always satisfied in my use cases. In any case, I am not planning on doing this any time soon: I am already busy enough with the order refactor and I consider this as a plan for after it is done

If someone else wants to think about this, feel free to do so!

Yaël Dillies (Jun 23 2021 at 11:22):

Damiano, do you think there's a way to have an order class that would state a < b ↔ a + 1 ≤ b? That would allow me to generalise this lemma (and the Icc, Ioc, Ioo variants).
lemma card_Ico (n m : ℕ) : (Ico n m).card = m - n := to , ℕ+ and fin n.

Yaël Dillies (Jun 23 2021 at 11:23):

The lemma for it is called int.lt_add_one_iff

Eric Wieser (Jun 23 2021 at 11:57):

@Anne Baanen had a has_enum refactor or similar to handle that

Yaël Dillies (Jun 23 2021 at 12:27):

Ah yeah. What I need is has_enum + archimedean.

Yaël Dillies (Jun 23 2021 at 12:36):

How is that going, Anne?

Anne Baanen (Jun 23 2021 at 13:45):

I have an old version in branch#fin_range, but I gave up my original attempt because it was too much work to replace the built-in list.range/multiset.range/finset.range outright (and I found another way to do what I "really" wanted without has_enum). The main action is in this file, containing a syntactic has_enum class (with only the definition of list.Ico) and a lawful_enum class with the specification: https://github.com/leanprover-community/mathlib/blob/fin_range/src/data/list/enum.lean

Anne Baanen (Jun 23 2021 at 13:50):

I did not include a lemma on + 1 or require the existence of a successor function, since fin 0 does not have a 1 but it can still be enumerated (namely, with the empty list), and the successor function cannot be injective and strictly larger on finite types.

Yaël Dillies (Jun 23 2021 at 13:51):

Oh but this is very much what I'm doing now. I thought has_enum would mean that every element is either top or covered by another one, and that's a strictly weaker property than locally_finite_order.

Eric Wieser (Jun 23 2021 at 13:52):

What was it that you "really" wanted when you did that?

Anne Baanen (Jun 23 2021 at 13:52):

Please re-use as much as you need!

Anne Baanen (Jun 23 2021 at 13:55):

Eric Wieser said:

What was it that you "really" wanted when you did that?

How to do the row manipulations in src#det_vandermonde (which in the end were easier to do with finset.range of natural numbers)

Yaël Dillies (Jun 23 2021 at 14:01):

What I now want here is to say that no element is in between the coercion from (or ) to α. That's again something different and I think something like

@[class] structure has_lt_iff_add_one_le (α : Type*) [ordered_semiring α] : Prop :=
(lt_iff_add_one_le :  a b : α, a < b  a + 1  b)

would be worth having.

Eric Wieser (Jun 23 2021 at 14:07):

(this isn't Discord, you don't need to mark your lean as haskell!)

Yaël Dillies (Jun 23 2021 at 14:22):

Whoops! Yeah


Last updated: Dec 20 2023 at 11:08 UTC