structure Lean.Meta.Grind.Arith.Cutsat.ToIntThms : Type

Theorems for operators that have support for i.wrap over i.wrap simplification. Currently only addition and multiplication have wrap cancellation theorems

• c? : Option Expr

  Basic theorem of the form

  toInt a = a' → toInt b = b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')`
  

• c_ww? : Option Expr

  Left-right wrap cancellation theorem of the form

  toInt a = i.wrap a' → toInt b = i.wrap b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
  

• c_wl? : Option Expr

  Left wrap cancellation theorem of the form

  toInt a = i.wrap a' → toInt b = b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
  

• c_wr? : Option Expr

  Right wrap cancellation theorem of the form

  toInt a = a' → toInt b = i.wrap b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
  

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms : Inhabited ToIntThms

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms.default }

structure Lean.Meta.Grind.Arith.Cutsat.SymbolicBound : Type

• val : Expr
• ival? : Option Int

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound : Inhabited SymbolicBound

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound.default }

def Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.isNumeral (b : SymbolicBound) : Bool

Equations

• b.isNumeral = b.ival?.isSome

inductive Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval : Type

Similar to IntInterval, but with symbolic bounds.

• co (lo hi : SymbolicBound) : SymbolicIntInterval
• ci (lo : SymbolicBound) : SymbolicIntInterval
• io (hi : SymbolicBound) : SymbolicIntInterval
• ii : SymbolicIntInterval

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval : Inhabited SymbolicIntInterval

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval.default }

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.isFinite (i : SymbolicIntInterval) : Bool

Equations

• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo hi).isFinite = true
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo).isFinite = false
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi).isFinite = false
• Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii.isFinite = false

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.lo? (i : SymbolicIntInterval) : Option SymbolicBound

Equations

• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo hi).lo? = some lo
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo).lo? = some lo
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi).lo? = none
• Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii.lo? = none

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.hi? (i : SymbolicIntInterval) : Option SymbolicBound

Equations

• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co lo hi).hi? = some hi
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi).hi? = some hi
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo).hi? = none
• Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii.hi? = none

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.wrap (i : SymbolicIntInterval) (x : Expr) : MetaM Expr

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo).wrap x = Lean.throwError (Lean.toMessageData "`grind` internal error, `.ci` interval support has not been implemented yet")
• (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi).wrap x = Lean.throwError (Lean.toMessageData "`grind` internal error, `.io` interval support has not been implemented yet")
• Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ii.wrap x = pure x

structure Lean.Meta.Grind.Arith.Cutsat.ToIntInfo : Type

• id : Nat
• type : Expr
• u : Level
• toIntInst : Expr
• rangeExpr : Expr
• range : SymbolicIntInterval
• toInt : Expr
• wrap : Expr
• ofWrap0? : Option Expr
• ofEq : Expr
• ofDiseq : Expr
• lowerThm? : Option Expr
• upperThm? : Option Expr
• ofLE? : Option (Option Expr)
• ofNotLE? : Option (Option Expr)
• ofLT? : Option (Option Expr)
• ofNotLT? : Option (Option Expr)
• addThms? : Option ToIntThms
• mulThms? : Option ToIntThms
• subThm? : Option (Option Expr)
• negThm? : Option (Option Expr)
• divThm? : Option (Option Expr)
• modThm? : Option (Option Expr)
• powThm? : Option (Option Expr)
• zeroThm? : Option (Option Expr)
• ofNatThm? : Option (Option Expr)

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo : Inhabited ToIntInfo

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo.default }

structure Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo : Type

For each term e of type α which implements the ToInt α i class, we store its corresponding Int term eToInt, a proof he : toInt e = eToInt, and the type α.

• eToInt : Expr
• α : Expr
• he : Expr