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)

[Jovan Gerbscheid]

I have fixed the merge conflicts in the to_dual PR (#21719), and I've made a new PR to to_additive to define the to_additive self syntax (#27387).

Here at the Class Field Theory formalization event, some people would like to have the to_dual attribute for homology and cohomology.

[Bryan Gin-ge Chen]

The way I structured the to_dual PR was to have it depend on #21696 which starts to split up the to_additive code into bits that can be re-used by to_dual. Should we make an effort to revive that one too or should we just try and merge #21719 all in one go? I'll see if I can make some time to work on to_dual / review related PRs this week; just ping me or DM me if you have some tasks I can help with.

[Jovan Gerbscheid]

I think we can merge it all in one go, but I don't really mind.

[Jovan Gerbscheid]

I think in an ideal world, it would be possible to declare a new translation attribute with a one-liner. And then we would do this for to_additive and for to_dual. This would require an extra argument isDual : Bool which determines whether to add a reverse translation for every given translation.

[Jovan Gerbscheid]

Jovan Gerbscheid said:

I think we can merge it all in one go, but I don't really mind.

Although I am trying to PR independent features one-by-one whenever possible, to reduce the size of the final PR.

[Jovan Gerbscheid]

Thanks for the quick review! Here is another PR that ports a fix from the to_dual PR: #27405

Another thought: to_dual and reassoc have a funny interaction. For lemmas currently tagged @[reassoc] that we want to tag with to_dual, we want the lemma and its dual to have a reassoc version. But those are not dual to eachother, so we will need to add their duals as well. So we end up with 6 lemmas. So I guess we should define some @[to_dual_reassoc] for this, which adds both the _assoc and _assocRev lemmas.

[Jovan Gerbscheid]

In #21719, I have now split out the to_dual code into a separate file, so that ToAdditive.Frontend is changed as little as possible. It is now mostly ready to be PR-ed :tada:. I think the PR will have to contain only a little bit of tagging things with @[to_dual], and we can leave the rest for future PRs.

One more TODO is to fix the error messages. It currently will tell you that "to_additive failed" even though you actually used to_dual. I'm less worried about trace messages and comments in the code mentioning to_additive.

Another TODO is to figure out how to deal with associativity of composition in category theory, and the reassoc attribute. But that question doesn't need to block to_dual from being used for order theory.

[Bryan Gin-ge Chen]

Thanks so much for your work on this Jovan! I'll try and take a look at this in the next few days and maybe knock off some of the TODOs, unless you're still planning on making more big changes.

[Violeta Hernández]

I wasn't aware that this was still being worked on! What's the progress status?

[Jovan Gerbscheid]

The progress status is that essentially all the prerequisites are now in place: to_additive existing now has a check in place to verify that the attribute can be applied. We now have the to_additive self syntax as a special case of existing. The new naming converntion for le/ge has been applied.

In #21719, I've also been tagging a bunch of lemmas about orders, and category theory. This can be ported in later PRs, but there will still be a lot more tagging to do.

[Jovan Gerbscheid]

I made a new PR for the to_dual attribute in #27887, and it is now ready for review! It only adds @[to_dual] tags in files that directly need to import ToDual, namely Order/Defs/PartialOrder, Order/Notation and Combinatorics/Quiver/Basic.

When this gets merged, we will have to figure out how to best review PRs that expand the use of to_dual.

• Reviewing tags of the form to_dual self (reorder := ...) or to_dual existing (reorder := ...) is easy, because the attribute checks automatically that the reorder argument is correct.
• But for to_dual (reorder := ...), it is much trickier to check that the generated lemma matches the original lemma. And I don't know if we even want it to become exactly the same; do we care about the order of implicit arguments?

[Bryan Gin-ge Chen]

If when we tag, we always start by trying to_dual existing (reorder := ...) original_lemma, and then only delete original_lemma afterwards, then we can take advantage of the checking, right? I guess this doesn't make it easy for reviewers to check unless we require separate commits.

[Jovan Gerbscheid]

The to_dual PR has been merged!

Now, I'd like people's opinion on #31722, where I change the (reorder := ...) notation to use 0-indexed counting instead of 1-indexed counting. Personally, I would have expected this to use 0-indexed counting. But if people prefer counting that starts at 1, let me know.

[Bryan Gin-ge Chen]

/poll How should the (reorder := ...) notation be indexed?

[Bryan Gin-ge Chen]

Are there any other tactics that have syntax for refering to arguments by position?

The only one that comes to my mind isn't a real example: nth_rewrite is apparently 1-indexed, but that's for the nth occurrence of some expression in the rewrite target, not for counting arguments.

[Jovan Gerbscheid]

There is the @[specialize] compiler attribute, which allows you to specify arguments by name or by index, and the number is 1-indexed.

[Jovan Gerbscheid]

There is also the conv mode syntax that uses numbers to specify which argument to zoom into. But in that case, 0 refers to the head function, and then the arguments are counted from 1.

[Kevin Buzzard]

If you want more opinions then you might want to give an example or two of current behaviour, I have no idea what this question is about but I could imagine having an opinion if i saw some examples

[Jovan Gerbscheid]

Here are some examples, using the current 1-indexed counting.

swapping `a ^ n` into `n • a`.
attribute [to_additive existing (reorder := 1 2, 5 6) hSMul] HPow.hPow

@[to_additive (reorder := 5 6) smul_apply] -- swapping f and a
lemma pow_apply [∀ i, Pow (M i) α] (f : ∀ i, M i) (a : α) (i : ι) : (f ^ a) i = f i ^ a := ...

-- turning `a < b` into `b < a` etc.
attribute [to_dual self (reorder := 3 4)] LE.le LT.lt GE.ge GT.gt

@[to_dual self (reorder := 3 4)] -- swapping a and b
lemma lt_or_ge {α : Type*} [LinearOrder α] (a b : α) : a < b ∨ b ≤ a := ...

@[to_dual self (reorder := 3 4, 5 6, 9 10)]
lemma homOfEq_eq_iff {V : Type*} [Quiver V] {X Y X' Y' : V}
    (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') :
    Quiver.homOfEq f hX hY = g ↔ f = Quiver.homOfEq g hX.symm hY.symm := ...

[Jovan Gerbscheid]

I wonder whether it would be helpful to also allow referring to the arguments by name. This would probably make it easier, but there could also be a cost to having multiple ways of saying the same thing.

[Kevin Buzzard]

You are counting things, so shouldn't this start at one? For example in homOfEq_eq_iff I'm sure you would accept that you're talking about the 3rd, 4th, 5th, 6th, 9th and 10th inputs to the function

[Robin Arnez]

It would probably be simplest if you could also refer to the names of parameters instead of counting them, similar to how @[specialize] does it, so you would do:

attribute [to_additive existing (reorder := α β, 5 6) hSMul] HPow.hPow

@[to_additive (reorder := f a) smul_apply]
lemma pow_apply [∀ i, Pow (M i) α] (f : ∀ i, M i) (a : α) (i : ι) : (f ^ a) i = f i ^ a := ...

-- turning `a < b` into `b < a` etc.
attribute [to_dual self (reorder := 3 4)] LE.le LT.lt GE.ge GT.gt

@[to_dual self (reorder := a b)]
lemma lt_or_ge {α : Type*} [LinearOrder α] (a b : α) : a < b ∨ b ≤ a := ...

@[to_dual self (reorder := X Y, X' Y', hX hY)]
lemma homOfEq_eq_iff {V : Type*} [Quiver V] {X Y X' Y' : V}
    (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') :
    Quiver.homOfEq f hX hY = g ↔ f = Quiver.homOfEq g hX.symm hY.symm := ...

[Floris van Doorn]

Note that tactics like nth_rw and pick_goal are also 1-indexed.
I think when you're doing metaprogramming, things should be 0-indexed, but for "user-facing" tactics/commands/attributes it should be 1-indexed.

[Yaël Dillies]

I'm personally always surprised to see that nth_rw starts counting at 1. It is unintuitive to me.

[Damiano Testa]

Whatever the numbering is, would it be possible to add a flag somewhere that, if set, logs a message at the specified location, instead of performing whatever computation the command is supposed to do?

[Jovan Gerbscheid]

What sort of flag do you mean?

[Damiano Testa]

Something like to_additive --dry-run ....

[Damiano Testa]

Or maybe the output of to_additive? already does this, or can be extended to make this more explicit?

[Jireh Loreaux]

At this point, I don't really care about this sort of thing, I just don't want it to change! The confusing bit for me with nth_rw wasn't that it starts counting at 1, it's that it used to start counting at 0, and then I had to relearn. So, I don't really care, as long as the behavior (whether 1-indexed or 0-indexed) is documented in the docstring.

[Jireh Loreaux]

Ideally, the referring to the parameters by name would be best.

[Jovan Gerbscheid]

@Damiano Testa If you mean that you want to have a log of what the attribute does, then you can use to_additive?.

[Damiano Testa]

What I was hoping for would be something where by writing

@[to_additive (reorder := 5 6) smul_apply] -- swapping f and a
lemma pow_apply [∀ i, Pow (M i) α] (f : ∀ i, M i) (a : α) (i : ι) : (f ^ a) i = f i ^ a := ...

what is going to be reordered is underlined, and if I change 5 or 6, then the new positions are underlined. So, some "live" signaling of what is going on.

[Jovan Gerbscheid]

Jireh Loreaux said:

Ideally, the referring to the parameters by name would be best.

I agree. I will implement this, and then we can use parameter names, rather than indices, most of the time. And then I don't really mind anymore which indexing style is used.

[Jovan Gerbscheid]

@Damiano Testa I see, though that sounds quite fancy. What you can do, is see the type of smul_apply when you hover over it, so you can see what was swapped.

[Damiano Testa]

Ok, I often would like to see a more extensive use of the Expr.diff functionality that is used in the infoview.

[Jovan Gerbscheid]

Here's my PR: #31748

As a bonus, I've added hover info to the arguments, so you can see the argument's name and type.

afbeelding.png

[Jovan Gerbscheid]

I have tagged the content of Order.Defs.LinearOrder in #31709. One issue I found is that there is a duplication of lemmas such as LinearOrder.min_def and min_def. I think we should treat LinearOrder.min_def as an implementation detail, and only use min_def, so LinearOrder.min_def should not be tagged with to_dual. I raised this issue in #mathlib4 > Should duplicated class projections be private? , and I made the PR #31808 to remove all uses of these internal lemmas.

[Yaël Dillies]

Yes, they were never meant to be used

[Jovan Gerbscheid]

In #31902, I implement a heuristic for guessing the (reorder := ...) argument when using to_dual self or to_dual existing. This means that in the example above, we can simply write

@[to_dual self]
lemma homOfEq_eq_iff {V : Type*} [Quiver V] {X Y X' Y' : V}
    (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') :
    Quiver.homOfEq f hX hY = g ↔ f = Quiver.homOfEq g hX.symm hY.symm := ...

[Violeta Hernández]

Has this tactic been "released" yet? i.e. can I and should I start tagging things?

[Jovan Gerbscheid]

Yes, sort of, we are now in the process of tagging things in mathlib. The problem is that this has to be done in a top-down fashion, so we first need to tag all of the most basic files, in order, in order to be able to use it in more complicated files. I currently have a few open PRs doing just that.

[Violeta Hernández]

@Jovan Gerbscheid I'd like to help by adding to_dual to docs#Order.IsSuccPrelimit and docs#Order.IsSuccLimit. What do I need to edit in order for theorem names to be translated properly?

[Jovan Gerbscheid]

In the current set-up, Limit gets translated into Colimit. I don't know if we should remove this translation from the dictionary. But even if we don't, we can still get this to work. You'll have to add an entry to the fixAbbreviations dictionary, so that it turns SuccColimit into SuccPrelimit.

And for the other direction, you can simply add the translation from Prelimit to Limit directly to the main guessName disctionary.

[Violeta Hernández]

Oh, I should have specified. The dual of IsSuccPrelimit is IsPredPrelimit. And the dual of IsSuccLimit is IsPredLimit.

[Violeta Hernández]

So presumably that's what I want to add to fixAbbreviations?

[Jovan Gerbscheid]

Aha, we can add the translations between succ and pred to the main dictionary, and remove limit from it. Or we can keep the limit to colimit translation and work around it with fixAbbreviations.

[Violeta Hernández]

We definitely want succ ↔ pred in either case, since docs#Order.succ should also get dualized to docs#Order.pred

[Violeta Hernández]

Perhaps we can remove limit ↔ colimit for the moment? And judge whether to add it back if someone makes use of it.

[Jovan Gerbscheid]

When we get a bit further with the tagging, we will get to SemilatticeSup, which is dual to SemilatticeInf, and for example these two lemmas are dual:

theorem sSup_le_sSup {s t : Set α} (h : s ⊆ t) : sSup s ≤ sSup t
theorem sInf_le_sInf {s t : Set α} (h : s ⊆ t) : sInf t ≤ sInf s

The interesting thing to note here is that even though s ⊆ t is an alternative spelling to s ≤ t, we don't actually swap the s and t. There is also a long-term plan to have ⊆ and ≤ be different notations for the same underlying constant (similar to how max a b and a ⊔ b are different notations for the same constant).

So, we should tag Set with @[to_dual_dont_translate], so that we never translate order structures on Set.

[Jovan Gerbscheid]

Today, I had an idea for dealing with definitions like DecidableLT for which we want that the dual is not the same as the dual of the value. The idea is to pre-process (proof) terms in such a way thay they do not rely on unfolding DecidableLT. This can be done by inserting some rewrite or some cast in the right places in the expression.

I made the draft PR #32438, which shows some basic cases working for DecidableLT, WCovBy and Set.Icc.

[Violeta Hernández]

image.png
Am I doing something wrong? This gives me an error "expected PredOrder to have a value"

[Jovan Gerbscheid]

It is not yet supported to generate structures automatically, so you will have to do the following:

import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Order.Cover
import Mathlib.Order.Iterate

variable {α β : Type*}

/-- Order equipped with a sensible successor function. -/
class SuccOrder (α : Type*) [Preorder α] where
  /-- Successor function -/
  succ : α → α
  /-- Proof of basic ordering with respect to `succ` -/
  le_succ : ∀ a, a ≤ succ a
  /-- Proof of interaction between `succ` and maximal element -/
  max_of_succ_le {a} : succ a ≤ a → IsMax a
  /-- Proof that `succ a` is the least element greater than `a` -/
  succ_le_of_lt {a b} : a < b → succ a ≤ b

/-- Order equipped with a sensible predecessor function. -/
@[to_dual (attr := ext) SuccOrder]
class PredOrder (α : Type*) [Preorder α] where
  /-- Predecessor function -/
  pred : α → α
  /-- Proof of basic ordering with respect to `pred` -/
  pred_le : ∀ a, pred a ≤ a
  /-- Proof of interaction between `pred` and minimal element -/
  min_of_le_pred {a} : a ≤ pred a → IsMin a
  /-- Proof that `pred b` is the greatest element less than `b` -/
  le_pred_of_lt {a b} : a < b → a ≤ pred b

[Jovan Gerbscheid]

(I am providing it the name SuccOrder manually because the succ ↔ pred translation is not yet in the guessName dictionary)

[Violeta Hernández]

I'll add it when I make my PR :slight_smile:

[Jovan Gerbscheid]

Eventually I'd like better support for tagging structures and generating the reorders there automatically, but for the time being you will also need to add

attribute [to_dual (reorder := a b)] PredOrder.le_pred_of_lt

To update the reorder argument to be correct for PredOrder.le_pred_of_lt/SuccOrder.succ_le_of_lt

[Violeta Hernández]

Hmm... I'm running across a new error
image.png

[Violeta Hernández]

Is to_dual set up to work with OrderDual?

[Jovan Gerbscheid]

Unfortunately, to_dual cannot yet reorder arguments of arguments. This means that it cannot translate PredOrder.mk to SuccOrder.mk correctly. This should not come up too often, but you've encountered one of these cases now. While we don't have this feature, we will need to declare both instances separately, and link them with to_dual existing.

[Violeta Hernández]

More problems :frown:
image.png

[Violeta Hernández]

I think the issue is the same, with arguments of arguments, but the validation doesn't even let me add the to_dual existing attribute

[Jovan Gerbscheid]

Exactly. The attribute knows that it cannot reorder arguments of arguments, so it disallows adding the to_dual existing attribute here, because this would lead to wrong translations later on anyways.

[Aaron Liu]

somehow this doesn't feel like a very smart attribute

[Violeta Hernández]

It's quite a useful attribute as is, and I trust that it'll get better :slight_smile:

[Violeta Hernández]

How does to_dual interface with alias? If I have something like

alias ⟨foo, bar⟩ := baz

and I want to override both names, do I just have to split it up into?

@[to_dual foo']
alias ⟨foo, _⟩ := baz

@[to_dual bar']
alias ⟨_, bar⟩ := baz

[Jovan Gerbscheid]

Yeah, in general I think

@[attrs]
alias ⟨foo, bar⟩ := baz

is equivalent to

alias ⟨foo, bar⟩ := baz
attribute [attrs] foo bar

So you could also make it

alias ⟨foo, bar⟩ := baz
attribute [to_dual foo'] foo
attribute [to_dual bar'] bar

[Violeta Hernández]

Sorry I'm troubleshooting so much but I just came across another issue :frown:
image.png

[Violeta Hernández]

Is this perhaps fixed by #32438?

[Jovan Gerbscheid]

Yes exactly. WCovBy has the property that the unfolded value of a ⩿ b is not dual to the unfolded value of b ⩿ a. So currently, to_dual doesn't work here, and #32438 should fix this.

[Violeta Hernández]

oh damn I just noticed Monotone and co. haven't been tagged

[Violeta Hernández]

I should probably start there

[Jovan Gerbscheid]

Monotone is problematic for the same reason WCovByis :(

[Violeta Hernández]

oh :frown:

[Violeta Hernández]

I take it that the order dual tactic can't yet handle pi types?

import Mathlib.Order.Iterate

variable [Preorder α] {f : α → α}

@[to_dual iterate_le_id_of_le_id']
theorem id_le_iterate_of_id_le' (h : id ≤ f) (n : ℕ) : id ≤ f^[n] := by
  simpa only [Function.iterate_id] using monotone_id.iterate_le_of_le h n

[Violeta Hernández]

It's not flipping h

[Jovan Gerbscheid]

It does work, we are just missing a tag :)

import Mathlib.Order.Iterate

variable [Preorder α] {f : α → α}

attribute [to_dual existing le_iterate_of_le] Monotone.iterate_le_of_le

@[to_dual iterate_le_id_of_le_id']
theorem id_le_iterate_of_id_le' (h : id ≤ f) (n : ℕ) : id ≤ f^[n] := by
  simpa only [Function.iterate_id] using monotone_id.iterate_le_of_le h n

[Violeta Hernández]

Oh, thanks!

[Violeta Hernández]

I notice OrderTop and OrderBot haven't been dualized

[Violeta Hernández]

Any obstacle, or just no one has done it yet?

[Jovan Gerbscheid]

See #32377

[Violeta Hernández]

Oh, awesome! I'll review it :slight_smile:

[Violeta Hernández]

Just opened #32447 for SuccOrder and PredOrder

[Violeta Hernández]

Also opened #32459 for the Directed file

[Violeta Hernández]

...I'm realizing an issue

[Violeta Hernández]

IsDirected α (· ≤ ·) gets dualized to IsDirected α fun x y ↦ y ≤ x which is def-eq but not syntactically equal to IsDirected α (· ≥ ·) and apparently that messes up typeclass lookup

[Violeta Hernández]

Perhaps the solution is to make abbrevs IsDirectedLE α and IsDirectedGE α, use those instead, and mark them as dual?

[Violeta Hernández]

Why not #32462

[Jovan Gerbscheid]

Are you sure it messes up type class lookup? I don't think it should be a problem because the things are defEq in the reducible transparency.

[Violeta Hernández]

It does seem to mess up some things. Here's an example:

import Mathlib.Order.Bounds.Basic

variable {α : Type*} [Preorder α]

attribute [-instance] OrderDual.isDirected_ge OrderDual.isDirected_le

@[to_dual isDirected_le]
instance isDirected_ge [IsDirected α (· ≤ ·)] : IsDirected αᵒᵈ (· ≥ ·) := by
  assumption

-- The theorem below fails if you delete this
instance isDirected_le' [IsDirected α (· ≥ ·)] : IsDirected αᵒᵈ (· ≤ ·) :=
  isDirected_le

theorem union [IsDirected α (· ≥ ·)] {s t : Set α} :
    BddBelow s → BddBelow t → BddBelow (s ∪ t) :=
  @BddAbove.union αᵒᵈ _ _ _ _

[Violeta Hernández]

I think the abbrevs are probably a good thing anyways? Stops people from trying to write things like IsDirected α fun x y ↦ y ≤ x or IsDirected α (swap (· ≤ ·))

[Jovan Gerbscheid]

Oh wow, thats interesting. The discrimination tree normalization procedure repeatedly does eta-reduction, and unfolding the head constant. So fun x y ↦ x ≥ y get reduced to GE.ge which gets reduced to fun x y ↦ y ≤ x.

But, fun x y ↦ y ≥ x does not get reduced to fun x y ↦ x ≤ y!

[Violeta Hernández]

@Jovan Gerbscheid Ehm, I believe you've somehow introduced a bug in #32377

[Violeta Hernández]

It's making #32477 fail all of a sudden. I'll attempt to minimize it. I think it has to do with typeclass search going through some weird path LinearOrder → LT which doesn't get properly dualized.

[Violeta Hernández]

Adding the lines

@[to_dual bar]
theorem foo {α : Type*} [Lattice α] {a b : α} : a < b → a < b := id

right below docs#Lattice on latest Mathlib makes the to_dual tactic fail with the error

@[to_dual] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
bar:
Application type mismatch: The argument
  inst✝.toSemilatticeInf
has type
  SemilatticeInf α
but is expected to have type
  SemilatticeSup α
in the application
  @SemilatticeSup.toPartialOrder α inst✝.toSemilatticeInf

[Violeta Hernández]

Oh, this seems to be fixed by adding

attribute [to_dual existing] Lattice.toSemilatticeInf

[Jovan Gerbscheid]

Violeta Hernández said:

Jovan Gerbscheid Ehm, I believe you've somehow introduced a bug in #32377

Does that fix this problem?

[Violeta Hernández]

I'm currently recompiling but I think it does

[Jovan Gerbscheid]

I see. Indeed the instance LinearOrder -> LE goes through SemilatticeInf (which seems a bit silly), so now you indeed need to tag Lattice.toSemilatticeInf

[Violeta Hernández]

Just opened #32488 dualizing WithTop and WithBot

[Violeta Hernández]

Might I ask what the status on #32438 is?

[Violeta Hernández]

Do you think there's a way to get to_dual to work on docs#Lex and docs#Colex ?

[Violeta Hernández]

The idea is that on pi types α → β and the like, Colex (α → β) means Lex (αᵒᵈ → β), so it just dualizes one argument

[Aaron Liu]

so there are two ways to dualize?

[Aaron Liu]

since I think (Lex (α → β))ᵒᵈ is the same as Lex (α → βᵒᵈ)

[Violeta Hernández]

Aaron Liu said:

since I think (Lex (α → β))ᵒᵈ is the same as Lex (α → βᵒᵈ)

That's true but I don't believe that's a def-eq

[Violeta Hernández]

Yep, there's two ways to dualize

[Jovan Gerbscheid]

Violeta Hernández said:

Might I ask what the status on #32438 is?

I'm on holiday now, so won't work on it for this week. I wrote in the PR description what is still TODO, but other than those things, it is ready for review.

[Violeta Hernández]

Happy holidays! I'll tag whatever else I can in the meanwhile.

[Kim Morrison]

Sorry, what is the deal with #32488? I think it is essential that we drop the defeq between WithTop/WithBot and Option --- it leaks through all over the place and makes working with WithTop/WithBot very unpleasant. I have been working on this at #27918, and #32488 has introduced fundamental merge conflicts.

Does someone have a plan for proceeding? I would really appreciate if someone (else) could just get this finished.

[Violeta Hernández]

I don't believe #32488 really changes the situation? All the to_dual tactic does is autogenerate the same definitions and lemmas that already existed.

[Violeta Hernández]

I do agree that we want to get rid of the def-eq. I can draft #32498 in the meanwhile, since that will also introduce new merge conflicts.

[Violeta Hernández]

Another option might be to first tag everything here with to_dual and then perform the def-eq dropping. That way we only need to do half the work.

[Violeta Hernández]

I'm willing to take this over

[Kim Morrison]

That's great!

If you could resolve the merge conflicts on #27918 that would be a great start. Thanks.

[Violeta Hernández]

Of course! Can I push to your branch?

[Kim Morrison]

(Context: the FRO interval arithmetic plans are not moving as fast as we'd like, but still hope to eventually get there, and I would really like WithTop/WithBot to be usable by then, as they will be part of the user extension API.)

[Kim Morrison]

Let me check if I need to give your permissions.

[Kim Morrison]

You should have an invite now.

[Violeta Hernández]

Hm, I see an issue. to_dual doesn't seem to like the fact that WithBot is an inductive while WithTop is a (definitionally equal) def.

[Violeta Hernández]

Do we want them to be definitionally equal with each other?

[Violeta Hernández]

Perhaps a solution is to make some auxiliary structure, and declare WithBot and WithTop both def-eq to it

[Violeta Hernández]

Though surely the long term solution is to not have them be def-eq and use to_dual for our order dualizing purposes.

[Violeta Hernández]

Just pushed a merge commit to the branch. I've used this "auxiliary structure" solution for now, but it's a dirty hack and in the future we surely want to just dualize the definition for WithBot itself.

[Kim Morrison]

Violeta Hernández said:

Do we want them to be definitionally equal with each other?

I think in the long run, no, we don't. However the decision in previous discussions around #27918 was that this was too difficult to break on the first pass.

[Violeta Hernández]

This also applies to docs#WithBot.instLE and docs#WithTop.instLE, right? I found that design a bit odd when I added the to_dual tags on #32499.

[Violeta Hernández]

Did you delete some files? The build fails immediately

[Violeta Hernández]

@Kim Morrison The grind cases attribute doesn't seem to work on WithBot anymore. Any fix or way to circumvent this?

[Jovan Gerbscheid]

Violeta Hernández said:

Hm, I see an issue. to_dual doesn't seem to like the fact that WithBot is an inductive while WithTop is a (definitionally equal) def.

I think there should be no fundamental obstacle to this. It's just that nobody has tried/tested it before.

[Jovan Gerbscheid]

But I think the easiest approach is to first tag everything with to_dual, and then changing the definition of WithBot should be easy.

[Kim Morrison]

Violeta Hernández said:

Kim Morrison The grind cases attribute doesn't seem to work on WithBot anymore. Any fix or way to circumvent this?

No, this is why I made it an inductive.

[Kim Morrison]

but I guess this can be a feature request. Any chance you could provide me with a #mwe of what we want from grind cases?

[Jovan Gerbscheid]

I've made #33036 for order homs/embeddings/equivs. This one was a bit tricky because the definition for embeddings/equivs unfolds to something that is not self-dual. This is the problem that #32438 addresses. Unfortuately, #32438 doesn't fix this instance of the problem.

Luckily, we don't tend to rely on unfolding this definition in practice, so we can work around this.

[Violeta Hernández]

Could you help me out with #32459? I don't understand why this randomly turned some instance on ENNReal noncomputable.

[Jovan Gerbscheid]

I don't see anything about ENNReal or noncomputable there? I do see a type class synthesis failure for IsDirectedOrder that may or may not go away if you merge master.

[Violeta Hernández]

Ah! Wrong PR, sorry. One sec

[Violeta Hernández]

I meant #32626

[Violeta Hernández]

Incidentally, I've merged master on #32459. It should hopefully be ready for review. (If it doesn't build, I'll fix it tomorrow, I'm getting really sleepy)

[Jovan Gerbscheid]

The PR for unfold boundaries (#32438) should now be ready for review. It introduces two new commands: to_dual_insert_cast and to_dual_insert_cast_fun (I'm still not quite sure what the commands should really be called), and they are used as follows:

to_dual_insert_cast Monotone := by grind

to_dual_insert_cast_fun DecidableLE := fun inst a b ↦ inst b a, fun inst a b ↦ inst b a

to_dual_insert_cast requires you to prove an equality between the dual and the dual of its value.
to_dual_insert_cast_fun requires you to give a dual to the unfold and refold functions. This for cases where proving equality doesn't make sense, in particular DecidableLE and DecidableLT, because they are types.