from le to ge by duality?

Stream: maths

[Jalex Stark]

I have a theorem about mins for an arbitrary linear order $M$. I'd like to get the dual theorems about max by applying the first theorem to $M^{op}$ and then reinterpreting them in $M$. Is there any particular machinery to make this easier or should I just do it?

import tactic

import data.finset
import data.finsupp
import data.nat.basic


universes u
open_locale classical

open function

class DLO (α : Type u) extends decidable_linear_order α :=
(dense : ∀ a b : α, (a < b) → ∃ c, a < c ∧ c < b)
(without_top : ∀ a : α, ∃ b, a < b)
(without_bot : ∀ a : α, ∃ b, b < a)

variables {M N : Type u} [DLO M] [DLO N] [inhabited M] [inhabited N]
open pfun

example

-- given a finset in a DLO, produce an element below or above everything

def min_of_finset' (X : finset M) (X_nonempty : finset.nonempty X) : ∃ l ∈ X, ∀ x ∈ X, l ≤ x := finset.exists_min X id X_nonempty

def lb_of_finset (X : finset M) : ∃ l, ∀ x∈ X, l < x := begin
by_cases finset.nonempty X,
swap,
{   use arbitrary M,
    intro x, intro hx,
    unfold finset.nonempty at h, push_neg at h,
    exfalso, exact h x hx},
-- maybe using have and contradiction is mathier in the above
have m := min_of_finset' _ h,
cases m with m hm,
cases hm with m_in_X hm,
have key := DLO.without_bot m,
cases key with l hl,
use l,
intros x hx,
apply lt_of_lt_of_le hl,
apply hm, assumption,
end

[Jalex Stark]

Hmm I guess the answer is going to be that the machinery is in the category_theory library, so maybe I'll just do it "by hand" for now

[Chris Hughes]

You can use order_dual

[Chris Hughes]

The proof of the dual of lb_of_finset should be @lb_of_finset (order_dual M) _ _. You have to put the right DLO instance on order_dual M for this to work. Put an instance for the recerse order on it.

[Chris Hughes]

There should already be a linear_order instance.

[Jalex Stark]

hmm I don't know how to break up DLO so that I can give the linear_order and without_* instance separately

[Jalex Stark]

In other words, I don't understand what the constructor is for typeclass that's made via extends
so probably I can answer this by reading TPiL

[Yury G. Kudryashov]

BTW, we already have class no_top_order

[Yury G. Kudryashov]

Moreover, we have classes no_top_order, no_bot_order and densely_ordered

[Yury G. Kudryashov]

So if you're writing for mathlib, then you can use [linear_order α] [no_bot_order α] [densely_ordered α]

[Yury G. Kudryashov]

See also directed.finset_le and finset.exists_le in algebra/big_operators.

[Yury G. Kudryashov]

So, for finset.exists_lt you just need [nonempty α] [directed_order α] [no_bot_order α]

[Yury G. Kudryashov]

Note that we don't have a dual to directed_order

[Yury G. Kudryashov]

And we don't have any good instance for directed_order. You can easily add semilattice_inf.directed_order.

[Jalex Stark]

is there a way to bundle linear_order, no_top_order, no_bot_order and densely_ordered into one class?

[Jalex Stark]

I can do this but then I'm carrying around new names? I really want to chain the extends

class DLO' (α : Type u) extends decidable_linear_order α :=
(dense : densely_ordered α)
(without_top : no_top_order α )
(without_bot : no_bot_order α )

[David Wärn]

I had this issue a while ago (working on the same kata!) (link). Mario recommended the solution you describe. My understanding is that chaining all the extends is problematic because densely_ordered is parametrised by the order. You could at least combine no_top_order, no_bot_order and densely_ordered into one class?

In the end I decided against defining a new class, and just did the back-and-forth argument with assumptions decidable_linear_order, no_top_order, ... for both types.

[David Wärn]

Btw, I think you might want finset.max' / finset.min'?