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

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

Equations

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

instance Mathlib.Tactic.Order.instInhabitedAtomicFact : Inhabited AtomicFact

Equations

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

instance Mathlib.Tactic.Order.instBEqAtomicFact : BEq AtomicFact

Equations

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

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.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.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 defenitionally equal (but may be not syntactically equal) to type.

Equations

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

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.

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

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