Commit 2025-02-26 07:29 ac48cd5b

View on Github →

feat(Tactic): order tactic for Preorder, PartialOrder, LinearOrder (#21877) Implement an efficient decision procedure for Preorder, PartialOrder and LinearOrder in a new order tactic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Order.lean

added inductive Mathlib.Tactic.Order.OrderType

added def Mathlib.Tactic.Order.findBestOrderInstance

added def Mathlib.Tactic.Order.findContradictionWithNe

added def Mathlib.Tactic.Order.findContradictionWithNle

added def Mathlib.Tactic.Order.updateGraphWithNlt

Created Mathlib/Tactic/Order/CollectFacts.lean

added inductive Mathlib.Tactic.Order.AtomicFact

added def Mathlib.Tactic.Order.addFact

added def Mathlib.Tactic.Order.collectFacts

added def Mathlib.Tactic.Order.collectFactsImp

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

added structure Mathlib.Tactic.Order.Edge

added structure Mathlib.Tactic.Order.Graph.DFSState

added def Mathlib.Tactic.Order.Graph.addEdge

added def Mathlib.Tactic.Order.Graph.buildTransitiveLeProof

added def Mathlib.Tactic.Order.Graph.constructLeGraph

Created Mathlib/Tactic/Order/Graph/Tarjan.lean

added structure Mathlib.Tactic.Order.Graph.TarjanState

added def Mathlib.Tactic.Order.Graph.findSCCs

added def Mathlib.Tactic.Order.Graph.findSCCsImp

Created Mathlib/Tactic/Order/Preprocessing.lean

added theorem Mathlib.Tactic.Order.le_of_not_lt_le

added theorem Mathlib.Tactic.Order.not_lt_of_not_le

added def Mathlib.Tactic.Order.preprocessFactsLinear

added def Mathlib.Tactic.Order.preprocessFactsPartial

added def Mathlib.Tactic.Order.preprocessFactsPreorder

Created MathlibTest/order.lean

Modified scripts/noshake.json