def Lean.Meta.Grind.Arith.CommRing.get' : GoalM State

Equations

• Lean.Meta.Grind.Arith.CommRing.get' = do let __do_lift ← get pure __do_lift.arith.ring

@[inline]

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.checkMaxSteps : GoalM Bool

Equations

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

def Lean.Meta.Grind.Arith.CommRing.incSteps : GoalM Unit

Equations

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

structure Lean.Meta.Grind.Arith.CommRing.RingM.Context : Type

• ringId : Nat
• checkCoeffDvd : Bool

  If checkCoeffDvd is true, then when using a polynomial k*m - p to simplify .. + k'*m*m_2 + ..., the substitution is performed IF

  • k divides k', OR
  • Ring implements NoNatZeroDivisors.

  We need this check when simplifying disequalities. In this case, if we perform the simplification anyway, we may end up with a proof that k * q = 0, but we cannot deduce q = 0 since the ring does not implement NoNatZeroDivisors See comment at PolyDerivation.

class Lean.Meta.Grind.Arith.CommRing.MonadGetRing (m : Type → Type) : Type

• getRing : m Ring

Instances

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingOfMonadLift
• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingReaderTRingMetaM
• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM

@[always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetRing m] : MonadGetRing n

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingOfMonadLift m n = { getRing := liftM Lean.Meta.Grind.Arith.CommRing.getRing }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.RingM (α : Type) : Type

We don't want to keep carrying the RingId around.

Equations

• Lean.Meta.Grind.Arith.CommRing.RingM = ReaderT Lean.Meta.Grind.Arith.CommRing.RingM.Context Lean.Meta.Grind.GoalM

Instances For

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.RingM.run {α : Type} (ringId : Nat) (x : RingM α) : GoalM α

Equations

• Lean.Meta.Grind.Arith.CommRing.RingM.run ringId x = x { ringId := ringId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.getRingId : RingM Nat

Equations

• Lean.Meta.Grind.Arith.CommRing.getRingId = do let __do_lift ← read pure __do_lift.ringId

def Lean.Meta.Grind.Arith.CommRing.RingM.getRing : RingM Ring

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM : MonadGetRing RingM

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM = { getRing := Lean.Meta.Grind.Arith.CommRing.RingM.getRing }

@[inline]

def Lean.Meta.Grind.Arith.CommRing.modifyRing (f : Ring → Ring) : RingM Unit

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd {α : Type} (x : RingM α) : RingM α

Equations

• Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd x = withReader (fun (ctx : Lean.Meta.Grind.Arith.CommRing.RingM.Context) => { ringId := ctx.ringId, checkCoeffDvd := true }) x

def Lean.Meta.Grind.Arith.CommRing.checkCoeffDvd : RingM Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.checkCoeffDvd = do let __do_lift ← read pure __do_lift.checkCoeffDvd

def Lean.Meta.Grind.Arith.CommRing.getTermRingId? (e : Expr) : GoalM (Option Nat)

Equations

• Lean.Meta.Grind.Arith.CommRing.getTermRingId? e = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.get' pure (Lean.PersistentHashMap.find? __do_lift.exprToRingId { expr := e })

def Lean.Meta.Grind.Arith.CommRing.setTermRingId (e : Expr) : RingM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.nonzeroChar? {m : Type → Type} [Monad m] [MonadGetRing m] : m (Option Nat)

Returns some c if the current ring has a nonzero characteristic c.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.nonzeroCharInst? {m : Type → Type} [Monad m] [MonadGetRing m] : m (Option (Expr × Nat))

Returns some (charInst, c) if the current ring has a nonzero characteristic c.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.noZeroDivisorsInst? : RingM (Option Expr)

Equations

• Lean.Meta.Grind.Arith.CommRing.noZeroDivisorsInst? = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure __do_lift.noZeroDivInst?

def Lean.Meta.Grind.Arith.CommRing.noZeroDivisors : RingM Bool

Returns true if the current ring satisfies the property

∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0

Equations

• Lean.Meta.Grind.Arith.CommRing.noZeroDivisors = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure __do_lift.noZeroDivInst?.isSome

def Lean.Meta.Grind.Arith.CommRing.hasChar : RingM Bool

Returns true if the current ring has a IsCharP instance.

Equations

• Lean.Meta.Grind.Arith.CommRing.hasChar = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure __do_lift.charInst?.isSome

def Lean.Meta.Grind.Arith.CommRing.getCharInst : RingM (Expr × Nat)

Returns the pair (charInst, c). If the ring does not have a IsCharP instance, then throws internal error.

Equations

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

def Lean.Grind.CommRing.Expr.toPolyM (e : Meta.Grind.Arith.CommRing.RingExpr) : Meta.Grind.Arith.CommRing.RingM Poly

Converts the given ring expression into a multivariate polynomial. If the ring has a nonzero characteristic, it is used during normalization.

Equations

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

def Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p.mulConstM k = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.nonzeroChar? pure (p.mulConst' k __do_lift)

def Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p.mulMonM k m = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.nonzeroChar? pure (p.mulMon' k m __do_lift)

def Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p₁.mulM p₂ = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.nonzeroChar? match __do_lift with | some c => pure (p₁.mulC p₂ c) | x => pure (p₁.mul p₂)

def Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM Poly

Equations

• p₁.combineM p₂ = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.nonzeroChar? pure (p₁.combine' p₂ __do_lift)

def Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : Meta.Grind.Arith.CommRing.RingM SPolResult

Equations

• p₁.spolM p₂ = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.nonzeroChar? match __do_lift with | some c => pure (p₁.spol p₂ (some c)) | x => pure (p₁.spol p₂)

def Lean.Meta.Grind.Arith.CommRing.isQueueEmpty : RingM Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isQueueEmpty = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure (Lean.RBTree.isEmpty __do_lift.queue)

def Lean.Meta.Grind.Arith.CommRing.getNext? : RingM (Option EqCnstr)

Equations

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