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 that maps a type to atomic facts collected for this type.

Equations

• Mathlib.Tactic.Order.CollectFactsState = Std.HashMap 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 Mathlib.Tactic.AtomM

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.

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 α.

Equations

• Mathlib.Tactic.Order.collectFacts only? hyps negGoal = do let __do_lift ← StateT.run (Mathlib.Tactic.Order.collectFactsImp only? hyps negGoal) ∅ pure __do_lift.snd