Multiple orders on the same type

Stream: general

[Michael Stoll]

Say, I have a type like fin n → ℕ and want to work with two different partial orders (say, the product order and the lexicographic order) on this type at the same time (e.g., to prove that a ≤prod b implies a ≤lex b [fixed this]). Is there a recommended way of doing this?

[Johan Commelin]

Probably it is best to use a type synonym.

[Johan Commelin]

I guess the default one is the product order?

[Johan Commelin]

Does docs#lex lead to a useful type synonym?

[Damiano Testa]

And maybe docs#pi.to_lex_monotone?

[Damiano Testa]

If n is non-zero, then there is also docs#finsupp.lex which may or may not be better to use! :upside_down:

[Yaël Dillies]

Oh wait, Damiano, did you introduce a new type synonym rather than using lex (α →₀ β)?

[Damiano Testa]

I did. I thought that the one you had for pi used some wf stuff that was not needed for the one on finsupp. Maybe this is a wrong reason?

[Junyan Xu]

a ≤lex b implies a ≤prod b

Backwards?

In case you really want relations on the same type: in e.g. docs#prod.rprod_sub_lex the relations are referred to explicitly; you may declare local notation for them for convenience. Instead of using docs#has_le.le_trans etc. you may have to use docs#is_trans.trans from a docs#is_partial_order instance.

[Junyan Xu]

lex (α →₀ β)

What does this even mean? Which lex makes this type check?

[Yaël Dillies]

docs#lex is a general type synonym. lex (Π i, α i) is the lexicographic pi type, and I meant lex (ι →₀ α) to mean the lexicographic finite supported functions.

[Junyan Xu]

Damiano Testa said:

If n is non-zero, then there is also docs#finsupp.lex which may or may not be better to use! :upside_down:

Why n nonzero makes a difference for whether to use pi or finsupp? I think if n=0 both pi.lex and finsupp.lex are not reflexive.

[Yaël Dillies]

The point of a single type synonym is that you can carry over everything you don't care about. You don't want to write #16122 for each lexicographic type synonym :wink:

[Damiano Testa]

@Junyan Xu I just wanted to point out that fin n -> anything is automatically a finsupp only when n = 0.

@Yaël Dillies maybe I can remove the finsupp.lex definition. Is this what you are saying?

[Yaël Dillies]

Hmm, it's automatically a finsupp for all n because fin n is always a fintype, right?

[Damiano Testa]

Also fin 0?

[Junyan Xu]

docs#finsupp.equiv_fun_on_fintype (a bit hard to find!)

[Damiano Testa]

I know that I am always confused about this... fin 0 is empty, while zmod 0 is int?

[Damiano Testa]

Ok, my last comment makes sense. Yes, fin n should always be a fintype!

[Junyan Xu]

Damiano Testa said:

Yaël Dillies maybe I can remove the finsupp.lex definition. Is this what you are saying?

Should we use lex for docs#pi.lex as well?

[Damiano Testa]

Ok, so lex is a "blanket" synonym, that will have all the whatever-lex-order-you-can-think-of instances, right?

[Michael Stoll]

What I actually have is a preorder on fin n → ℕ obtained by pulling back a partial order under a map and the product order. I just want to be able to talk about both of them. Right now, I define

def weight (n d : ℕ) : Type := fin n.succ → ℕ
def f (w : weight n d) : blah := ...
instance preorder : preorder (weight n d) := preorder.lift f
infix ` ≤d `:50 := @has_le.le (weight _ _) _
infix ` ≤c `:50 := @has_le.le (fin _ → ℕ) _

This allows me to use notation for the two different (pre)orders. But in the infoview, both are just printed as ≤, which can be confusing.

[Junyan Xu]

Oh wait, it turns out we are already using docs#lex for the type carrying pi.lex and finsupp.lex. pi.lex and finsupp.lex operate on the relations instead. Sorry for the confusion!

[Damiano Testa]

Yes, I got confused as well. I did not introduce a new type synonym, I introduced the relation docs#finsupp.lex, analogous to the relation docs#pi.lex as an instance on the same type synonym docs#lex.

This and fin 0 caused a short circuit in my brain!

[Yaël Dillies]

Ah great! That's what I was hoping for.

[Damiano Testa]

After having derailed Michael's question, let me go back to it.

I think that it will be clearer, in the long run, to have the two instances defined on different-but-synonymous types. In your case, the two types are fin n.succ → ℕ and weight n.

You have one Type X with its order and a copy of X like your weight n with the other order. You give names to the identity maps to weight n and from weight n and you pretend that they are different. You then prove lemmas about monotonicity of these maps (like docs#pi.to_lex.monotone) or whatever you want to prove. It is a little laborious, but having two orders on the same type is ultimately very confusing.

It is possible that the notation can help to avoid this, especially if you only need very limited interaction between the types. But anything more substantial will likely be easier with type synonyms with different order instances.