Lexicographical LinearOrder

Stream: lean4

[Marcus Rossel]

What is the easiest way to derive LinearOrder for some structure whose fields all have LinearOrder instances?
E.g. I have:

import Mathlib

def Time := Nat
deriving LinearOrder

structure Tag where
  time : Time
  microstep : Nat

... and would like to derive:

instance : LinearOrder Tag := ...

... with < being the lexicographical ordering.
I tried deriving LinearOrder on Tag, but that gives:

default handlers have not been implemented yet, class: 'LinearOrder' types: [Tag].

Also, I've seen docs4#Sum.Lex which seems like it might be relevant. But I don't understand how to use it.

[Yaël Dillies]

sum.lex won't make a linear order. You probably want psigma.lex instead since all structures can be written as nested sigma types.

[Eric Wieser]

cc @Kyle Miller regarding !4#3215 which constructs an equivalence to Sum/Sigma types

[Eric Wieser]

I hadn't expected my suggestion there to be needed by someone so quickly!

[Kyle Miller]

In mathlib4#3198 I've refactored it to reconfigure how the proxy type is generated.

I think you would just need to make your own mkCtorProxyType by starting with defaultMkCtorProxyType, and make your own term elaborator with this configuration to construct an equivalence.

[Kyle Miller]

What's the function to pull a LinearOrder across an Equiv?

[Eric Wieser]

docs4#LinearOrder.lift'

[Kyle Miller]

import Mathlib.Tactic.ProxyType
import Mathlib.Order.Basic
import Mathlib.Data.Sigma.Order

namespace Mathlib.ProxyType
open Lean Meta Elab Term

def lexMkCtorProxyType (xs : List (Expr × Name)) : TermElabM (Expr × Term) :=
  match xs with
  | [] => return (mkConst ``Unit, ← `(term| ()))
  | [(x, a)] => do
    let xty ← inferType x
    if ← Meta.isProp xty then
      return (← mkAppM ``PLift #[xty], ← `(term| ⟨$(mkIdent a)⟩))
    else
      return (xty, mkIdent a)
  | (x, a) :: xs => do
    let (xsty, patt) ← defaultMkCtorProxyType xs
    let xty ← inferType x
    if ← Meta.isProp xty then
      withLocalDeclD `x' (← mkAppM ``PLift #[xty]) fun x' => do
        let xsty' := xsty.replaceFVar x (← mkAppM ``PLift.down #[x'])
        let ty ← mkAppM ``Lex #[← mkAppM ``Sigma #[← mkLambdaFVars #[x'] xsty']]
        return (ty, ← `(term| ⟨⟨$(mkIdent a)⟩, $patt⟩))
    else
      let ty ← mkAppM ``Lex #[← mkAppM ``Sigma #[← mkLambdaFVars #[x] xsty]]
      return (ty, ← `(term| ⟨$(mkIdent a), $patt⟩))

def ProxyEquivConfig.lexDefault (indVal : InductiveVal) : ProxyEquivConfig where
  proxyName := indVal.name.mkStr "proxyLexType"
  proxyEquivName := indVal.name.mkStr "proxyLexTypeEquiv"
  mkCtorProxyType := lexMkCtorProxyType
  mkProxyType := defaultMkProxyType

elab "proxy_lex_equiv% " t:term : term <= expectedType => do
  let (type, indVal) ← elabProxyEquiv t expectedType
  let config : ProxyEquivConfig := ProxyEquivConfig.lexDefault indVal
  ensureProxyEquiv config indVal
  mkAppOptM config.proxyEquivName (type.getAppArgs.map .some)

end Mathlib.ProxyType

def Time := Nat
deriving LinearOrder

structure Tag where
  time : Time
  microstep : Nat

instance : LinearOrder Tag :=
  LinearOrder.lift' _ (Equiv.injective (Equiv.symm (proxy_lex_equiv% Tag)))

[Kyle Miller]

I guess this also needs an implementation of mkProxyType to turn Sum a b into Lex (Sum a b) for multi-constructor inductive types. What's the rationale for Sum not having a LinearOrder by default?

[Kyle Miller]

With some more tweaking, this is what it looks like:

import Mathlib.Tactic.ProxyType
import Mathlib.Order.Basic
import Mathlib.Data.Sigma.Order
import Mathlib.Data.Sum.Order

namespace Mathlib.ProxyType
open Lean Meta Elab Term

def ProxyEquivConfig.lexDefault (indVal : InductiveVal) : ProxyEquivConfig where
  proxyName := indVal.name.mkStr "proxyLexType"
  proxyEquivName := indVal.name.mkStr "proxyLexTypeEquiv"
  mkCtorProxyType := defaultMkCtorProxyType (decorateSigma := fun e => mkAppM ``Lex #[e])
  mkProxyType := defaultMkProxyType (decorateSum := fun e => mkAppM ``Lex #[e])

syntax (name := proxy_lex_equiv) "proxy_lex_equiv% " term : term

@[term_elab proxy_lex_equiv]
def elab_proxy_lex_equiv : Elab.Term.TermElab := fun stx expectedType? =>
  match stx with
  | `(proxy_lex_equiv% $t) => do
    let (type, indVal) ← elabProxyEquiv t expectedType?
    let config : ProxyEquivConfig := ProxyEquivConfig.lexDefault indVal
    ensureProxyEquiv config indVal
    mkAppOptM config.proxyEquivName (type.getAppArgs.map .some)
  | _ => throwUnsupportedSyntax

end Mathlib.ProxyType

def Time := Nat
deriving LinearOrder

structure Tag where
  time : Time
  microstep : Nat

instance foo : LinearOrder Tag :=
  LinearOrder.lift' _ (proxy_lex_equiv% Tag).symm.injective

[Kyle Miller]

It uses Lex (Sum _ _) for multi-constructor types:

inductive X
  | a : Nat → Nat → X
  | b : Nat → X

instance : LinearOrder X :=
  LinearOrder.lift' _ (proxy_lex_equiv% X).symm.injective

The type it generates here is Lex (Lex ((_ : ℕ) × ℕ) ⊕ ℕ)

[Kyle Miller]

I pushed mathlib4#3251 for this simple LinearOrder derive handler.

Example usage:

import Mathlib.Tactic.DeriveLinearOrder

def Time := Nat
deriving LinearOrder

structure Tag where
  time : Time
  microstep : Nat
  deriving LinearOrder

[Kyle Miller]

It supports types more complicated than structures, but not recursive ones or ones with indices.

inductive X (α : Type)
  | a : Nat → α → X α
  | b : Nat → X α
  deriving LinearOrder

#check instLinearOrderX
-- instLinearOrderX {α✝ : Type} [inst✝ : LinearOrder α✝] : LinearOrder (X α✝)