Solver for preorders, partial orders, linear orders, and support for offsets.

@[reducible, inline]

abbrev Lean.Meta.Grind.Order.NodeId : Type

Equations

• Lean.Meta.Grind.Order.NodeId = Nat

inductive Lean.Meta.Grind.Order.CnstrKind : Type

• le : CnstrKind
• lt : CnstrKind

instance Lean.Meta.Grind.Order.instInhabitedCnstrKind : Inhabited CnstrKind

Equations

• Lean.Meta.Grind.Order.instInhabitedCnstrKind = { default := Lean.Meta.Grind.Order.instInhabitedCnstrKind.default }

def Lean.Meta.Grind.Order.instInhabitedCnstrKind.default : CnstrKind

Equations

• Lean.Meta.Grind.Order.instInhabitedCnstrKind.default = Lean.Meta.Grind.Order.CnstrKind.le

structure Lean.Meta.Grind.Order.Cnstr (α : Type) : Type

A constraint of the form u ≤ v + k (u < v + k if strict := true) Remark: If the order does not support offsets, then k is zero. h? := some h if the Lean expression is not definitionally equal to the constraint, but provably equal with proof h.

• kind : CnstrKind
• u : α
• v : α
• k : Int
• e : Expr

  Denotation of this constraint as an expression.

• h? : Option Expr

instance Lean.Meta.Grind.Order.instInhabitedCnstr {a✝ : Type} [Inhabited a✝] : Inhabited (Cnstr a✝)

Equations

• Lean.Meta.Grind.Order.instInhabitedCnstr = { default := Lean.Meta.Grind.Order.instInhabitedCnstr.default }

def Lean.Meta.Grind.Order.instInhabitedCnstr.default {a✝ : Type} [Inhabited a✝] : Cnstr a✝

Equations

• Lean.Meta.Grind.Order.instInhabitedCnstr.default = { kind := default, u := default, v := default, k := default, e := default, h? := default }

structure Lean.Meta.Grind.Order.Weight : Type

• k : Int
• strict : Bool

def Lean.Meta.Grind.Order.instInhabitedWeight.default : Weight

Equations

• Lean.Meta.Grind.Order.instInhabitedWeight.default = { k := default, strict := default }

instance Lean.Meta.Grind.Order.instInhabitedWeight : Inhabited Weight

Equations

• Lean.Meta.Grind.Order.instInhabitedWeight = { default := Lean.Meta.Grind.Order.instInhabitedWeight.default }

structure Lean.Meta.Grind.Order.ProofInfo : Type

Auxiliary structure used for proof extraction.

• w : NodeId
• k : Weight
• proof : Expr

instance Lean.Meta.Grind.Order.instInhabitedProofInfo : Inhabited ProofInfo

Equations

• Lean.Meta.Grind.Order.instInhabitedProofInfo = { default := Lean.Meta.Grind.Order.instInhabitedProofInfo.default }

def Lean.Meta.Grind.Order.instInhabitedProofInfo.default : ProofInfo

Equations

• Lean.Meta.Grind.Order.instInhabitedProofInfo.default = { w := default, k := default, proof := default }

inductive Lean.Meta.Grind.Order.ToPropagate : Type

Auxiliary inductive type for representing constraints and equalities that should be propagated to core. Recall that we cannot compute proofs until the short-distance data-structures have been fully updated when a new edge is inserted. Thus, we store the information to be propagated into a list. See field propagate in State.

• eqTrue (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : ToPropagate
• eqFalse (c : Cnstr NodeId) (e : Expr) (u v : NodeId) (k k' : Weight) : ToPropagate
• eq (u v : NodeId) : ToPropagate

def Lean.Meta.Grind.Order.instInhabitedToPropagate.default : ToPropagate

Equations

• Lean.Meta.Grind.Order.instInhabitedToPropagate.default = Lean.Meta.Grind.Order.ToPropagate.eqTrue default default default default default default

instance Lean.Meta.Grind.Order.instInhabitedToPropagate : Inhabited ToPropagate

Equations

• Lean.Meta.Grind.Order.instInhabitedToPropagate = { default := Lean.Meta.Grind.Order.instInhabitedToPropagate.default }

structure Lean.Meta.Grind.Order.Struct : Type

State for each order structure processed by this module. Each type must at least implement the instance Std.IsPreorder.

• id : Nat
• type : Expr
• u : Level

  Cached getDecLevel type

• isPreorderInst : Expr
• leInst : Expr

  LE instance

• ltInst? : Option Expr

  LT instance if available

• isPartialInst? : Option Expr

  IsPartialOrder instance if available

• isLinearPreInst? : Option Expr

  IsLinearPreorder instance if available

• lawfulOrderLTInst? : Option Expr

  LawfulOrderLT instance if available

• ringId? : Option Nat

  id of the CommRing (or Ring) structure in the grind ring module if available.

• isCommRing : Bool

  true if ringId? is the Id of a commutative ring

• ringInst? : Option Expr

  Ring instance if available

• orderedRingInst? : Option Expr

  OrderedRing instance if available

• leFn : Expr
• ltFn? : Option Expr
• nodes : PArray Expr

  Mapping from NodeId to the Expr represented by the node.

• nodeMap : PHashMap ExprPtr NodeId

  Mapping from Expr to a node representing it.

• cnstrs : PHashMap ExprPtr (Cnstr NodeId)

  Mapping from Expr representing inequalities to constraints.

• cnstrsOf : PHashMap (NodeId × NodeId) (List (Cnstr NodeId × Expr))

  Mapping from pairs (u, v) to a list of constraints on u and v. We use this mapping to implement exhaustive constraint propagation.

• sources : PArray (AssocList NodeId Weight)

  For each node with id u, sources[u] contains pairs (v, k) s.t. there is a path from v to u with weight k.

• targets : PArray (AssocList NodeId Weight)

  For each node with id u, targets[u] contains pairs (v, k) s.t. there is a path from u to v with weight k.

• proofs : PArray (AssocList NodeId ProofInfo)

  Proof reconstruction information. For each node with id u, proofs[u] contains pairs (v, { w, proof }) s.t. there is a path from u to v, and w is the penultimate node in the path, and proof is the justification for the last edge.

• propagate : List ToPropagate

  Truth values and equalities to propagate to core.

def Lean.Meta.Grind.Order.instInhabitedStruct.default : Struct

Equations

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

instance Lean.Meta.Grind.Order.instInhabitedStruct : Inhabited Struct

Equations

• Lean.Meta.Grind.Order.instInhabitedStruct = { default := Lean.Meta.Grind.Order.instInhabitedStruct.default }

structure Lean.Meta.Grind.Order.State : Type

State for all order types detected by grind.

• structs : Array Struct

  Order structures detected.

• typeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "structure id". We cache failures using none. typeIdOf[type] is some id, then id < structs.size.

• exprToStructId : PHashMap ExprPtr Nat

  Mapping from expressions/terms to their structure ids.

• cnstrsMap : PHashMap ExprPtr (Expr × Expr)

  Mapping from terms/constraints that have been mapped into Rings before being internalized. Example: given x y : Nat, x ≤ y + 1 is mapped to Int.ofNat x ≤ Int.ofNat y + 1, and proof of equivalence.

• cnstrsMapInv : PHashMap ExprPtr (Expr × Expr)

  cnstrsMap inverse

instance Lean.Meta.Grind.Order.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Order.instInhabitedState = { default := Lean.Meta.Grind.Order.instInhabitedState.default }

def Lean.Meta.Grind.Order.instInhabitedState.default : State

Equations

• Lean.Meta.Grind.Order.instInhabitedState.default = { structs := default, typeIdOf := default, exprToStructId := default, cnstrsMap := default, cnstrsMapInv := default }

opaque Lean.Meta.Grind.Order.orderExt : SolverExtension State

def Lean.Meta.Grind.Order.get' : GoalM State

Equations

• Lean.Meta.Grind.Order.get' = Lean.Meta.Grind.Order.orderExt.getState

@[inline]

def Lean.Meta.Grind.Order.modify' (f : State → State) : GoalM Unit

Equations

• Lean.Meta.Grind.Order.modify' f = Lean.Meta.Grind.Order.orderExt.modifyState f