Reordering arguments in a translation

This module defines reorders, which are used by to_dual (reorder := ...) and to_additive (reorder := ...) to deal with definitions and theorems that need to have their arguments reordered.

A reordering is specified using disjoint cycle notation. For example, 1 2 3, 4 5 will move the 1st argument to the 2nd, move the 2nd to the 3rd, and the 3rd to the 1st, and it will swap the 4th and 5th arguments.

Instead of using numbers to refer to argument, you can also refer to them by name. For example a b will swap the arguments named a and b. This is implemented in elabArgStx.

To specify reordering arguments of arguments, the syntax is recursive. For example, 4 (1 2) will reorder the first two arguments of the fourth argument.

Examples

• to_dual needs to swap the arguments of some definitions to translate them, such as a ≤ b ↦ b ≤ a and a ⇨ b ↦ b \ a. In these cases, we reorder the 3rd and 4th arguments, which can be specified using @[to_dual (reorder := 3 4)].

• to_additive needs to swap the arguments when translating a ^ n ↦ n • a.

• Some theorems are dual to themselves only after reordering some arguments. For example, le_total : ∀ a b : α, a ≤ b ∨ b ≤ a is dual to itself after swapping a and b. Thanks to the heuristic in guessReorder, this reordering can often be found automatically, so it suffices to write @[to_dual self].

TODO

We need better support for reordering of universes for to_dual in category theory, for example to dualize CategoryTheory.Comma to itself.

structure Mathlib.Tactic.Translate.Reorder : Type

Reorder represents a permutation of arguments in a translation.

• perm : List { l : List ℕ // 2 ≤ l.length }

  The list of disjoint cycles that represents the permutation.

• argReorders : Array (ℕ × Reorder)

  The recursive reorders for reordering arguments of arguments. For the purpose of checking equality between reorders, this should be sorted.

@[implicit_reducible]

instance Mathlib.Tactic.Translate.instInhabitedReorder : Inhabited Reorder

def Mathlib.Tactic.Translate.instInhabitedReorder.default : Reorder

def Mathlib.Tactic.Translate.Reorder.permuteUniv {α : Type u_1} (r : Reorder) (us : List α) : List α

Permute a list of either universe levels or universe parameters. The current heuristic is to swap the first two universes if the first argument is permuted.

def Mathlib.Tactic.Translate.Reorder.isEmpty (r : Reorder) : Bool

Return true if the reorder doesn't do anything.

def Mathlib.Tactic.Translate.Reorder.permute! {α : Type u_1} [Inhabited α] (r : Reorder) : Array α → Array α

Permute an array of arguments using the given reorder.

@[irreducible]

def Mathlib.Tactic.Translate.Reorder.reverse (r : Reorder) : Reorder

Return the reorder that reverses the action of the given reorder.

def Mathlib.Tactic.Translate.Reorder.range (r : Reorder) : ℕ

Return the minimum size of an array on which the given reorder is valid.

partial def Mathlib.Tactic.Translate.Reorder.beq (r₁ r₂ : Reorder) : Bool

Two Reorders are considered equal if they act on expressions in the same way.

@[implicit_reducible]

instance Mathlib.Tactic.Translate.instBEqReorder : BEq Reorder

@[irreducible]

def Mathlib.Tactic.Translate.Reorder.toString (r : Reorder) : String

Print a Reorder, representing the arguments by their index.

@[implicit_reducible]

instance Mathlib.Tactic.Translate.instToStringReorder : ToString Reorder

@[implicit_reducible]

instance Mathlib.Tactic.Translate.instToMessageDataReorder : Lean.ToMessageData Reorder

Reordering an expression

partial def Mathlib.Tactic.Translate.reorderForall (reorder : Reorder) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Reorder the arguments of a function type using the given Reorder.

partial def Mathlib.Tactic.Translate.reorderLambda (reorder : Reorder) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Reorder the arguments of a function using the given Reorder.

Guessing the reorder given the reordered expression

partial def Mathlib.Tactic.Translate.guessReorder (src tgt : Lean.Expr) : Lean.MetaM Reorder

Try to determine the value of the (reorder := ...) option that would be needed to translate type e₁ to type e₂. If there is no good guess, default to []. The heuristic that we use is to compare the conclusions of e₁ and e₂, and to observe which variables are swapped. We also apply this heuristic recursively in hypotheses.

Syntax for specifying a reorder

def Lean.Parser.Category.translateReorder : Category

The syntax category for the reorder syntax.

def Mathlib.Tactic.Translate.translateReorder.quot : Lean.ParserDescr

def Mathlib.Tactic.Translate.reorderPart : Lean.ParserDescr

def Mathlib.Tactic.Translate.reorder : Lean.ParserDescr

(reorder := ...) reorders the arguments/hypotheses in the generated declaration. This is used in to_dual to swap the arguments in ≤, < and ⟶, and it is used in to_additive to translate from a ^ n to n • a. It uses disjoint cycle notation for the permutation. For reordering arguments of an argument a, it uses the notation a (...) where ... can be any reorder.

For example:

• (reorder := α β, 5 6) swaps the arguments α and β with each other and the fifth and the sixth argument.
• (reorder := 3 4 5) will move the fifth argument before the third argument.
• (reorder := H (x y)) will swap the arguments x and y that appear in the hypothesis H.

If the translated declaration already exists (i.e. when using existing or self), the reorder argument is automatically inferred using the function guessReorder.

def Mathlib.Tactic.Translate.elabArgStx (stx : Lean.TSyntax [`ident, `num]) (argNames : Array Lean.Name) (fvars : Array Lean.Expr) (head : Lean.MessageData) : Lean.MetaM ℕ

Elaborate syntax that refers to an argument of a declaration or hypothesis. This is either a 1-indexed number, or a name from argNames.

• fvars is only used to add hover information to stx
• head is only used for the error message.

partial def Mathlib.Tactic.Translate.elabReorder (stx : Lean.TSyntax `translateReorder) (argNames : Array Lean.Name) (args : Array Lean.Expr) (head : Lean.MessageData) : Lean.MetaM Reorder

Elaborate the argument of a (reorder := ...) option.