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

@[implicit_reducible]

instance Mathlib.Tactic.Order.instInhabitedAtomicFact : Inhabited AtomicFact

def Mathlib.Tactic.Order.instInhabitedAtomicFact.default : AtomicFact

def Mathlib.Tactic.Order.instBEqAtomicFact.beq : AtomicFact → AtomicFact → Bool

@[implicit_reducible]

instance Mathlib.Tactic.Order.instBEqAtomicFact : BEq AtomicFact

@[implicit_reducible]

instance Mathlib.Tactic.Order.instToStringAtomicFact : ToString AtomicFact

@[reducible, inline]

abbrev Mathlib.Tactic.Order.CollectFactsState : Type

State for CollectFactsM. It contains a map that maps a type to atomic facts collected for this type.

@[reducible, inline]

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

Monad for the fact collection procedure.

def Mathlib.Tactic.Order.addType {u : Lean.Level} (type : Q(Type u)) : CollectFactsM Q(Type u)

Adds type to the state. It checks if the type has already been added up to reducible_and_instances transparency. Returns the type that is added to the state and definitionally equal (but may be not syntactically equal) to type.

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

Adds fact to the state. Assumes that type is already added by addType.

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 ⊓. Assumes that type is already added by addType.

def Mathlib.Tactic.Order.collectFactsImp (only? : Bool) (hyps : Array Lean.Expr) (negGoal : Lean.Expr) : CollectFactsM Unit

Implementation for collectFacts in CollectFactsM monad.

def Mathlib.Tactic.Order.collectFacts (only? : Bool) (hyps : Array Lean.Expr) (negGoal : Lean.Expr) : AtomM (Std.HashMap Lean.Expr (Array AtomicFact))

Collects facts from the local context. negGoal is the negated goal, hyps is the expressions passed to the tactic using square brackets. If only? is true, we collect facts only from hyps and negGoal, otherwise we also use the local context.

For each occurring type α, the returned map contains an array containing all collected AtomicFacts about atoms of type α.