orderDual defeq abuse

Stream: mathlib4

[Kim Morrison]

We still have quite a number of places in Mathlib where we are abusing the defeq of OrderDual.

One that I ran into today was docs#Dense.borel_eq_generateFrom_Ioc_mem_aux. Would anyone be interested in taking a look?

[Kim Morrison]

The first convert can be improved to

  convert hd.orderDual.borel_eq_generateFrom_Ico_mem_aux (by simpa using hbot)
    fun x y hlt he => hIoo (ofDual y) (ofDual x) hlt _ using 2

but this is still not right.

One can put seal OrderDual in above the declaration to ensure that defeq abuse is avoided! :-)

[Wrenna Robson]

I kept hitting this today. OrderDual is just very annoying to work with.

[Wrenna Robson]

What does "seal" do?

[Wrenna Robson]

One issue is tbf I constantly find myself wishing for a type that represents order-reversing homomorphisms (and isomorphisms).

[Wrenna Robson]

We generally define these using OrderDual but it somewhat funnels you into accidentally defeq abusing.

[Junyan Xu]

I thought defeq abusing OrderDual in proofs is a feature not a bug ...

[Wrenna Robson]

I just had an issue with using PartialOrder.lift where even when putting in ofDual explicitly it lifted the wrong order.

[Wrenna Robson]

Junyan Xu said:

I thought defeq abusing OrderDual in proofs is a feature not a bug ...

I think of it as a cowboy era thing in some ways.

[Wrenna Robson]

I think in an ideal world OrderDual would be a one-element structure.

[Wrenna Robson]

The issue is it encourages things like (OrderDual (OrderDual (a)) = a. And that's inherently a bit evil.

[Junyan Xu]

Yeah the instances on αᵒᵈᵒᵈ are the same as (I mean defeq to) those on α. Is there an example of abusing this in defs in mathlib?

[Yaël Dillies]

Junyan Xu said:

the instances on αᵒᵈᵒᵈ are the same as those on α

This is unfortunately wishful thinking, and some operations disagree, but there are so few that I can't even remember a single one off the top of my head

[Kenny Lau]

how can they disagree if Xdd is isomorphic to X

[Wrenna Robson]

Isomorphism is not equality.

[Yaël Dillies]

Equality is not definitional equality

[Jovan Gerbscheid]

We will need to use OrderDual a lot less once the to_dual attribute makes it to mathlib.

[Wrenna Robson]

What will that attribute do?

[Jovan Gerbscheid]

It is very similar to @[to_additive], which takes a theorem, replaces every * with a + where appropriate, and produces a proof of the translates version by translating the original proof. Instead, @[to_dual] will replace every a ≤ b with b ≤ a where appropriate, and dualize whatever can be dualized, e.g. max → min.

[Wrenna Robson]

Right. But that wouldn't let you avoid the use of it for e.g. defining an order-reversing map.

[Jovan Gerbscheid]

Exactly, but I would expect that those kind of uses don't do much defeq abuse.