Reordering arguments in a translation

This module defines reorders, which can be specified with to_dual (reorder := ...) or to_additive (reorder := ...), to deal with definitions and theorems that need to have their arguments and/or universe parameters 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.

If the declaration is translated to itself or to an existing declaration, the heuristic in guessReorder tries to predict the argument reorder. This is done with a syntactic comparison of which variable is moved where.

The universe reordering is always inferred automatically, using guessUnivReorder.

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, it suffices to write @[to_dual self].

Implementation details

Permutation are stored as their disjoint cycle representation (Permutation). This allows efficiently permuting an array/list of arguments/universes (Permutation.permute!/Permutation.permuteList!).

@[reducible, inline]

abbrev Mathlib.Tactic.Translate.Permutation : Type

A permutation, represented using cycle notation.

Equations

• Mathlib.Tactic.Translate.Permutation = List { l : List Nat // 2 ≤ l.length }

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

Permute an array of arguments using the given reorder.

Equations

• c.permute! init = List.foldl (fun (x1 : Array α) (x2 : { l : List Nat // 2 ≤ l.length }) => Mathlib.Tactic.Translate.Permutation.permute!.cyclicPermute!✝ x1 x2.val) init c

def Mathlib.Tactic.Translate.Permutation.permuteList! {α : Type u_1} [Inhabited α] (p : Permutation) (us : List α) : List α

Permute a list of either universe levels or universe parameters.

Equations

• p.permuteList! us = if List.isEmpty p = true then us else (p.permute! us.toArray).toList

def Mathlib.Tactic.Translate.Permutation.reverse (c : Permutation) : Permutation

Return the inverse permutation.

Equations

• c.reverse = List.map (fun (x : { l : List Nat // 2 ≤ l.length }) => ⟨x.val.reverse, ⋯⟩) c

def Mathlib.Tactic.Translate.Permutation.range (p : Permutation) : Nat

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

Equations

• p.range = Std.Iter.fold max 0 (Std.Iter.map (fun (x : Nat) => x + 1) (Std.Iter.flatMap (fun (x : { l : List Nat // 2 ≤ l.length }) => x.val.iter) (List.iter p)))

def Mathlib.Tactic.Translate.Permutation.beq (p₁ p₂ : Permutation) : Bool

Two permutations are considered equal if they permute in the same way.

Equations

• p₁.beq p₂ = (p₁.range == p₂.range && have rangeArr := (0...p₁.range).toArray; p₁.permute! rangeArr == p₂.permute! rangeArr)

structure Mathlib.Tactic.Translate.ArgReorder : Type

ArgReorder represents a permutation of arguments in a translation.

• perm : Permutation

  The list of disjoint cycles that represents the permutation.

• argReorders : Array (Nat × ArgReorder)

  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.instInhabitedArgReorder : Inhabited ArgReorder

Equations

• Mathlib.Tactic.Translate.instInhabitedArgReorder = { default := Mathlib.Tactic.Translate.instInhabitedArgReorder.default }

def Mathlib.Tactic.Translate.instInhabitedArgReorder.default : ArgReorder

Equations

• Mathlib.Tactic.Translate.instInhabitedArgReorder.default = { perm := default, argReorders := default }

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

Return true if the reorder doesn't do anything.

Equations

• r.isEmpty = match r with | { } => true | x => false

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

Permute an array of arguments using the given reorder.

Equations

• r.permute! = r.perm.permute!

@[irreducible]

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

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.ArgReorder.range (r : ArgReorder) : Nat

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

Equations

• One or more equations did not get rendered due to their size.

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

Two reorders are considered equal if all permutations are the same.

@[implicit_reducible]

instance Mathlib.Tactic.Translate.ArgReorder.instBEq : BEq ArgReorder

Equations

• Mathlib.Tactic.Translate.ArgReorder.instBEq = { beq := Mathlib.Tactic.Translate.ArgReorder.beq }

@[irreducible]

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

Print an ArgReorder, representing the arguments by their index.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Mathlib.Tactic.Translate.ArgReorder.instToString : ToString ArgReorder

Equations

• Mathlib.Tactic.Translate.ArgReorder.instToString = { toString := fun (x : Mathlib.Tactic.Translate.ArgReorder) => x.toString }

@[implicit_reducible]

instance Mathlib.Tactic.Translate.ArgReorder.instToMessageData : Lean.ToMessageData ArgReorder

Equations

• Mathlib.Tactic.Translate.ArgReorder.instToMessageData = { toMessageData := fun (x : Mathlib.Tactic.Translate.ArgReorder) => (Lean.MessageData.ofFormat ∘ Std.format) x.toString }

structure Mathlib.Tactic.Translate.Reorder : Type

Reorder represents a permutation of arguments and universe levels for translating a given constant.

• univReorder : Permutation

  The reordering of universe levels.

• reorder : ArgReorder

  The reordering of arguments.

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

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

Equations

• r.reverse = { univReorder := r.univReorder.reverse, reorder := r.reorder.reverse }

Reordering an expression

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

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

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

Reorder the arguments of a function using the given ArgReorder.

Guessing the reorder given the reordered expression

def Mathlib.Tactic.Translate.guessUnivReorder (reorder : ArgReorder) (decl : Lean.ConstantInfo) : Permutation

Determine the universe level reorder for decl, given the argument reorder. For each reordering in reorder, we find any corresponding universe reorderings, which are then combined to get the result.

Equations

• One or more equations did not get rendered due to their size.

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

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.

Equations

• Lean.Parser.Category.translateReorder = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Mathlib.Tactic.Translate.reorder = Lean.ParserDescr.node `Mathlib.Tactic.Translate.reorder 1022 (Mathlib.Tactic.Translate.reorderPart.sepBy "," (Lean.ParserDescr.symbol ", "))

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

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