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

Equations

• Mathlib.Tactic.Order.instInhabitedAtomicFact = { default := Mathlib.Tactic.Order.instInhabitedAtomicFact.default }

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

Equations

• Mathlib.Tactic.Order.instInhabitedAtomicFact.default = Mathlib.Tactic.Order.AtomicFact.eq default default default

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

Equations

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

instance Mathlib.Tactic.Order.instBEqAtomicFact : BEq AtomicFact

Equations

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

instance Mathlib.Tactic.Order.instToStringAtomicFact : ToString AtomicFact

Equations

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

@[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.

Equations

• Mathlib.Tactic.Order.CollectFactsState = Std.HashMap Lean.Expr (Lean.Meta.DiscrTree (ℕ × Lean.Expr) × Array Mathlib.Tactic.Order.AtomicFact)

@[reducible, inline]

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

Monad for the fact collection procedure.

Equations

• Mathlib.Tactic.Order.CollectFactsM = StateT Mathlib.Tactic.Order.CollectFactsState Lean.MetaM

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

Adds fact to the state.

Equations

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

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 (only? : Bool) (hyps : Array Lean.Expr) (negGoal : Lean.Expr) : CollectFactsM Unit

Implementation for collectFacts in CollectFactsM monad.

Equations

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

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

Extracts facts and atoms from the expression.

def Mathlib.Tactic.Order.collectFacts (only? : Bool) (hyps : Array Lean.Expr) (negGoal : Lean.Expr) : Lean.MetaM (Std.HashMap Lean.Expr (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 a pair (idxToAtom, facts), where the map idxToAtom converts indices to found atomic expressions of type α, and facts contains all collected AtomicFacts about them.

Equations

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