Order dual tactic

Stream: mathlib4

[Violeta Hernández]

I would imagine this has been discussed before but: is there any progress on a tactic alike to_additive that converts a theorem to its order-dual version?

[Violeta Hernández]

Something like:

import Mathlib.Order.SuccPred.Limit
open Order

@[to_order_dual] -- IsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a
theorem isSuccLimit_iff' [PartialOrder α] [OrderBot α] {a : α} :
    IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a :=
  isSuccLimit_iff

[Violeta Hernández]

@Yaël Dillies

[Yaël Dillies]

No more than last time, at least as much as I'm aware of. @Calle Sönne was interested in the category theoretical version but has since been plagued with painful wrists like me

[Eric Wieser]

One complication here is that you would expect it to sometimes reorder arguments

[Yaël Dillies]

And sometimes you want it to generate $2^n - 1$ lemmas for some $n > 1$

[Violeta Hernández]

I would imagine that even this basic version could already get rid of a lot of cruft throughout the library

[Violeta Hernández]

Other examples of order duals would include Sup and Inf, or IsMin and IsMax, or IsLUB and IsGLB, ...

[Bryan Gin-ge Chen]

I've started playing around with using the to_additive infrastructure to make an order_dual tactic in #21719. (#21696 is where I'm putting non-order_dual-specific changes to to_additive.) I'm a relative newcomer to metaprogramming, so I'd be happy to collaborate with anyone who's interested!

I'm currently stuck on a decidable instance which isn't getting translated:

application type mismatch
  ite (b ≤ a)
argument has type
  Decidable ((fun x1 x2 ↦ x1 ≤ x2) a b)
but function has type
  [h : Decidable (b ≤ a)] → α → α → α

[Damiano Testa]

I look forward to this very much! In my experiments, the main issue was generating the "correct" ordering of the variable names in the statements, plus some twisted difficulty with associativity for statements involving more than 2 elements.

[Bryan Gin-ge Chen]

Ah, sounds like your experiments may have proceeded farther than mine... if you've got any notes or old code still lying around I'd love to take a look.

[Damiano Testa]

I think that #12528 was one of the latest experiments that I had. It is not at all polished!

[Bryan Gin-ge Chen]

@Damiano Testa I had a quick look at #12528 and it looks like you implemented some useful functions! I'm still working on figuring out the to_additive machinery, but hopefully what you wrote can be plugged in somewhere...

[Bryan Gin-ge Chen]

As a general progress report, the very simple approach of just replacing the multiplicative->additive dictionaries with an order-dual dictionary and using to_additive's reorder to reverse the arguments of every ≤ in sight in #21719 is now stuck at LinearOrder.lean and WithBot.lean with different issues. I'll keep digging into what's going on so I can try to ask more focused questions later, but any experts with spare time are welcome to take a look and suggest / push fixes.

[Damiano Testa]

If I remember correctly, I did not hook into the to_additive machinery, but made a simple syntactic translation, so I think that your approach probably complements nicely the one that I had started.

[Damiano Testa]

I am definitely interested in this automation and I have had it in the back of my mind for a while: I'll help, but also do remind me, in case I get distracted by other projects! :smile:

[Bryan Gin-ge Chen]

I made some progress on understanding what is broken in LinearOrder.lean. It turns out the naïve approach of just swapping the arguments to ≤ is incompatible with the definition of max that we're using. Compare:

min := fun a b => if a ≤ b then a else b
max := fun a b => if a ≤ b then b else a

If we just swap the arguments of ≤, then min would get translated to:

max := fun a b => if b ≤ a then b else a

(which is actually what mathlib3 used up until mathlib3#17470).

Now if we change the definition of max back to this, then order_dual seems to work quite well translating theorems about min and max... until we try to define a linear order on the natural numbers, where all hell breaks loose because max is defined in core with the first definition -- which is of course the reason that we had to land mathlib3#17470 in the first place.

It is possible to manually apply the attribute to any lemmas whose proofs unfold max or min to ≤, so I'll try doing that next. I'm hoping we eventually get to a point where the max / min API gets sealed off and order_dual can take over.

[Mario Carneiro]

or maybe core just has the wrong definition of max

[Mario Carneiro]

and possibly things have changed enough that we can actually have the backport go the other way around

[Bryan Gin-ge Chen]

I haven't made it that much further yet but so far the min max messiness seems to be contained to a handful of lemmas.

[Mario Carneiro]

I mean sure we can keep working around this but I think the only reason we backported at the time was because core is annoying to PR to and it still kinda is but less so

[Mario Carneiro]

I'm almost certain whoever wrote that definition of max did not think about this issue at all and just wrote the first ordering that came to mind

[Bryan Gin-ge Chen]

My first reaction was certainly the same: wow things would be much cleaner if we just switched the definition back. But as I tag more and more lemmas with order_dual I'm less and less sure that I'm not just imposing my own arbitrary choices when I tell the tactic to re-order variables.

[Bryan Gin-ge Chen]

Today's progress update (all work can be found in #21719): As always, any feedback / questions here or on the PR is welcome!

I've now managed to tag most lemmas where the order_dual applies through the start of Order.Basic. Up to now I've been doing it all "by feel", so I think now is a good time to try and put the process into words, if just for my own benefit. So far most of the declarations order_dual has been applied to are just simple statements about < and ≤, with a few that mention min and max; I did do some tests with WithBot and WithTop as well, but maybe I'll talk about those in a later post.

First, everything starts at the top of Order.Defs.PartialOrder, where I decided that order_dual should transform a ≤ b to b ≤ a (and similarly a < b should be transformed to b < a, etc.):

attribute [order_dual existing (reorder := 3 4) LE.le] LE.le
attribute [order_dual existing (reorder := 3 4) LT.lt] LT.lt
attribute [order_dual existing (reorder := 3 4) GE.ge] GE.ge
attribute [order_dual existing (reorder := 3 4) GT.gt] GT.gt

Here you can see the use of to_additive's reorder option to swap the arguments of these functions.

Now that these have been registered, order_dual can transform theorems or defs that mention any of these functions to their dual versions, where "dual" just means that the LHS and RHS of every ≤, <, etc. in sight have been swapped. Note that a theorem like le_rfl : a ≤ a is manifestly self-dual so there's no reason to tag it with order_dual as the default behavior is to do nothing.

So now suppose we have a declaration where order_dual actually transforms it into something different. Consider the resulting dual declaration:

Case 1: Most of the time, the transformed version is just some slight variation of the original theorem that no one has needed up until now. For the time being, I'm manually naming these theorems as the original name + OD as a suffix:

@[order_dual le_of_lt_or_eqOD] -- {a b : α} (h : b < a ∨ a = b) : b ≤ a
lemma le_of_lt_or_eq (h : a < b ∨ a = b) : a ≤ b := h.elim le_of_lt le_of_eq
@[order_dual le_of_eq_or_ltOD] -- {a b : α} (h : a = b ∨ b < a) : b ≤ a
lemma le_of_eq_or_lt (h : a = b ∨ a < b) : a ≤ b := h.elim le_of_eq le_of_lt

It's a bit unfortunate that this leads to a bunch of new trivial theorems, but we need to add these variants so that order_dual will know how to transform the source theorems properly when they show up in proofs later on.

Case 2: Sometimes we get lucky and the transformed version of a theorem is secretly the same theorem except with some arguments permuted. In that case we just register the theorem as the dual version of itself with reorder:

@[order_dual existing (reorder := 3 4) lt_iff_le_not_le]
-- note that swapping the LHS and RHS of < and ≤ below yields:
-- b < a ↔ b ≤ a ∧ ¬a ≤ b
-- which is also what we get if we swap a and b
lemma lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a := Preorder.lt_iff_le_not_le _ _

Case 3: Sometimes we get even more lucky and the transformed theorem happens to be one that is proved later on in the file. This is the happy case where order_dual will let us delete lines of code (though I'm just commenting things out for now):

@[order_dual (attr := trans) gt_of_gt_of_ge]
lemma lt_of_lt_of_le (hab : a < b) (hbc : b ≤ c) : a < c :=
  lt_of_le_not_le (le_trans (le_of_lt hab) hbc) fun hca ↦ not_le_of_lt hab (le_trans hbc hca)

@[order_dual (attr := trans) gt_of_ge_of_gt]
lemma lt_of_le_of_lt (hab : a ≤ b) (hbc : b < c) : a < c :=
  lt_of_le_not_le (le_trans hab (le_of_lt hbc)) fun hca ↦ not_le_of_lt hbc (le_trans hca hab)

-- @[trans] lemma gt_of_gt_of_ge (h₁ : a > b) (h₂ : b ≥ c) : a > c := lt_of_le_of_lt h₂ h₁
-- @[trans] lemma gt_of_ge_of_gt (h₁ : a ≥ b) (h₂ : b > c) : a > c := lt_of_lt_of_le h₂ h₁

One thing that I've been treating inconsistently is whether I should identify variations that use ge and gt as the same as the ones with le and lt. Also, case is still relatively rare so far, but I expect that the proportion will be higher for pairs of theorems about min max top bot, etc. rather than these theorems about le and lt.

I think we eventually want special order_dual self syntax for order_dual to verify case 2, since it's easy to screw up the reordering. Also, it would be nice to have some automation to search for case 3 theorems as well, since searching for defeq theorems later in the file with a different name than expected is a bit annoying. Previously I was also trying to use reorder to try to match up the output of order_dual with later declarations, but I kept making mistakes, so I ended up undoing all of those and using reorder only when we get back the original declaration. Maybe there's some way to use automation here as well?

I haven't given much thought at all to how order_dual should be changing the names of theorems like these at all - this might help with identifying case 3 declarations. Right now, order_dual only knows to change min to max, bot to top, sup to inf, so theorems about lt and le just end up with the same name.

[Violeta Hernández]

(I don't mean to sidetrack you but my sincere thanks for this! It'll really come in handy in a lot of places)

[Violeta Hernández]

I think it's fine and even expected that lt and le should be kept the same. The only exception is when this would lead to the entire name being the same for two different theorems, which ime is where a lot of these ge/gt theorems come from.

[Violeta Hernández]

Are you planning to hit a certain tagging goal before PRing the tactic? I think it's important to have a working proof of concept before we get this into Mathlib, but tagging everything that could be tagged is complete overkill at this point.

[Bryan Gin-ge Chen]

Yeah, I’m not sure how far I should tag before cleaning up the tactic changes. I kind of want to see if I can get to lattices, but maybe it’s already useful enough?

[Bryan Gin-ge Chen]

(If anyone feels like pushing some commits tagging more lemmas and defs to my branch while I’m sleeping I certainly don’t mind!)

[Mario Carneiro]

Bryan Gin-ge Chen said:

Case 3: Sometimes we get even more lucky and the transformed theorem happens to be one that is proved later on in the file. This is the happy case where order_dual will let us delete lines of code (though I'm just commenting things out for now):

@[order_dual (attr := trans) gt_of_gt_of_ge]
lemma lt_of_lt_of_le (hab : a < b) (hbc : b ≤ c) : a < c :=
  lt_of_le_not_le (le_trans (le_of_lt hab) hbc) fun hca ↦ not_le_of_lt hab (le_trans hbc hca)

@[order_dual (attr := trans) gt_of_ge_of_gt]
lemma lt_of_le_of_lt (hab : a ≤ b) (hbc : b < c) : a < c :=
  lt_of_le_not_le (le_trans hab (le_of_lt hbc)) fun hca ↦ not_le_of_lt hbc (le_trans hca hab)

-- @[trans] lemma gt_of_gt_of_ge (h₁ : a > b) (h₂ : b ≥ c) : a > c := lt_of_le_of_lt h₂ h₁
-- @[trans] lemma gt_of_ge_of_gt (h₁ : a ≥ b) (h₂ : b > c) : a > c := lt_of_lt_of_le h₂ h₁

By the way, I don't exactly consider this example a win, the order_dual tactic produces a proof from scratch by "copy paste" while the original proof was much shorter because it's defeq to an existing lemma

[Mario Carneiro]

given the additional issue about gt here I would be enclined to just tag the latter lemma rather than trying to translate it

[Bryan Gin-ge Chen]

Yeah, that makes sense! This is along the lines of something I mentioned at the end of my message, but one thing about tagging lemmas after the fact with existing is that order_dual no longer goes through the proof and checks that things translate properly, so it's easy to accidentally add a tag that's nonsense. What I've been doing is temporarily generating a new lemma and then checking with an example that it is indeed defeq to the other declaration - it'd be nice if there was some kind of automated checking here (though I haven't thought through exactly what I want, I guess).

[Mario Carneiro]

Bryan Gin-ge Chen said:

but one thing about tagging lemmas after the fact with existing is that order_dual no longer goes through the proof and checks that things translate properly, so it's easy to accidentally add a tag that's nonsense

that sounds fixable? order_dual / to_additive should be able to validate these at attribute application time

[Kim Morrison]

Yes, we're open to change the definitions up in Lean, but I'd like to be presented with a "yes, it all works, including Mathlib, and people have signed off on the fact the change really makes tactic implementations easier" PR if possible. I don't have time to do this myself right now.

[Bryan Gin-ge Chen]

I finally found some time this week to come back to this and I've added the order_dual self syntax that I mentioned earlier, so tagging self-dual lemmas is now a lot less verbose.

I also attempted to add some validation for order_dual self and order_dual existing to check that the type of the declaration generated by order_dual (after variable reordering) is indeed defeq to the type of the original declaration itself (for self) or the type of the provided declaration (for existing), respectively. However, I'm getting mismatches where there just seems to be a difference in a universe variable:

order_dual failed validation!
tgt type:
∀ {α : Type u_2} [self : Preorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ c,
transformed type:
∀ {α : Type u_1} [inst : Preorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ c

The main validation code consists of these 8 lines or so, and I was already well outside my metaprogramming comfort zone when I wrote them, so there's probably some obvious mistake(s).

Before PRing, I also need to refactor things to separate out the parts of the code which are specific to to_additive, so I would appreciate it anyone has any suggestions on how to do this cleanly; more generally, any comments about the current state of the meta code are very welcome!

[Damiano Testa]

I do not know how AttrM works, but couldn't you try to combine the two MetaM.runs into a single one?

[Damiano Testa]

I think that the universe level information may be stored in the MetaM state somewhere and maybe the two runs do not keep track of the same assignments?

[Bryan Gin-ge Chen]

Thanks Damiano! However, I tried putting isDefEq into the same function that generates the order dual type in the next commit and unfortunately I'm still getting the same errors.

[Damiano Testa]

Ok, so maybe "manually" creating fresh (universe) metavariables before unification might help?

[Aaron Liu]

How does to_additive do it?

[Damiano Testa]

I'm not sure that to_additive has this check.

[Damiano Testa]

In fact, today I was goofing around and you can actually place multiple copies of the to_additive attribute on the same declaration and you get new "identical" declarations.

[Damiano Testa]

(You need to give them manually different names, though, since the environment catches the name clash otherwise.)

[Aaron Liu]

In that case I would instantiate one with universe variables and the other one with fresh universe metavariables, and do a defeq check on those. Then do it the other way around too to be safe.

[Bryan Gin-ge Chen]

OK, thanks! I guess the issue is the one that Kyle mentioned in #lean4 > Checking defeq in Command @ 💬 . Unfortunately his snippet starts with Names not Exprs. Is there an easy way to refresh universe metavariables in my use case?

For reference here's the current checking code (far from an MWE, see #21719):

def checkDeclType (b : BundledExtensions)
    (tgt : Name) (srcDecl tgtDecl : ConstantInfo) (reorder : List (List Nat) := []) :
    MetaM (Expr × Bool) := do
  let mut decl := srcDecl.updateName tgt
  if 0 ∈ reorder.flatten then
    decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
  let exp ← applyReplacementFun b <| ← reorderForall reorder
    <| ← expand b <| ← unfoldAuxLemmas decl.type
  return ⟨exp, ← isDefEq exp tgtDecl.type⟩

and I guess I need to do more setup with exp and tgtDecl.type before passing them to isDefEq.

edit: this was resolved in #metaprogramming / tactics > checking if two Exprs are defeq @ 💬

[Aaron Liu]

You can use docs#Lean.ConstantInfo.instantiateTypeLevelParams

[Damiano Testa]

If I understand correctly, Bryan wants to do this for the "new" expr, the one that does not have a corresponding declaration.

[Aaron Liu]

You can docs#Lean.ConstantInfo.updateType an existing declaration.

[Jovan Gerbscheid]

You mentioned having trouble with the order on WithBotand WithTop. Note that there is some ongoing work on refactoring these definitions at #19668, by @Yaël Dillies.

[Bryan Gin-ge Chen]

For the time being I've just turned the validation error into a logInfo so I can continue. Interestingly, I'm now seeing panics in later files coming from the reorderForall function where sometimes the validation function is sending an expression with too few arguments. So there's probably something else wrong in my approach here...

[Jovan Gerbscheid]

In the reorderForall function, you accidentally replaced mkForallFVars by mkLambdaFVars, which gives the mismatch.

[Bryan Gin-ge Chen]

Ah that was silly of me! Fixing that does get rid of most of the mismatches, but it looks like there are still two remaining coming from:

/-
reorderForall tried to reorder a list that was too small:
forall {α : Type.{u_2}} [self : LinearOrder.{u_2} α],
  DecidableRel.{succ u_2, succ u_2} α α (fun (x1._@.Mathlib.Order.Defs.LinearOrder._hyg.636 : α)
    (x2._@.Mathlib.Order.Defs.LinearOrder._hyg.636 : α) =>
  LE.le.{u_2} α (Preorder.toLE.{u_2} α (PartialOrder.toPreorder.{u_2} α (LinearOrder.toPartialOrder.{u_2} α self))) x1._@.Mathlib.Order.Defs.LinearOrder._hyg.636 x2._@.Mathlib.Order.Defs.LinearOrder._hyg.636)
#[_uniq.1658, _uniq.1659]
[[2, 3]]
-/
attribute [order_dual self (reorder := 3 4)] LinearOrder.decidableLE
/-
reorderForall tried to reorder a list that was too small:
forall {α : Type.{u_2}} [self : LinearOrder.{u_2} α],
  DecidableRel.{succ u_2, succ u_2} α α (fun (x1._@.Mathlib.Order.Defs.LinearOrder._hyg.661 : α)
    (x2._@.Mathlib.Order.Defs.LinearOrder._hyg.661 : α) =>
  LT.lt.{u_2} α (Preorder.toLT.{u_2} α (PartialOrder.toPreorder.{u_2} α (LinearOrder.toPartialOrder.{u_2} α self))) x1._@.Mathlib.Order.Defs.LinearOrder._hyg.661 x2._@.Mathlib.Order.Defs.LinearOrder._hyg.661)
#[_uniq.1691, _uniq.1692]
[[2, 3]]
-/
attribute [order_dual self (reorder := 3 4)] LinearOrder.decidableLT

in Order.Defs.LinearOrder.

If I had to guess, probably the functions from to_additive don't handle DecidableRel well?

[Jovan Gerbscheid]

A priori DecidableRel is not a forall. Only after unfolding it, does it become a forall (Luckily it is reducible, so in the reducible transparency it is a forall). So the fix is probably to replace some ForallTelescope by ForallTelescopeReducing. (And making sure you are in the reducible tranparency)

[Jovan Gerbscheid]

Although I'm not sure if reducing abbreviations is wanted in general. To avoid unnecessarily unfolding reducibles, you can use ForallBoundedTelescopeReducing (or something like that). This one only unfolds up to how many foralls you want to have.

[Jovan Gerbscheid]

I don't think I fully understand what the role/purpose is of reordering the arguments in LinearOrder.decidableLE. Can you explain why they should be swapped?

[Bryan Gin-ge Chen]

I can't say I fully understand it either, but without the reordering it seems like the instance doesn't apply when we need it to. Looks like the first failure is lt_trichotomy: (edit: let me look for the actual first failure...)

[Jovan Gerbscheid]

I looked at docs#Decidable.lt_or_eq_of_le, and I'm confused why this theorem exists, because it is weaker than docs#lt_or_eq_of_le. I thought mathlib was a classical mathematics library.

[Damiano Testa]

I think that it is a classical mathematical library outside the Decidable namespace.

[Ruben Van de Velde]

This theorem dates back to the core lean 3 repository. I'm not sure anyone would mind if it disappeared

[Bryan Gin-ge Chen]

OK, if I remove Decidable from the proof of lt_trichotomy, then order_dual (without reordering in LinearOrder.decidableLE) is happy with it, however things blow up just a little bit further below:

/-
application type mismatch
  dite (a ≤ b)
argument has type
  Decidable ((fun x1 x2 ↦ x1 ≤ x2) b a)
but function has type
  ∀ [h : Decidable (a ≤ b)],
    (a ≤ b → b < a ∨ a ≤ b) → (¬a ≤ b → b < a ∨ a ≤ b) → b < a ∨ a ≤ b
-/
@[order_dual lt_or_leOD]
lemma lt_or_le (a b : α) : a < b ∨ b ≤ a :=
  if hba : b ≤ a then Or.inr hba else Or.inl <| lt_of_not_ge hba

[Aaron Liu]

Can you show this with pp.explicit? The problem is in the invisible instance.

[Bryan Gin-ge Chen]

Sure, here you go!

application type mismatch
  @dite
    (Or (@LT.lt α (@Preorder.toLT α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) b a)
      (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b))
    (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b)
    (@LinearOrder.decidableLE α inst✝ b a)
argument has type
  Decidable
    ((fun x1 x2 ↦ @LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) x1 x2)
      b a)
but function has type
  ∀
    [h :
      Decidable (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b)],
    (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b →
        Or (@LT.lt α (@Preorder.toLT α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) b a)
          (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b)) →
      (Not (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b) →
          Or (@LT.lt α (@Preorder.toLT α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) b a)
            (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b)) →
        Or (@LT.lt α (@Preorder.toLT α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) b a)
          (@LE.le α (@Preorder.toLE α (@PartialOrder.toPreorder α (@LinearOrder.toPartialOrder α inst✝))) a b)

[Yaël Dillies]

It's the classic "(if a ≤ b then a else b) = (if b ≤ a then b else a) is not defeq", no?

[Aaron Liu]

I think the easiest way to fix this would just be to reorder the arguments to LinearOrder.decidableLE.

[Bryan Gin-ge Chen]

Right, the proof was working when attribute [order_dual self (reorder := 3 4)] LinearOrder.decidableLE was not commented out, so (as in the short version of the error) I think it's just that the known decidability of ≤ doesn't apply to (fun x2 x1 ↦ x1 ≤ x2).

[Aaron Liu]

It looks like you need to change these lines to a docs#Lean.Meta.forallBoundedTelescope.

[Bryan Gin-ge Chen]

Thanks! Looks like that worked. Now it's just the issue with the universe names confusing isDefEq.

[Jovan Gerbscheid]

In your implementation, you didn't pass a bound to forallBoundedTelescope, which kind of defeats the purpose of using forallBoundedTelescope over forallTelescopeReducing. You can instead pass it the bound reorder.flatten.max? (and if the Option value is none, then don't telescope at all, since there is nothing to reorder)

[Bryan Gin-ge Chen]

Makes sense! I guess I'll do the same thing with lambdaBoundedTelescope in reorderLambda.

[Jovan Gerbscheid]

Oh and I said earlier to use the reducible transparency, but I take that back, because now that we're using a bounded telescope, it will only reduce if explicitly told to do so. (Assuming you didn't modify the transparency yourself, it's set to default by default, so you don't need to change it)

[Bryan Gin-ge Chen]

Right, I didn't change the transparency at all.

Here's what I have now (I had to add a +1 to the bound but it works):

/-- Reorder pi-binders. See doc of `reorderAttr` for the interpretation of the argument -/
def reorderForall (reorder : List (List Nat) := []) (src : Expr) : MetaM Expr := do
  if let some maxReorder := reorder.flatten.max? then
    forallBoundedTelescope src (some (maxReorder + 1)) fun xs e => do
      if xs.size > maxReorder then
        mkForallFVars (xs.permute! reorder) e
      else
        dbg_trace "reorderForall tried to reorder a list that was too small:\n\
          {src}\n{xs}\n{reorder}"
        return src
  else
    return src

/-- Reorder lambda-binders. See doc of `reorderAttr` for the interpretation of the argument -/
def reorderLambda (reorder : List (List Nat) := []) (src : Expr) : MetaM Expr := do
  if let some maxReorder := reorder.flatten.max? then
    lambdaBoundedTelescope src (maxReorder + 1) fun xs e => do
      if xs.size > maxReorder then
        mkLambdaFVars (xs.permute! reorder) e
      else
        dbg_trace "reorderLambda tried to reorder a list that was too small:\n\
          {src}\n{xs}\n{reorder}"
        return src
  else
    return src

[Jovan Gerbscheid]

I would write "if xs.size = maxReorder + 1" (although this shouldn't change the effect of the code)

[Bryan Gin-ge Chen]

Is there a reason to prefer that over xs.size > maxReorder?

[Jovan Gerbscheid]

I think it makes it more readable, and it would throw an error if we accidentally passed the wrong bound to the bounded telescope

[Jovan Gerbscheid]

@Bryan Gin-ge Chen, I've had a look at the decidableLE issue, and one solution I've found is to define decidableGE, which is the dual of decidableLE, as follows:

abbrev DecidableGT (α : Type*) [LT α] := DecidableRel (fun a b : α ↦ LT.lt b a)
abbrev DecidableGE (α : Type*) [LE α] := DecidableRel (fun a b : α ↦ LE.le b a)

attribute [order_dual existing DecidableGT] DecidableLT
attribute [order_dual existing DecidableGE] DecidableLE

However, I think a cleaner solution would be to refactor DecidableLE to not be an abbrev, but instead a structure. Then we can tag its projection function with order_dual

[Bryan Gin-ge Chen]

Thanks for taking a look! Right, I thought briefly about having a dual class, but it does indeed seem messy. DecidableLE and friends are defined in core, right? I wonder if they had some specific reasons for making it an abbrev rather than a structure.

I also wonder if there's a way to use metaprogramming to have order_dual reorder the arguments to instances appropriately when the type contains ≤ or something else tagged with the "reorder" attribute.

[Jovan Gerbscheid]

Bryan Gin-ge Chen said:

I also wonder if there's a way to use metaprogramming to have order_dual reorder the arguments to instances appropriately when the type contains ≤ or something else tagged with the "reorder" attribute.

I presume you're talking about for example lt_or_eq_of_le, where order_dual gives the error

application type mismatch
  @dite (b < a ∨ a = b) (a ≤ b) (inst✝ b a)
argument
  inst✝ b a
has type
  Decidable (b ≤ a) : Type
but is expected to have type
  Decidable (a ≤ b) : Type

Although it is true that swapping a and b here solves the problem, I think this is hard to acomplish automatically. The same problem would be solved by either making decidableLE a structure, or giving it a dual decidableGE.

[Jovan Gerbscheid]

I think core only defined DecidableLE quite recently. Before that it was just DecidableRel LE.le (which would work better with order_dual). Anyways I think there is no real downside to defining DecidableLE as a structure.

[Bryan Gin-ge Chen]

Right, I see how making DecidableLE a structure or giving it a dual will solve the issue, but I'd like to better understand why it'd be hard to deal with instances automatically.

It's certainly out of reach of my current metaprogramming abilities, but doesn't something like the following algorithm work? Whenever the proof that we're dualizing contains an instance term, first dualize its type and note all reordered arguments, then use that to swap the arguments to the instance?

[Bryan Gin-ge Chen]

In any case, let's ping @Kim Morrison to see whether making DecidableLE a structure in core would be acceptable.

[Jovan Gerbscheid]

In the part where you say "first dualize its type", what exactly would decidableLE α be dualized to? I think in your model it wouldn't be dualized. So then "note all reordered arguments" would have to look at something else than the usual reorder

[Bryan Gin-ge Chen]

Ah, OK I see now. I was imagining that we could see through the abbrev, but obviously that doesn't happen for free...

[Aaron Liu]

Why doesn't reorder just work?

[Jovan Gerbscheid]

What @Bryan Gin-ge Chen wanted to do is reorder arguments a and b in inst b a. But inst is a local variable, so it cannot be globally tagged with reorder.

[Aaron Liu]

Just reorder on DecidableLE then, it's a @[reducible, inline] def defined in Prelude

[Aaron Liu]

or does that not work for some reason

[Aaron Liu]

Do it the same way you reorder LE.le

[Jovan Gerbscheid]

Which arguments of DecidableLE do you want to swap? It only takes 2 arguments: a type and an instance.

[Aaron Liu]

The third and fourth argument :)

[Aaron Liu]

wait, that doesn't work

[Aaron Liu]

hmmmmmm

[Aaron Liu]

I guess the best way to do this is to reorder inst

[Aaron Liu]

Since it's a local variable, it must have been introduced into the context at some point

[Aaron Liu]

Then you can just mark it as reorder when it's introduced

[Aaron Liu]

and that's based on the type

[Aaron Liu]

I guess this is the price you pay for having dependent types

[Aaron Liu]

Maybe this could be a new attribute? Something like type_reorder

[Jovan Gerbscheid]

I think this may cause some problems if you have both decidableLE and decidableRel LE.le. Because one of them gets dualized by swapping the arguments to the local instance, and the other by dualizing the type of the local instance. So we end up with two reducibly defEq expressions that get dualized to two non-defEq expressions. This could give rise to very obscure failures

[Aaron Liu]

oh, I can see how that could cause problems

[Bryan Gin-ge Chen]

Is there a library design constraint lurking here? Something more general than "don't use abbrevs to define classes if you want to be able to use order_dual".

[Jovan Gerbscheid]

What sort of constraint do you mean? In my experience, using abbrevs to define classes can lead to trouble, but it is convenient because it saves you from writing many instances.

I had a go at implementing DecidableLE as a structure, but to be able to use that, I think we'd need to rewrite all type class instances such as e.g. instance (a b : Int16) : Decidable (a ≤ b) into the form instance : DecidableLE Int16, which is kind of annoying to do for all of Lean and Mathlib.

On the other hand, using the abbrev DecidableGE isn't actually that bad, because type class search can automatically infer DecidableLE and DecidableGE from eachother.

[Bryan Gin-ge Chen]

OK, I was a bit hesitant to add another class, but if DecidableGE doesn't end up being too hard to work with then we can go with that. One minor downside is that theorems that use DecidableLE can't be self-dual anymore, but I don't think there are that many theorems which use DecidableLE anyways.

[Aaron Liu]

Can typeclass infer DecidableGE from DecidableLE?

[Jovan Gerbscheid]

Yes, because they unfold to ∀ a b, Decidable a ≤ b, and ∀ a b, Decidable b ≤ a respectively. And Lean introduces the ∀ variables as metavariables.

[Jovan Gerbscheid]

I made some progress using the approach with DecidableGE and pushed my changes. Some comments:

• When I write @[order_dual self (attr := simp)], does it apply the simp tag once or twice to the same lemma? I tried instead writing @[simp, order_dual self], but then the linter complains that it wants 'both' lemmas tagged with simp
• I generally prefer to not change statements of lemmas in the process of using order_dual. For example I noticed you set ge_trans to be the dual of le_trans, but this means that it is now defined in terms of ≤ instead of ≥. Instead, by reordering the arguments in the right way, le_trans and ge_trans can both be self-dual.

• I know there was the idea to change the definition of max or min in core to make it a bit more convenient for order_dual. But I think there is actually a good reason for the specific definitions in core, which is written in a comment at maxOfLe and minOfLe:
  -- Marked inline so that `min x y + max x y` can be optimized to a single branch.
  So I think the point is that min and max have the same condition so that using both of them together generates efficient code.

• To make tagging easier, would it be sensible to have special support for aliases? If A is an alias of B, then the dual of A should just be the dual of B.

• To make tagging easier, can there be a syntax (or lack of syntax) to indicate that the dual name should be the name followed by OD, if the name would otherwise be the same?

[Bryan Gin-ge Chen]

When I write @[order_dual self (attr := simp)], does it apply the simp tag once or twice to the same lemma?

Good question. applyAttributes and copyMetadata don't check if src and tgt are the same; is applying attributes not idempotent?

The other bullet points / suggestions sound good to me other than the last one. The OD suffix was basically me being lazy and putting off thinking about names, so I'm hesitant to make it a permanent default; I'm fine if we make it a temporary syntax / convention though (i.e. add a TODO in the comments).

[Aaron Liu]

I would suggest making better names, but if you're just testing and the names are temporary then I guess it's fine.

[Jovan Gerbscheid]

I think whether attribute application is idempotent depends on the implementation of that attribute, (i.e. does it use a HashSet or an Array)

[Jovan Gerbscheid]

For the names, the main case in which I didn't know how to do the naming is if the theorem contains both ≤ and =, like le_of_eq. Because the order dual swaps the arguments in ≤ but not in =, so it's almost the same theorem again. Do we pick a keyword to append to the name? Like le_of_eq_swapped?

[Jovan Gerbscheid]

Some more points:

• Attribute syntax: I noticed that the syntax of order_dual takes the arguments self, existing, (reorder := ..) and (attr := ..), in any order (and even multiple times). I think it would be nicer for consistency to pick one order and enforce that. I've been going for order_dual (self/existing)? attr? reorder? name?.
• Syntax hovering: it would be nice if the attribute syntax had better hover information. This should include an example of the attribute syntax and the required order of arguments (from the above point), and also the hover information for the attr := attributes. And more generally a basic explanation of order_dual.
• simp Iff lemmas: for iff lemmas tagged with simp, lean uses some weird auxiliary lemma instead of just applying prop_ext every time. I ran into this issue yesterday and I could solve it by squeezing the simp, but that isn't a nice solution.

[Yaël Dillies]

Jovan Gerbscheid said:

For the names, the main case in which I didn't know how to do the naming is if the theorem contains both ≤ and =, like le_of_eq. Because the order dual swaps the arguments in ≤ but not in =, so it's almost the same theorem again. Do we pick a keyword to append to the name? Like le_of_eq_swapped?

Naming convention is ge_of_eq

[Jovan Gerbscheid]

Do you mean that out of these three

le_of_eq : a = b → a ≤ b
le_of_eq' : a = b → b ≤ a
ge_of_eq : a = b → a ≥ b

the middle one should be called ge_of_eq?

[Jovan Gerbscheid]

le_trans' : b ≤ c → a ≤ b → a ≤ c
ge_trans : a ≥ b → b ≥ c → a ≥ c

These two lemmas both exist, but your convention seems to imply le_trans' should be called ge_trans?

[Edward van de Meent]

actually, in my opinion that one should be le_comp

[Edward van de Meent]

since it's precisely the difference between comp and trans, applied to le

[Jovan Gerbscheid]

So would you suggest removing the current ge_trans in favour of the current le_trans'?

[Edward van de Meent]

i don't see why yet

[Jovan Gerbscheid]

I find it a bit confusing with the ≤ vs ≥ notation and le vs ge naming. For the notation, appart from a few exceptions, we always use ≤. And I thought that this should be reflected in the name: always use le for ≤. But @Yaël Dillies is suggesting to use ge in the name for ≤ if the lemma is generated by the order dual tactic. Don't you think that this would be very confusing?

[Edward van de Meent]

yes. i guess the issue is that in our typical naming scheme, we hardly track where which free variables end up, which is typically precisely the difference between le and ge

[Yaël Dillies]

Jovan Gerbscheid said:

@Yaël Dillies is suggesting to use ge in the name for ≤ if the lemma is generated by the order dual tactic. Don't you think that this would be very confusing?

No, this is not the naming convention. The naming convention is approximately

1. Turn foo_le_bar into bar_le_foo
2. If that fails (because eg foo = bar or there is another ambiguity), instead replace le with ge

[Jovan Gerbscheid]

So far I'm mostly looking at lemmas where the two sides of le are free variables, so point 1 doesn't apply.

[Yaël Dillies]

Then le → ge it is. But I must warn you that point 1 really is the one that applies most often in practice

[Yaël Dillies]

(I know it makes the naming algorithm much harder, there's a reason why I failed to write to_dual for several years!)

[Edward van de Meent]

i guess it might be best if we can reserve an option to explicitly name the dual lemma?

[Jovan Gerbscheid]

Oh right, should we call it to_dual instead of order_dual? It is really about any kind of dual.

[Jovan Gerbscheid]

Yes, we can choose to override the the automatically generated name for the dual lemma

[Yaël Dillies]

Yes, eg @Calle Sönne is hoping to steal all your work on this tactic and apply it to category theory :smile:

[Jovan Gerbscheid]

Ok, I'll make a PR to clean up some of these lemmas to use the gt and ge naming, but using < and ≤. But first I have #24277 to remove some @[trans] annotations.

[Bryan Gin-ge Chen]

If we want to_dual to dualize both order-theoretically and category-theoretically at the same time, then it might already be possible to start tagging theorems now with the current state of the attribute.

[Jovan Gerbscheid]

Some of the changes to the to_additive infrastructure should probably be PR-ed before to_dual itself. Your check that to_additive existing does the correct thing is very useful, and will probably find some mistakes in mathlib. (In fact I found one by accident here #24283).

Additionally I think reorderForall and reorderLambda should throw an error if the permutation numbers are out of bounds.

[Jovan Gerbscheid]

@Yaël Dillies, I'm trying to replace lemmas about > with lemmas about <, but still calling them gt when appropriate. Do you think the following lemmas should use ge/gt in the name?

lt_or_le (a b : α) : a < b ∨ b ≤ a
lt_or_lt_of_ne (h : a ≠ b) : a < b ∨ b < a

the naming conventions seem to suggest the names I wrote, but the names lt_or_ge and lt_or_gt_of_ne also seem natural.

[Yaël Dillies]

Both pairs of names are fine (and possibly we should have both)

[Yaël Dillies]

cf docs#le_or_lt

[Jovan Gerbscheid]

Do you also think Ne.lt_of_le' : b ≠ a → a ≤ b → a < b should be renamed to Ne.gt_of_ge?

[Yaël Dillies]

This one is a bit tougher in the sense that I think of it as having the != reversed, not the <= and <

[Jovan Gerbscheid]

I have tagged a bunch of category theory results now with order_dual. I ran into a few issues:

• Applying attributes in the case of order_dual self. I write @[simp, order_dual self (reorder := ..)], but the linter complains that it wants @[order_dual self (attr := simp) (reorder := ..)]. So if we want the first form, then we should change the linter to complain about the second option instead of the first.
• Higher order functions. A few functions require swapping arguments inside an argument in order to be order_dual to themself, such as Prefunctor.mk {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (obj : V → W) (map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)) : V ⥤q W (need to swap X and Y). I could imagine extending the reorder syntax to support this, but that seems overly complicated, and otherwise we can just have such constants not be self-dual.
• IsThin suffers the same problem as decidableLE, so we get the dual IsThin' which is equivalent to IsThin.
• When tagging a structure projection function with order_dual (reorder := ..), the reordering doesn't apply if the projection is in the form of an Expr.proj. So I think we need to refold all of the Expr.proj expressions into their projection functions before transforming the expression. This comes up because the reassoc attribute creates such proof terms.

[Jovan Gerbscheid]

I noticed there is a special meaning when the number 0 appears in the reorder := .. syntax, which swaps the order of the first two universe variables. I think this is very confusing, and it isn't used or documented anywhere. Should we remove it?

[Jovan Gerbscheid]

Have you considered using == instead of isDefEq to check that the generated and actual order dual expressions are the same? I would expect that they should satisfy ==.

[Bryan Gin-ge Chen]

Jovan Gerbscheid said:

I noticed there is a special meaning when the number 0 appears in the reorder := .. syntax, which swaps the order of the first two universe variables. I think this is very confusing, and it isn't used or documented anywhere. Should we remove it?

I didn't realize this was unused. Maybe @Floris van Doorn has an opinion on this? (It seems the feature was added along with the reorder syntax in !3#7888)

[Bryan Gin-ge Chen]

Jovan Gerbscheid said:

Have you considered using == instead of isDefEq to check that the generated and actual order dual expressions are the same? I would expect that they should satisfy ==.

I didn't consider it at all -- do you think it'd be beneficial? I can test it out when I have a chance, but if you're currently hacking on order_dual, maybe you're better poised to do so at the moment. I'd be interested to know the results.

[Jovan Gerbscheid]

I also renamed it to to_dual just now :grinning:

[Jovan Gerbscheid]

Ah actually I got confused about the off-by-one property of reorder. So what happens is that if reorder := .. contains a 1, then it reorders the first two universe variables, which is required for HPow -> HSMul.

[Jovan Gerbscheid]

But I do think this could lead to surprising behaviour, as it is a hack.

[Jovan Gerbscheid]

I tried using ==, which works fine. The change made it so that LinearOrder.toDecidableLE can't be self dual, but that is fine, as we can define LinearOrder.toDecidableGE. I also discovered the following weird universe thing in the process:

run_meta do -- (α : Type u) → [inst : LT α] → Type (max 0 u)
  let info ← Lean.getConstInfo ``DecidableLT
  Lean.logInfo m! "{info.type}"

Anyways, we do need a way to turn off the verification with syntax like self! or existing! (which I saw you suggested in a comment). The place where verification breaks is the constructor CategoryTheory.Iso.mk, where we need to swap the fields hom_inv_id : hom ≫ inv = 𝟙 X := by aesop_cat and inv_hom_id : inv ≫ hom = 𝟙 Y := by aesop_cat, but the two by aesop_cat autoParams aren't == to eachother (which is a bit unfortunate)

[Jovan Gerbscheid]

I made a PR (#24401) that introduces to_dual's verification step into to_additive, and I had to fix around 20 files where warnings were shown.

[Jovan Gerbscheid]

Also, my PR refactoring order lemmas is now at the new #24396, because in the previous PR it was getting unmanageable to fix all of the broken proofs. So instead I've added the old names as aliases, with a TODO to deprecate them.

[Floris van Doorn]

Bryan Gin-ge Chen said:

Jovan Gerbscheid said:

I noticed there is a special meaning when the number 0 appears in the reorder := .. syntax, which swaps the order of the first two universe variables. I think this is very confusing, and it isn't used or documented anywhere. Should we remove it?

I didn't realize this was unused. Maybe Floris van Doorn has an opinion on this? (It seems the feature was added along with the reorder syntax in !3#7888)

Oh, I thought I had documented that.
It is definitely used in to_additive. The universes have to be reordered correctly as well, and as a hack, I only implemented the following case: if the first two arguments are reordered, to_additive assumes that both of them are types, and then also reorders the first two universe levels. This is a very common scenario, and was necessary for many lemmas to_additive generates with the reorder option. Not reordering them would cause failures when declarations using the faulty one are additivized.
Of course, this is a hack. Feel free to implement a more robust solution.

[Floris van Doorn]

Oh, I now read further and see that Jovan also realized this.

[Jovan Gerbscheid]

(Note that the universes are swapped when doing any permutation involving the first argument, not just a swap with the second argument)

[Jovan Gerbscheid]

Should we use export LinearOrder (le_total min_def max_def) instead of having two identical lemmas in the root and LinearOrder namespaces? The duplication is a bit annoying for tagging.

[Yaël Dillies]

Jovan Gerbscheid said:

Should we use export LinearOrder (le_total min_def max_def) instead of having two identical lemmas in the root and LinearOrder namespaces? The duplication is a bit annoying for tagging.

It's useful to not use export because then the lemmas show up under the expected name in the docs (hopefully doc-gen can be fixed to avoid needing this hack)