Ordered set

Stream: new members

[Marcus Rossel]

Is there a notion of a (totally) ordered set in Mathlib?
I'm not a mathematician, so I basically think of this as a list without duplicates. But I'm guessing a more mathy version would be a set together with a linear order (?).

[Yakov Pechersky]

A list such that docs#list.sorted

[Yakov Pechersky]

or you can encode it using a docs#order_embedding

[Heather Macbeth]

or just docs#linear_order

[Marcus Rossel]

Oh, turns out I actually do only need a partial order :see_no_evil:

[Heather Macbeth]

docs#partial_order

[Marcus Rossel]

@Heather Macbeth I'm not sure if I can use docs#partial_order for my use case.
I'm trying to define a proposition that defines when an ordered set is a topological ordering over a graph:
Currently, instead of using "ordered set", I use a list and also force it to be nodup:

def list.is_topo_over (l : list ι) (g : graph ι δ ε) : Prop :=
  l.nodup ∧ ∀ i i' ∈ l, g.has_path_from_to i i' → (l.index_of i < l.index_of i')

[Yakov Pechersky]

Imports?

[Yakov Pechersky]

This should be sufficient:

def list.is_topo_over (g : graph ι δ ε) : Prop :=
  l.nodup ∧ l.pairwise g.has_path_from_to

[Marcus Rossel]

I guess this would be an MWE:

structure graph := (unimportant: nat)
def graph.has_path_from_to (g : graph) (i i' : nat) : Prop := g.unimportant = i

def list.is_topo_over (l : list nat) (g : graph) : Prop :=
  l.nodup ∧ ∀ i i' ∈ nat, g.has_path_from_to i i' → (l.index_of i < l.index_of i')

[Marcus Rossel]

Yakov Pechersky said:

This should be sufficient:

def list.is_topo_over (g : graph ι δ ε) : Prop :=
  l.nodup ∧ l.pairwise g.has_path_from_to

So list with nodup is basically the notion of ordered set?

[Kevin Buzzard]

that's a finite ordered set

[Marcus Rossel]

Yes, I forgot the finite part.

[Yakov Pechersky]

import data.list.nodup

structure graph := (unimportant: nat)
def graph.has_path_from_to (g : graph) (i i' : nat) : Prop := g.unimportant = i

variables (l : list nat) (g : graph)

def list.is_topo_over  : Prop :=
  l.nodup ∧ l.pairwise g.has_path_from_to

open list

example (n m : ℕ) (hn : n < l.length) (hm : m < l.length) (ho : n < m) (h : l.is_topo_over g) :
  g.has_path_from_to (l.nth_le n hn) (l.nth_le m hm) :=
pairwise_iff_nth_le.mp h.right _ _ _ ho

[Heather Macbeth]

Have you proved that g.has_path_from_to gives a partial order instance on ι? If so, Yakov's code can be written as something like

def list.is_topo_over (g : graph ι δ ε) : Prop := l.pairwise (<)

[Yakov Pechersky]

It gives a partial order instance on the subtype given by elements of l

[Heather Macbeth]

Because when you have a preorder (defined using $\le$), mathlib automatically makes the $<$ relation for you: docs#preorder.to_has_lt

[Yakov Pechersky]

def graph.induced_order : partial_order {i : nat // i ∈ l} :=
{ le := λ i j, i = j ∨ g.has_path_from_to i j,
  lt := λ i j, g.has_path_from_to i j,
  le_refl := λ i, or.inl rfl,
  le_trans := by sorry,
  lt_iff_le_not_le := by sorry,
  le_antisymm := by sorry }

[Marcus Rossel]

I don't understand how ...

l.pairwise g.has_path_from_to

... is the same as ...

∀ i i' ∈ l, g.has_path_from_to i i' → (l.index_of i < l.index_of i')

The docs for docs#list.pairwise state that "pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes." But in the ∀-based definition, i having a smaller index than i' doesn't necessarily mean that there's a path from i to i' (I think). It's rather the other way around.

[Yakov Pechersky]

docs#list.pairwise_iff_nth_le is precisely what your index_of based statement implies.

[Yakov Pechersky]

index_of is an iso iff the list is nodup. So I'd just use pairwise for your Prop def, and require nodup when you're proving things about it.

[Marcus Rossel]

Hm, I still don't see the equivalence of the two definitions. I'll try to find a counterexample.

[Yakov Pechersky]

I see the issue here. You said ∀ i i' ∈ nat while I am saying ∀ i i' ∈ l.

[Marcus Rossel]

Oh that's just a typo ^^'

[Yakov Pechersky]

Do you agree that if l.index_of i = n then l.nth n = some i?

[Marcus Rossel]

Yes :)

[Yakov Pechersky]

So we can just refer to the elements of l using l.nth_le. docs#list.pairwise_iff_nth_le states that if a list is pairwise R, then R (nth_le n _) (nth_le m _) for n < m. That means that for all elements x y in l, R x y if x comes before y in l.

[Marcus Rossel]

As a counterexample: Let's assume g : graph with:

g.has_path_from_to 10 20
g.has_path_from_to 10 30

Then by the ∀-based definition both [10, 20, 30] and [10, 30, 20] are topos over g.
But by the pairwise-based definition there is no topo over g.
Is this right?

[Yakov Pechersky]

Is your path transitive?

[Marcus Rossel]

Yes, but the edges are directed :D
I.e. g.has_path_from_to x y doesn't imply g.has_path_from_to y x.

[Yakov Pechersky]

[10, 20, 30].pairwise R means 10 R 20, 10 R 30, 20 R 30. pairwise makes no requirement or statement about whether R is symmetric or not.

[Marcus Rossel]

Yes exactly, but in the case of

g.has_path_from_to 10 20
g.has_path_from_to 10 30

The 20 R 30 part isn't true, but [10, 20, 30] should be valid.

[Yakov Pechersky]

Aha, I see, I had the implication the wrong way.

[Marcus Rossel]

Thanks for taking the time anyway. Very much appreciated! :pray:

[Yakov Pechersky]

docs#is_preorder, when your operate on the subtype of elements of l?

[Yakov Pechersky]

or I guess even strong, docs#is_partial_order?

[Yakov Pechersky]

I think again I have the implication wrong. So I think what you had originally is good, but should use

∀ (n < l.length) (m < l.length), g.has_path_from_to (l.nth_le n ‹_›) (l.nth_le m ‹_›) → n < m

[Marcus Rossel]

Yakov Pechersky said:

I think again I have the implication wrong. So I think what you had originally is good, but should use

∀ (n < l.length) (m < l.length), g.has_path_from_to (l.nth_le n ‹_›) (l.nth_le m ‹_›) → n < m

What's the benefit of ...

∀ (n < l.length) (m < l.length), g.has_path_from_to (l.nth_le n ‹_›) (l.nth_le m ‹_›) → n < m

... over ...?

∀ i i' ∈ l, g.has_path_from_to i i' → (l.index_of i < l.index_of i')

[Yakov Pechersky]

The index_of version will be only useful if the list is nodup. Plus there are many more lemmas about nth_le than index_of

[Yakov Pechersky]

The contravariant version of docs#relator.lift_fun would be useful here

[Yakov Pechersky]

In the meantime, a convoluted way to say something about your list:

#check ((λ (i j : fin l.length), g.has_path_from_to (l.nth_le i i.is_lt) (l.nth_le j j.is_lt)) ⇒ (<)) id id

[Yakov Pechersky]

Your phrasing was

#check (g.has_path_from_to ⇒ (<)) (λ i, list.index_of i l) (λ i, list.index_of i l)

[Yakov Pechersky]

It's too bad that l.index_of is inferred to do the wrong thing.