Documentation

Mathlib.Tactic.Order.Preprocessing

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.

source
theorem Mathlib.Tactic.Order.not_lt_of_not_le {α : Type u} [Preorder α] {x y : α} (h : ¬x ≤ y) :
¬x < y
source
theorem Mathlib.Tactic.Order.le_of_not_lt_le {α : Type u} [Preorder α] {x y : α} (h1 : ¬x < y) (h2 : x ≤ y) :
y ≤ x
source
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.
Instances For
    source
    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.
    Instances For
      source
      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.
      Instances For