Facts collection for the order Tactic

This file implements the collection of facts for the order tactic.

inductive Mathlib.Tactic.Order.AtomicFact : Type

A structure for storing facts about variables.

• eq (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
• ne (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
• le (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
• nle (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
• lt (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
• nlt (lhs rhs : ℕ) (proof : Lean.Expr) : AtomicFact
• isTop (idx : ℕ) : AtomicFact
• isBot (idx : ℕ) : AtomicFact
• isInf (lhs rhs res : ℕ) : AtomicFact
• isSup (lhs rhs res : ℕ) : AtomicFact

instance Mathlib.Tactic.Order.instInhabitedAtomicFact : Inhabited AtomicFact

instance Mathlib.Tactic.Order.instBEqAtomicFact : BEq AtomicFact

instance Mathlib.Tactic.Order.instToStringAtomicFact : ToString AtomicFact

@[reducible, inline]

abbrev Mathlib.Tactic.Order.CollectFactsState : Type

State for CollectFactsM. It contains a map where the key t maps to a pair (atomToIdx, facts). atomToIdx is a DiscrTree containing atomic expressions with their indices, and facts stores AtomicFacts about them.

@[reducible, inline]

abbrev Mathlib.Tactic.Order.CollectFactsM (α : Type) : Type

Monad for the fact collection procedure.

def Mathlib.Tactic.Order.addFact (type : Lean.Expr) (fact : AtomicFact) : CollectFactsM Unit

Adds fact to the state.

partial def Mathlib.Tactic.Order.addAtom {u : Lean.Level} (type : Q(Type u)) (x : Q(«$type»)) : CollectFactsM ℕ

Updates the state with the atom x. If x is ⊤ or ⊥, adds the corresponding fact. If x is y ⊔ z, adds a fact about it, then recursively calls addAtom on y and z. Similarly for ⊓.

def Mathlib.Tactic.Order.collectFactsImp : CollectFactsM Unit

Implementation for collectFacts in CollectFactsM monad.

def Mathlib.Tactic.Order.collectFactsImp.processExpr (expr : Lean.Expr) : CollectFactsM Unit

Extracts facts and atoms from the expression.

def Mathlib.Tactic.Order.collectFacts : Lean.MetaM (Std.HashMap Lean.Expr (Std.HashMap ℕ Lean.Expr × Array AtomicFact))

Collects facts from the local context. For each occurring type α, the returned map contains a pair (idxToAtom, facts), where the map idxToAtom converts indices to found atomic expressions of type α, and facts contains all collected AtomicFacts about them.