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

@[reducible, inline]

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

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

• le : CnstrKind
• lt : CnstrKind

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

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

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

  If h? := some h, then h is proof for that the expression associated with this constraint is equal to e. Recall that the input constraints are normalized. For example, given x y : Int, x ≤ y is internally represented as x ≤ y + 0

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

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

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

• k : Int
• strict : Bool

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

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

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

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

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

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

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

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

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.

• termMap : 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.

• termMapInv : PHashMap ExprPtr (Expr × Expr)

  termMap inverse

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

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

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

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

@[inline]

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