@[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.hashPoly✝ }

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.hashExpr✝ }

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

• 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
• 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 = Lean.RBTree 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

• preorderInst? : Option Expr

  Preorder instance if available

• orderedAddInst? : Option Expr

  OrderedAdd instance with Preorder if available

• partialInst? : Option Expr

  PartialOrder instance if available

• linearInst? : Option Expr

  LinearOrder 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

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

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

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

Equations

• Lean.Meta.Grind.Arith.Linear.instInhabitedState = { default := { structs := default, typeIdOf := default, exprToStructId := default } }