@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.LinExpr : Type

Equations

• Lean.Meta.Grind.Arith.Linear.LinExpr = Lean.Grind.Linarith.Expr

instance Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean : Hashable Poly

Equations

• Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean = { hash := Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash }

def Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash : Poly → UInt64

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash Lean.Grind.Linarith.Poly.nil = 0

instance Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean : Hashable Grind.Linarith.Expr

Equations

• Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean = { hash := Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash }

def Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash : Grind.Linarith.Expr → UInt64

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash Lean.Grind.Linarith.Expr.zero = 0
• Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash (Lean.Grind.Linarith.Expr.var a) = mixHash 1 (hash a)
• Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a.neg = mixHash 4 (Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a)
• Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash (Lean.Grind.Linarith.Expr.natMul a a_1) = mixHash (mixHash 5 (hash a)) (Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a_1)
• Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash (Lean.Grind.Linarith.Expr.intMul a a_1) = mixHash (mixHash 6 (hash a)) (Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a_1)

structure Lean.Meta.Grind.Arith.Linear.EqCnstr : Type

An equality constraint and its justification/proof.

• p : Poly
• h : EqCnstrProof

inductive Lean.Meta.Grind.Arith.Linear.EqCnstrProof : Type

• core (a b : Expr) (lhs rhs : LinExpr) : EqCnstrProof
• coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : EqCnstrProof
• coreOfNat (a b : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : EqCnstrProof
• neg (c : EqCnstr) : EqCnstrProof
• coeff (k : Nat) (c : EqCnstr) : EqCnstrProof
• subst (x : Var) (c₁ c₂ : EqCnstr) : EqCnstrProof

structure Lean.Meta.Grind.Arith.Linear.IneqCnstr : Type

An inequality constraint and its justification/proof.

• p : Poly
• strict : Bool
• h : IneqCnstrProof

inductive Lean.Meta.Grind.Arith.Linear.IneqCnstrProof : Type

• core (e : Expr) (lhs rhs : LinExpr) : IneqCnstrProof
• notCore (e : Expr) (lhs rhs : LinExpr) : IneqCnstrProof
• coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : IneqCnstrProof
• notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : IneqCnstrProof
• coreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : IneqCnstrProof
• notCoreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : IneqCnstrProof
• combine (c₁ c₂ : IneqCnstr) : IneqCnstrProof
• norm (c₁ : IneqCnstr) (k : Nat) : IneqCnstrProof
• dec (h : FVarId) : IneqCnstrProof
• ofDiseqSplit (c₁ : DiseqCnstr) (decVar : FVarId) (h : UnsatProof) (decVars : Array FVarId) : IneqCnstrProof
• oneGtZero : IneqCnstrProof
• ofEq (a b : Expr) (la lb : LinExpr) : IneqCnstrProof

  a ≤ b from an equality a = b coming from the core.

• ofEqOfNat (a b : Expr) (natStructId : Nat) (la lb : LinExpr) : IneqCnstrProof

  a ≤ b from an equality a = b coming from the core.

• ofCommRingEq (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : IneqCnstrProof

  a ≤ b from an equality a = b coming from the core.

• subst (x : Var) (c₁ : EqCnstr) (c₂ : IneqCnstr) : IneqCnstrProof

structure Lean.Meta.Grind.Arith.Linear.DiseqCnstr : Type

• p : Poly
• h : DiseqCnstrProof

inductive Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof : Type

• core (a b : Expr) (lhs rhs : LinExpr) : DiseqCnstrProof
• coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : DiseqCnstrProof
• coreOfNat (a b : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : DiseqCnstrProof
• neg (c : DiseqCnstr) : DiseqCnstrProof
• subst (k₁ k₂ : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• subst1 (k : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• oneNeZero : DiseqCnstrProof

inductive Lean.Meta.Grind.Arith.Linear.UnsatProof : Type

• diseq (c : DiseqCnstr) : UnsatProof
• lt (c : IneqCnstr) : UnsatProof

instance Lean.Meta.Grind.Arith.Linear.instInhabitedDiseqCnstr : Inhabited DiseqCnstr

Equations

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

instance Lean.Meta.Grind.Arith.Linear.instInhabitedEqCnstr : Inhabited EqCnstr

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Linear.VarSet : Type

Equations

• Lean.Meta.Grind.Arith.Linear.VarSet = Std.TreeSet Lean.Grind.Linarith.Var compare

structure Lean.Meta.Grind.Arith.Linear.Struct : Type

State for each algebraic structure by this module. Each type must at least implement the instance IntModule. For being able to process inequalities, it must at least implement Preorder, and OrderedAdd

• id : Nat
• ringId? : Option Nat

  If the structure is a ring, we store its id in the CommRing module at ringId?

• type : Expr
• u : Level

  Cached getDecLevel type

• intModuleInst : Expr

  IntModule instance

• leInst? : Option Expr

  LE instance if available

• ltInst? : Option Expr

  LT instance if available

• lawfulOrderLTInst? : Option Expr

  LawfulOrderLT instance if available

• isPreorderInst? : Option Expr

  IsPreorder instance if available

• orderedAddInst? : Option Expr

  OrderedAdd instance with IsPreorder if available

• isPartialInst? : Option Expr

  IsPartialOrder instance if available

• isLinearInst? : Option Expr

  IsLinearOrder instance if available

• noNatDivInst? : Option Expr

  NoNatZeroDivisors

• ringInst? : Option Expr

  Ring instance

• commRingInst? : Option Expr

  CommRing instance

• orderedRingInst? : Option Expr

  OrderedRing instance with Preorder

• fieldInst? : Option Expr

  Field instance

• charInst? : Option (Expr × Nat)

  IsCharP instance for type if available.

• zero : Expr
• ofNatZero : Expr
• one? : Option Expr
• leFn? : Option Expr
• ltFn? : Option Expr
• addFn : Expr
• zsmulFn : Expr
• nsmulFn : Expr
• zsmulFn? : Option Expr
• nsmulFn? : Option Expr
• homomulFn? : Option Expr
• subFn : Expr
• negFn : Expr
• vars : PArray Expr

  Mapping from variables to their denotations. Remark each variable can be in only one ring.

• varMap : PHashMap ExprPtr Var

  Mapping from Expr to a variable representing it.

• lowers : PArray (PArray IneqCnstr)

  Mapping from variables to their "lower" bounds. We say a relational constraint c is a lower bound for a variable x if x is the maximal variable in c, and x coefficient in c is negative.

• uppers : PArray (PArray IneqCnstr)

  Mapping from variables to their "upper" bounds. We say a relational constraint c is a upper bound for a variable x if x is the maximal variable in c, and x coefficient in c is positive.

• diseqs : PArray (PArray DiseqCnstr)

  Mapping from variables to their disequalities. We say a disequality constraint c is a disequality for a variable x if x is the maximal variable in c.

• assignment : PArray Rat

  Partial assignment being constructed by linarith.

• caseSplits : Bool

  caseSplits is true if linarith is searching for model and already performed case splits. This information is used to decide whether a conflict should immediately close the current grind goal or not.

• conflict? : Option UnsatProof

  conflict? is some .. if a contradictory constraint was derived. This field is only set when caseSplits is true. Otherwise, we can convert UnsatProof into a Lean term and close the current grind goal.

• diseqSplits : PHashMap Poly FVarId

  Cache decision variables used when splitting on disequalities. This is necessary because the same disequality may be in different conflicts.

• elimEqs : PArray (Option EqCnstr)

  Mapping from variable to equation constraint used to eliminate it. solved variables should not occur in diseqs, lowers, or uppers.

• elimStack : List Var

  Elimination stack. For every variable in elimStack. If x in elimStack, then elimEqs[x] is not none.

• occurs : PArray VarSet

  Mapping from variable to occurrences. For example, an entry x ↦ {y, z} means that x may occur in lowers, or uppers, or diseqs of variables y and z. If x occurs in diseqs[y], lowers[y], or uppers[y], then y is in occurs[x], but the reverse is not true. If x is in elimStack, then occurs[x] is the empty set.

• ignored : PArray Expr

  Linear constraints that are not supported. We use this information for diagnostics. TODO: store constraints instead.

instance Lean.Meta.Grind.Arith.Linear.instInhabitedStruct : Inhabited Struct

Equations

• Lean.Meta.Grind.Arith.Linear.instInhabitedStruct = { default := Lean.Meta.Grind.Arith.Linear.instInhabitedStruct.default }

def Lean.Meta.Grind.Arith.Linear.instInhabitedStruct.default : Struct

Equations

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

structure Lean.Meta.Grind.Arith.Linear.NatStruct : Type

• id : Nat
• structId : Nat

  Id for OfNatModule.Q

• type : Expr
• u : Level

  Cached getDecLevel type

• natModuleInst : Expr

  NatModule instance for type

• leInst? : Option Expr

  LE instance if available

• ltInst? : Option Expr

  LT instance if available

• lawfulOrderLTInst? : Option Expr

  LawfulOrderLT instance if available

• isPreorderInst? : Option Expr

  IsPreorder instance if available

• orderedAddInst? : Option Expr

  OrderedAdd instance with IsPreorder if available

• isLinearInst? : Option Expr

  IsLinearOrder instance if available

• addRightCancelInst? : Option Expr
• rfl_q : Expr
• zero : Expr
• toQFn : Expr
• addFn : Expr
• smulFn : Expr
• termMap : PHashMap ExprPtr (Expr × Expr)

structure Lean.Meta.Grind.Arith.Linear.State : Type

State for all IntModule types detected by grind.

• structs : Array Struct

  Structures detected. We expect to find a small number of IntModules in a given goal. Thus, using Array is fine here.

• 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
• forbiddenNatModules : PHashSet ExprPtr

  Some types are unordered rings, so we do not process them in linarith. When such types are detected in getStructId?, we add them to the set forbiddenNatModules to avoid reprocessing them in getNatStructId?.

• natStructs : Array NatStruct

  NatModule. We support them using the envelope OfNatModule.Q

• natTypeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "nat module id". We cache failures using none. natTypeIdOf[type] is some id, then id < natStructs.size. If a type is in this map, it is not in typeIdOf.

• exprToNatStructId : PHashMap ExprPtr Nat

def Lean.Meta.Grind.Arith.Linear.instInhabitedState.default : State

Equations

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

instance Lean.Meta.Grind.Arith.Linear.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Arith.Linear.instInhabitedState = { default := Lean.Meta.Grind.Arith.Linear.instInhabitedState.default }

opaque Lean.Meta.Grind.Arith.Linear.linearExt : SolverExtension State