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

• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.eq a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.eq b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.ne a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.ne b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.le a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.le b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.nle a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.nle b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.lt a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.lt b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.nlt a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.nlt b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.isTop a) (Mathlib.Tactic.Order.AtomicFact.isTop b) = (a == b)
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.isBot a) (Mathlib.Tactic.Order.AtomicFact.isBot b) = (a == b)
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.isInf a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.isInf b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq (Mathlib.Tactic.Order.AtomicFact.isSup a a_1 a_2) (Mathlib.Tactic.Order.AtomicFact.isSup b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Tactic.Order.instBEqAtomicFact.beq x✝¹ x✝ = false

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 : CollectFactsM Unit

Implementation for collectFacts in CollectFactsM monad.

Equations

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

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

Extracts facts and atoms from the expression.

Equations

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

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.

Equations

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