!4#3360 OrderDual

Stream: mathlib4

[Jon Eugster]

Could somebody look at my hack here:

https://github.com/leanprover-community/mathlib4/pull/3360/commits/d13b8a047372cef061fdeec692059ca1100216ca#r1181537830

This changes seemingly

↑toDual s.toProd.fst ≤ ↑toDual b.toProd.fst

to

↑toDual b.toProd.fst ≤ ↑toDual s.toProd.fst

and while this works as it changes some hidden OrderDual α to α (and the corresponding LE instance), I think there is a lot of potential for improvement with the current OrderDual API. Maybe somebody who knows OrderDual better could try to golf that hack and give an educated opinion on what would need to be done here to make working with OrderDual more pleasant.

[Yaël Dillies]

What exactly is the problem? Is it that Lean unifies things wrongly?

[Yaël Dillies]

Have you tried doing @lemma αᵒᵈ (_) _ _ (with some combination of _ and (_) to be figured out)?

[Yaël Dillies]

The API for OrderDual is pretty much optimal with regards to Lean 3. It seems that Lean 4's new unification algorithm is throwing a massive wrench in the gears by preventing us from using our type synonyms to dualise lemmas. The better solution would be a dedicated dualisation tactic, but that's yet to be written.

[Yaël Dillies]

What are you finding sketchy about the API?

[Jon Eugster]

I think it's just the problems caused by the new lean 4 unification algorithm I experienced here.

The porting comment saying "sketchy" was before I realized what's happening and a.toProd ≤ b.toProd → b.toProd ≤ a.toProd seemed quite odd. I'll change that comment.

[Jon Eugster]

The lean3 proof here had basically the following three assumptions (in lean4 names)

h₁: (NonemptyInterval.toDualProd s).fst ≤ (NonemptyInterval.toDualProd b).fst
h₂: (NonemptyInterval.toDualProd s).snd ≤ (NonemptyInterval.toDualProd c).snd
h₃: s.toProd.fst ≤ s.toProd.snd

and then h₁.trans (h₃.trans h₂) was a proof of type b.toProd.fst ≤ c.toProd.snd, so there were a lot of implicit things going on there that don't work anymore now. It took me a while to figure out what steps where supposed to happen.

[Yaël Dillies]

Have you tried inserting docs4#OrderDual.toDual_le_toDual or docs4#OrderDual.ofDual_le_ofDual in the correct places?

[Yaël Dillies]

Those are type-correct versions of your OrderDual.le_def

[Eric Wieser]

The general rule in lean 3 was never to use defeq abuse in lemma statements, but to allow it in super-golfed proofs

[Jon Eugster]

Thanks @Yaël Dillies ! That'sthe lemma I was missing

[Kevin Buzzard]

Yes, porting sometimes indicates Lean 3 proofs which strictly speaking shoudln't typecheck, and only do because of definitional abuse.