Commit 2025-11-16 16:31 26cb6998

View on Github →

feat(Tactic/Order): translate linear orders to Int (#26580) It was pointed out that order is not complete for linear orders with lattice operations (while it remains complete for linear orders without lattice operations and for general lattices without assuming linearity). The problem for linear orders with lattice operations is NP-hard, but it can be translated from an arbitrary type to Int and then solved using a smart and efficient procedure (such as omega). This PR implements such a translation within the order tactic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Order.lean

deleted inductive Mathlib.Tactic.Order.OrderType

deleted def Mathlib.Tactic.Order.findBestOrderInstance

Modified Mathlib/Tactic/Order/Graph/Basic.lean

modified def Mathlib.Tactic.Order.Graph.constructLeGraph

Modified Mathlib/Tactic/Order/Preprocessing.lean

added inductive Mathlib.Tactic.Order.OrderType

added def Mathlib.Tactic.Order.findBestOrderInstance

added def Mathlib.Tactic.Order.preprocessFacts

added def Mathlib.Tactic.Order.replaceBotTop

Created Mathlib/Tactic/Order/ToInt.lean

added theorem Mathlib.Tactic.Order.ToInt.exists_translation

added def Mathlib.Tactic.Order.ToInt.mkFinFun

added theorem Mathlib.Tactic.Order.ToInt.toInt_eq_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_inf_toInt_eq_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_le_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_lt_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_ne_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_nle_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_nlt_toInt

added theorem Mathlib.Tactic.Order.ToInt.toInt_sup_toInt_eq_toInt

added def Mathlib.Tactic.Order.ToInt.translateToInt

Modified MathlibTest/order.lean