Facts preprocessing for the order tactic

In this file we implement the preprocessing procedure for the order tactic. See Mathlib/Tactic/Order.lean for details of preprocessing.

theorem Mathlib.Tactic.Order.not_lt_of_not_le {α : Type u} [Preorder α] {x y : α} (h : ¬x ≤ y) : ¬x < y

theorem Mathlib.Tactic.Order.le_of_not_lt_le {α : Type u} [Preorder α] {x y : α} (h1 : ¬x < y) (h2 : x ≤ y) : y ≤ x

inductive Mathlib.Tactic.Order.OrderType : Type

Supported order types: linear, partial, and preorder.

• lin : OrderType
• part : OrderType
• pre : OrderType

def Mathlib.Tactic.Order.instBEqOrderType.beq : OrderType → OrderType → Bool

Equations

• Mathlib.Tactic.Order.instBEqOrderType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Mathlib.Tactic.Order.instBEqOrderType : BEq OrderType

Equations

• Mathlib.Tactic.Order.instBEqOrderType = { beq := Mathlib.Tactic.Order.instBEqOrderType.beq }

instance Mathlib.Tactic.Order.instToStringOrderType : ToString OrderType

Equations

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

def Mathlib.Tactic.Order.findBestOrderInstance (type : Lean.Expr) : Lean.MetaM (Option OrderType)

Find the "best" instance of an order on a given type. A linear order is preferred over a partial order, and a partial order is preferred over a preorder.

Equations

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

def Mathlib.Tactic.Order.replaceBotTop (facts : Array AtomicFact) (idxToAtom : Std.HashMap ℕ Lean.Expr) : Lean.MetaM (Array AtomicFact)

Replaces facts of the form x = ⊤ with y ≤ x for all y, and similarly for x = ⊥.

Equations

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

def Mathlib.Tactic.Order.preprocessFactsPreorder (facts : Array AtomicFact) : Lean.MetaM (Array AtomicFact)

Preprocesses facts for preorders. Replaces x < y with two equivalent facts: x ≤ y and ¬ (y ≤ x). Replaces x = y with x ≤ y, y ≤ x and removes x ≠ y.

Equations

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

def Mathlib.Tactic.Order.preprocessFactsPartial (facts : Array AtomicFact) (idxToAtom : Std.HashMap ℕ Lean.Expr) : Lean.MetaM (Array AtomicFact)

Preprocesses facts for partial orders. Replaces x < y, ¬ (x ≤ y), and x = y with equivalent facts involving only ≤, ≠, and ≮. For each fact x = y ⊔ z adds y ≤ x and z ≤ x facts, and similarly for ⊓.

Equations

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

def Mathlib.Tactic.Order.preprocessFactsLinear (facts : Array AtomicFact) (idxToAtom : Std.HashMap ℕ Lean.Expr) : Lean.MetaM (Array AtomicFact)

Preprocesses facts for linear orders. Replaces x < y, ¬ (x ≤ y), ¬ (x < y), and x = y with equivalent facts involving only ≤ and ≠. For each fact x = y ⊔ z adds y ≤ x and z ≤ x facts, and similarly for ⊓.

Equations

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

def Mathlib.Tactic.Order.preprocessFacts (facts : Array AtomicFact) (idxToAtom : Std.HashMap ℕ Lean.Expr) (orderType : OrderType) : Lean.MetaM (Array AtomicFact)

Preprocesses facts for order of orderType using either preprocessFactsPreorder or preprocessFactsPartial or preprocessFactsLinear.

Equations

• Mathlib.Tactic.Order.preprocessFacts facts idxToAtom Mathlib.Tactic.Order.OrderType.pre = Mathlib.Tactic.Order.preprocessFactsPreorder facts
• Mathlib.Tactic.Order.preprocessFacts facts idxToAtom Mathlib.Tactic.Order.OrderType.part = Mathlib.Tactic.Order.preprocessFactsPartial facts idxToAtom
• Mathlib.Tactic.Order.preprocessFacts facts idxToAtom Mathlib.Tactic.Order.OrderType.lin = Mathlib.Tactic.Order.preprocessFactsLinear facts idxToAtom