Disjoint union of posets

Stream: Is there code for X?

[Paul Rowe]

Is there code anywhere for the disjoint union of partially ordered sets? Something that takes the disjoint union of their underlying types and keeps only the ordering relations that exist within each type? I've started to hack something together for my own purposes, but it would be great to know if there is already a robust API somewhere?

I'm also interested in the sequential composition of posets A and B, where everything from A precedes everything from B in the composition, and all other relations are preserved.

[Yaël Dillies]

You will be glad to know that I have a PR which does precisely this!

[Paul Rowe]

Does it do both things? I.e. "parallel" and "sequential" unions?

[Yaël Dillies]

For some reason I don't understand, nobody needed it so far. But I thought it would be fun to use the disjoint/lexicographic sum of orders for more complicated order notions (locally finite orders, graded orders, incidence algebras...). So I wrote #11157

[Yaël Dillies]

Because there are two natural orders to put on α ⊕ β, my design is to equip α ⊕ β with the disjoint order and have α ⊕ₗ β a type synonym which is equipped with the linear sum.

[Yaël Dillies]

I expect it be merged today or tomorrow at the latest.

[Paul Rowe]

Oh that's great! Where should I look and what should I look for to know when it is merged?

[Yaël Dillies]

You can click here --> #11157 <-- and later it will be in file#data/sum/order

[Paul Rowe]

Got it. Thanks. I'm excited to check it out.

[Yaël Dillies]

@Paul Rowe, it's in!

[Paul Rowe]

Fantastic! I'll check it out today.

[Paul Rowe]

So, I'm trying to use the new material by incorporating it into a structure that is basically a finite labeled partial order. I'm able to transfer sum_comm and sum_assoc to my new structure, but I hit a snag in transferring sum_lex_assoc. In the mwe below, the final simp tactic fails to solve the goal, when it does solve the equivalent goal of merge. I can probably power through, but I'm not sure if there's a good reason for this not to simplify?

import data.fintype.basic
import data.sum.order

structure evsys :=
(evt : Type)
(fin : fintype evt)
(poset : partial_order evt)
(l : evt → ℕ)

instance fintype_evsys (E : evsys) := E.fin
instance poset_evsys (E : evsys) := E.poset

structure evsys_iso (E1 E2 : evsys) :=
(order : order_iso E1.evt E2.evt)
(label : ∀ e, E1.l e = E2.l (order.to_fun e))

infix ` ≃ₑ `:25 := evsys_iso

variables {E1 E2 E3 : evsys} {e1 : E1.evt} {e2 : E2.evt}

def merge (E1 E2 : evsys) : evsys :=
{ evt := E1.evt ⊕ E2.evt,
  fin := sum.fintype E1.evt E2.evt,
  poset := sum.partial_order,
  l := λ e, begin
    cases e, exact E1.l e, exact E2.l e,
  end  }

infix ` ⋈ `:26 := merge

@[simp]
lemma merge_label_inl :
  (E1 ⋈ E2).l (sum.inl e1) = E1.l e1 := rfl

@[simp]
lemma merge_label_inr :
  (E1 ⋈ E2).l (sum.inr e2) = E2.l e2 := rfl

def merge.assoc (E1 E2 E3):
 (E1 ⋈ E2) ⋈ E3 ≃ₑ E1 ⋈ (E2 ⋈ E3) :=
{ order := order_iso.sum_assoc E1.evt E2.evt E3.evt,
  label := begin
    intro e, cases e, cases e, simp, simp, simp,
  end }

def merge.comm (E1 E2):
E1 ⋈ E2 ≃ₑ (E2 ⋈ E1) :=
{ order := order_iso.sum_comm E1.evt E2.evt,
  label := begin
    intro e, cases e, simp, simp,
  end }

  def before (E1 E2 : evsys) : evsys :=
{ evt := E1.evt ⊕ₗ E2.evt,
  fin := sum.fintype E1.evt E2.evt,
  poset := sum.lex.partial_order,
  l := λ e, begin
    cases e, exact E1.l e, exact E2.l e,
  end }

infix ` ▷ `:26 := before

@[simp]
lemma before_label_inl :
  (E1 ▷ E2).l (sum.inl e1) = E1.l e1 := rfl

@[simp]
lemma before_label_inr :
  (E1 ▷ E2).l (sum.inr e2) = E2.l e2 := rfl

def before_assoc (E1 E2 E3) :
(E1 ▷ E2) ▷ E3 ≃ₑ E1 ▷ (E2 ▷ E3) :=
{ order := order_iso.sum_lex_assoc E1.evt E2.evt E3.evt,
  label := begin
    intro e, cases e, cases e, simp,
  end }

[Yaël Dillies]

This is because casing on e : (E1 ▷ E2 ▷ E3).evt breaks the type synonym.

[Paul Rowe]

I see. So would it work if I replaced the casing with a lemma that details the cases?

[Paul Rowe]

Or, rather, I can't figure out how to add back in the type synonym info into the right places.

[Yaël Dillies]

Taking the first goal out of three before the simp in before_assoc, we get

case sum.inl sum.inl
E1 E2 E3: evsys
e: E1.evt
⊢ (E1 ▷ E2 ▷ E3).l (inl (inl e)) = (E1 ▷ (E2 ▷ E3)).l ((order_iso.sum_lex_assoc E1.evt E2.evt E3.evt).to_equiv.to_fun (inl (inl e))

but it should be

case sum.inl sum.inl
E1 E2 E3: evsys
e: E1.evt
⊢ (E1 ▷ E2 ▷ E3).l (inlₗ (inlₗ e)) = (E1 ▷ (E2 ▷ E3)).l ((order_iso.sum_lex_assoc E1.evt E2.evt E3.evt).to_equiv.to_fun (inlₗ (inlₗ e))

[Yaël Dillies]

This is a rather technical issue, I'm sorry :grimacing:
I didn't know how to do myself it until a week ago

[Yaël Dillies]

One easy way is to use change to fix the goal exactly as it should be, but the goal is long enough for that to be a pain.

[Paul Rowe]

I see. No problem! I'll give that a shot.

[Yaël Dillies]

Wait, I haven't given you the proper solution yet :grinning_face_with_smiling_eyes:

[Paul Rowe]

And yes, the type synonym stuff is basically all new to me, so I'm flying blind.

[Paul Rowe]

Yeah, I'm assuming that if I try to use change I can muddle through. :smile:

[Yaël Dillies]

The idea is to define custom pattern-matching and then use it instead of casing:

import data.fintype.basic
import data.sum.order

open sum

structure evsys :=
(evt : Type)
[fin : fintype evt]
[poset : partial_order evt]
(l : evt → ℕ)

instance fintype_evsys (E : evsys) := E.fin
instance poset_evsys (E : evsys) := E.poset

structure evsys_iso (E1 E2 : evsys) :=
(order : order_iso E1.evt E2.evt)
(label : ∀ e, E1.l e = E2.l (order.to_fun e))

infix ` ≃ₑ `:25 := evsys_iso

variables {E1 E2 E3 : evsys} {e1 : E1.evt} {e2 : E2.evt}

def merge (E1 E2 : evsys) : evsys :=
{ evt := E1.evt ⊕ E2.evt,
  l := λ e, e.elim E1.l E2.l }

infix ` ⋈ `:26 := merge

@[simp] lemma merge_label_inl : (E1 ⋈ E2).l (inl e1) = E1.l e1 := rfl
@[simp] lemma merge_label_inr : (E1 ⋈ E2).l (inr e2) = E2.l e2 := rfl

def merge.assoc (E1 E2 E3) : (E1 ⋈ E2) ⋈ E3 ≃ₑ E1 ⋈ (E2 ⋈ E3) :=
{ order := order_iso.sum_assoc E1.evt E2.evt E3.evt,
  label := begin
    intro e, cases e, cases e, simp, simp, simp,
  end }

def merge.comm (E1 E2) : E1 ⋈ E2 ≃ₑ (E2 ⋈ E1) :=
{ order := order_iso.sum_comm E1.evt E2.evt,
  label := begin
    intro e, cases e, simp, simp,
  end }

def before (E1 E2 : evsys) : evsys :=
{ evt := E1.evt ⊕ₗ E2.evt,
  fin := sum.fintype E1.evt E2.evt,
  l := λ e, e.elim E1.l E2.l }

infix ` ▷ `:26 := before

/-- Lexicographical `sum.inl`. Only used for pattern matching. -/
@[pattern] abbreviation binl (x : E1.evt) : (E1 ▷ E2).evt := to_lex (sum.inl x)

/-- Lexicographical `sum.inr`. Only used for pattern matching. -/
@[pattern] abbreviation binr (x : E2.evt) : (E1 ▷ E2).evt := to_lex (sum.inr x)

@[simp] lemma before_label_inl : (E1 ▷ E2).l (binl e1) = E1.l e1 := rfl
@[simp] lemma before_label_inr : (E1 ▷ E2).l (binr e2) = E2.l e2 := rfl

def before_assoc (E1 E2 E3) : (E1 ▷ E2) ▷ E3 ≃ₑ E1 ▷ (E2 ▷ E3) :=
{ order := order_iso.sum_lex_assoc E1.evt E2.evt E3.evt,
  label := λ e, match e with
    | binl (binl e) := by simp
    | binl (binr e) := by simp
    | binr e := by simp
  end }

[Yaël Dillies]

Note that I made some changes to the rest of the file to show you mathlib style and some tricks. For example, you can use [] in the definition of evsys to make Lean automatically fill in fintype evt and partial_order evt through typeclass inference.

[Yaël Dillies]

Also, what's your end goal? Do you have a reference I can look at?

[Paul Rowe]

Thanks for the tips and the style advice! I will try to run with what you gave me. I'm especially happy with the type class inference allowing one to elide those fields when defining merge. I just had the linter generate the skeleton of the structure for me, so I dutifully filled in each field. I assume the type synonym makes type class inference fail for the before structure so the fin field is still required there?

As for my end goal, I'm sort of just playing around. But one relevant reference is here. The code above is mostly elaborating Definition 4 (with the observation that I assumed labeled DAGs in the paper, when I really want partial orders having a transitive edge relation).

[Yaël Dillies]

The fin field shouldn't be required but we're missing the trivial instance fintype α : fintype (lex α) (you can try to provide it yourself! It's really not hard). lex is a newborn, so expect such holes.

[Paul Rowe]

Hmm... I think I don't understand. I tried instance fintype_lex (h : fintype α) : fintype (lex α) := h which doesn't complain, but that doesn't allow me to erase the fin field in before. Anyway, it doesn't really matter. I can clearly get by without type class inference doing it for me. I'm mostly just viewing this an opportunity to learn more about these more subtle (to me) points of style.

[Yaël Dillies]

Ah of course, you used the wrong brackets. Here's what you should do:

instance lex.fintype {α : Type*} [fintype α] : fintype (lex α) := ‹fintype α› -- \fl and \fr for French quotes

Then it works.

[Paul Rowe]

Indeed it does! \fl \fr is new to me. But I should have thought of using [] in the context. Thanks again for all your help!

[Yaël Dillies]

I'm reading your article. There's a typo in definition 2. image.png
Should be $\ell_G(n) = \ell_H(\eta(n))$

[Yaël Dillies]

If we only allow injective homomorphisms, then the preorder is actually a partial order (up to isomorphism) because injective homomorphisms in both directions between (finite) graphs G and H imply that G and H are isomorphic

This is nontrivial, right? The injections don't have to cancel.

[Yaël Dillies]

Maybe I've done too much type theory but this doesn't typecheck. What do you mean? image.png
An illustration or two would clarify

[Bhavik Mehta]

I think that makes sense - take all the edges from E, and add in an edge from every vertex of G to every vertex of H, essentially unioning the complete bipartite graph's edges on

[Yaël Dillies]

That's what I thought too but it's written $E \cup((N_G \times \{0\}) \times (N_H \times \{1\}))$ not $E \cup((N_G \times \{0\}) \cup (N_H \times \{1\}))$. Maybe a typo?

[Bhavik Mehta]

No, the product is needed there - it doesn't make sense with a union!

[Yaël Dillies]

How come? This doesn't make sense with

E is the disjoint union of the edges of G and H

[Bhavik Mehta]

E should be a set of pairs of things from N, and N is a set of pairs. So (to put it in type theory terms like you mentioned) to make E' we need to have something which is a doubly nested pair, not a singly nested pair like in your example

[Yaël Dillies]

But N_G is already a set of pairs!

[Bhavik Mehta]

Not here it's not!

[Bhavik Mehta]

Look at the definition of E in the paper, each element is a pair of pairs (where the innermost left thing is from N_G or N_H), so the thing we're unioning should also be of that form

[Bhavik Mehta]

The set we're adding to E can also be written as {((x, 0), (y, 1)) | x \in N_G and y \in N_H}

[Yaël Dillies]

I'm not convinced by the product, but it's the disjoint sum of graphs with all cross edges added, right?

[Bhavik Mehta]

Yeah

[Paul Rowe]

Just catching up here. Bhavik is right that N_G is not (necessarily) a set of pairs here. It's really just the elements of the underlying type of G. Pairing with 0 and 1 is essentially acting as inl and inr. So the pair (e,0) is akin to inl e and (e,1) is akin to inr e. It's a sort of ugly thing you have to do if you view the underlying universes of G and H as sets and not types. If they are sets, then it might happen that those sets intersect (which, of course, doesn't happen if they are distinct types).

[Paul Rowe]

Ultimately, your sum.lex is a much cleaner way to do things.

[Yaël Dillies]

Ah I see! You're not actually after graphs, but rather orders.

[Paul Rowe]

Exactly. I didn't really have it clear in my mind when I wrote the paper.

[Paul Rowe]

The edges added to the graph will ensure that when you take the order defined by the transitive closure of the edge relation everything in G is less than everything in H.

[Yaël Dillies]

Okay, so is there any reason you're defining evsys fully bundled? You could probably get away with using

class evsys (α : Type*) :=
(l : α → ℕ)

[Paul Rowe]

Also, to your question above about it being a partial order when the maps are injective, you are right that it is non-trivial. I think it's essentially an instance of the Cantor-Schroeder-Bernstein theorem.

[Paul Rowe]

To be honest, I don't really know what I'm doing style-wise, so I'm trying things out in various ways. This also will fit into a larger structure that has additional constraints. (The codomain of \nat is artificial, by the way. It's just there to have a mwe without a bunch of extra stuff.)

[Yaël Dillies]

Ah okay! But the additional structures shouldn't stop you from using a less bundled approach.

[Paul Rowe]

Just to give you a flavor of some of the extra content (definitely not enough to compile):

@[simp]
def adversary_ordered {event : Type} [partial_order event] (ℓ : event → label)
(d : component → component → Prop): Prop :=
∀ e1 e2 c,
  rel ℓ d c e1 → rel ℓ d c e2 →
  adv_lab (ℓ e1) → (e1 < e2 ∨ e2 < e1 ∨ e2 = e1)

structure exec extends evsys :=
(d : component → component → Prop)
(adv_ord : @adversary_ordered evt poset l d)

[Paul Rowe]

Is there general advice on when to use bundled vs. not bundled? I'm really just feeling around in the dark until something works and doesn't get too much in the way when I am trying to prove what I want to prove.

[Yaël Dillies]

Yes there is. Overbundled things are hard to use because there's too little info on the outside. Underbundling is bad too, but in subtler ways (like the size of the terms Lean comes up with). I'd advise you to not bundle evt. The rest can stay the same.

[Paul Rowe]

Ok, that's good to know. Thanks for the advice!

Last night, I tried doing something more like:

class evsys (E : Type) extends partial_order E, fintype E :=
(l : E → label)

class exec (E : Type) extends evsys E :=
(d : component → component → Prop)
(adv_ord : adversary_ordered E l d)

and I got completely lost in figuring out how to get the type class inference stuff to just work. I'll try unbundling and see if it goes better.

[Yaël Dillies]

Ah, you almost got it right! Exposing E is good, but you shouldn't use extends here.

[Yaël Dillies]

I should be clearer. evsys shouldn't extend partial_order nor fintype (evsys can't be nicely inserted in the order hierarchy nor is a clear successor of fintype), but exec should extend evsys (they really are part of the same lineage).

[Paul Rowe]

Ok, so I should then include assumptions of the form [partial_order E] and [fintype E] when I need them?

[Paul Rowe]

Cool. Btw, I'm about to ghost you as I go into meeting. I'll circle back around later.

[Yaël Dillies]

Yeah, and you might sometimes need to upgrade to linear_order E. Then you'll thank the mixin :wink:

[David Wärn]

Maybe I misunderstood something, but Cantor-Schröder-Bernstein is usually trivial for finite things. If you have an injective graph homomorphism $f : H \to G$ then $G$ has at least as many vertices and edges as $H$. If you also have an injective homomorphism $G \to H$ then they must have the same number of vertices and edges, so $f$ must already be an isomorphism.

(Usually Cantor-Schröder-Bernstein fails for infinite "things with structure". For example there are order embeddings $[0, 1] \to (0, 1)$ and $(0, 1) \to [0, 1]$ but no isomorphism.)

[Paul Rowe]

Yes, you are correct. It is straightforward for finite things. I was never fully clear when I needed or wanted things to be a preorder or a partial order etc. I never ended up using the fact that the injective embeddings induces a partial order for the finite structures, so that particular comment is a bit of a dangling morsel with no follow up.

[Paul Rowe]

Ok, I'm still pretty confused. In the final definition below, I certainly need Evt to be an exec so that I have access to the d field. I can't figure out what to type so it doesn't complain.

-- Extract relevant things as constants for mwe
constant label : Type
constant component : Type
constant adversary_ordered (Evt : Type) [partial_order Evt] (l : Evt → label)
     (d : component → component → Prop) : Prop
constant rel {Evt : Type} [partial_order Evt] (l : Evt → label)
(d : component → component → Prop) (c : component) (e : Evt) : Prop
constant adv_lab : label → Prop

class evsys (Evt : Type) :=
(l : Evt → label)

variables {Evt : Type}

class exec [partial_order Evt] extends evsys Evt :=
(d : component → component → Prop)
(adv_ord : adversary_ordered Evt evsys.l d)

--These next two type check without error.
@[simp]
def adv_evt [evsys Evt] (e : Evt) := adv_lab (evsys.l e)

@[simp]
def adv_evts (Evt : Type) [evsys Evt] : set Evt :=
{ e | adv_evt e}

-- This gives an error: function expected at exec term has type Type
@[simp]
def relevant' [exec Evt] (c : component) (e : Evt) := by sorry

[Paul Rowe]

So apparently the following will work for the last definition:

@[simp]
def relevant' [po : partial_order E] [@exec E po]  (c : component) (e : E) :=
@rel E po evsys.l (exec.d E) c e

Clearly I can't let Evt be implicit in the definition of exec. For some reason I thought making explicit caused a different set of problems, but it seems good now.

[Yaël Dillies]

by sorry -> sorry btw

[Yaël Dillies]

Sorry, I was too slow to help. But your diagnosis was correct.

[Paul Rowe]

No apology needed! But while I have your attention, I have another style question. I assume I should avoid writing variables {Evt : Typ} [partial_order Evt] unless I really want to require every declaration to require a partial_order instance in the scope. Is that right?

[Paul Rowe]

Or less obviously, if I'm willing to assume that Evt will always be an evsys in the current scope, but will sometimes be upgraded to exec, is it bad form to declare variables {Evt : Type} [evsys Evt]? The declarations requiring exec Evt end up with a redundant requirement for an evsys Evt instance. This seems like it would be bad form. On the other hand, it can get tedious typing in the [evsys Evt] argument to every definition and lemma.

[Yaël Dillies]

Yes, this is pretty bad because [evsys E] [exec E] is declaring two unrelated evsys structures on E. My advice is to make

section evsys
variables [evsys E]
...
end evsys

section exec
variables [exec E]
...
end exec

and you can do similarly for order instances

[Paul Rowe]

That makes sense. Thanks again! I've learned so much more about Lean in the last two days.

[Yaël Dillies]

Reading some more, I think "Minimum experts required" and "Minimum attack time" are the width (minimum number of chains needed for a partition in chains) and height (length of the longest chain) of the order.

[Yaël Dillies]

I don't exactly know about "Guards needed to counter attack" and "Time required for all attacks".

[Yaël Dillies]

Also, your "covariant" and "contravariant" really are docs#monotone and docs#antitone

[Paul Rowe]

Regarding the language around "Minimum experts required" etc. you are right. I don't love that language, but I was borrowing it from the main reference on which the paper is based. I agree that width and height are simpler concepts, but in papers on security, you'd be surprised by what ends up being more intuitive for reviewers with a bias towards the applications.

[Paul Rowe]

And thanks for pointers to monotone and antitone. Those will certainly be handy later.

[Paul Rowe]

Oh, and now that I go back and look, "Minimum experts required" is really the smallest width among the set of orders that form the semantics of a term, and "Minimum attack time" is the shortest height. The other two take the widest and the tallest among the set of orders in the semantics.

[Paul Rowe]

So for example, if you need one guard to counter an attack on every "branch" of an order, the widest order will result in requiring the most guards.

[Yaël Dillies]

Okay, that's pretty cool!

[Yaël Dillies]

We don't have partitions in chains/antichains, so we don't have the width and height of an order. Incidentally, #11308 will allow talking about those in graded orders, but this isn't the greatest generality.

[Yaël Dillies]

Dilworth would be a cool milestone

[Paul Rowe]

I'm glad you're reading through the paper. You may be the only one besides the reviewers to have read it!

[Paul Rowe]

I had to just look up Dilworth's theorem. That does sound like a good milestone. Of course, if width and height of an order do show up soon, it would be nice to characterize the attribute domains explicitly as above. I don't think Dilworth would be required for that.

[Yaël Dillies]

I can cook up the definitions in a few days, but I think I've done already too many digressions in the past month to allow myself more non-uni work :confused:

[Paul Rowe]

Yeah, I hear you. My efforts to formalize this stuff are not really on the main path of my projects at work, but it's often more fun.

[Yaël Dillies]

Some people have written Lean formalization accompanying their maths paper. Maybe you could do something similar as an excuse for leaning? :grinning_face_with_smiling_eyes:

[Yaël Dillies]

"a notion of homomorphism on elements" shouts category theory!

[Paul Rowe]

In an earlier paper (reference [11] in the paper you are reading) we did exactly that but with Coq. In fact, the reason I know any Lean at all is that I ported the Coq code to Lean code in the summer of 2020 as a personal project. That was pretty much a "transliteration" without trying to improve on things. But if this stuff works out, we might be able to use it for future papers. fingers crossed

[Paul Rowe]

Yeah, do you know if the "homomorphism order" exists anywhere in mathlib? I'm scared to touch the category theory, but it does seem like the right level of abstraction.

[Yaël Dillies]

docs#preorder.small_category is the category associated to a preorder. I don't know whether we have the other way around (which Propifies the arrows) but I expect you might want to work with a category rather than an order?

[Yaël Dillies]

and docs#category_theory.sum is the sum of two categories.

[Paul Rowe]

It's so hard finding the right level of generality. I'm happy enough when I can get to prove what I need it to prove. :grinning:

[Yaël Dillies]

I don't know whether the lexicographic sum of categories is a thing however

[Reid Barton]

http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/join+of+categories

[Bhavik Mehta]

Yaël Dillies said:

docs#preorder.small_category is the category associated to a preorder. I don't know whether we have the other way around (which Propifies the arrows) but I expect you might want to work with a category rather than an order?

docs#thin_skeleton does something kind of similar to this? Given a category with homsets which are data but subsingleton, it makes them into Props and takes the quotient so you end up with a partial order