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.checkMaxDegree (p : Poly) : GoalM Bool

Equations

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

def Lean.Meta.Grind.Arith.CommRing.incSteps (n : Nat := 1) : 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.

  We also need it when destructively simplifying equations, i.e., when replacing an equation with its simplified form (EqCnstr.simplify and EqCnstr.simplifyBasis): the rewrite multiplies the equation by k₁ = k/gcd k k', and the result is weaker than the original equation when k₁ ≠ ±1. See Note at EqCnstr.simplify.

@[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

@[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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonRingM : Sym.Arith.MonadCanon RingM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.RingM.getCommRing : RingM Sym.Arith.CommRing

The Sym.Arith classification record of the current ring.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.RingM.modifyCommRing (f : Sym.Arith.CommRing → Sym.Arith.CommRing) : RingM Unit

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingRingM : Sym.Arith.MonadCommRing RingM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.RingM.getCommRingState : RingM CommRingState

The per-goal solver state of the current ring.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.RingM.modifyCommRingState (f : CommRingState → CommRingState) : RingM Unit

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingStateRingM : MonadCommRingState RingM

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetVarRingM : Sym.Arith.MonadGetVar RingM

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.nonzeroChar? {m : Type → Type} [Monad m] [Sym.Arith.MonadRing 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] [Sym.Arith.MonadRing 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.Sym.Arith.getCommRing 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.Sym.Arith.getCommRing 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.Sym.Arith.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.Meta.Grind.Arith.CommRing.isField : RingM Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isField = do let __do_lift ← Lean.Meta.Sym.Arith.getCommRing pure __do_lift.fieldInst?.isSome

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.getCommRingState pure (Std.TreeSet.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.

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

• setTermId : Expr → m Unit

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.mkVarCore {m : Type → Type} [MonadLiftT GoalM m] [Monad m] [MonadRingState m] [MonadSetTermId m] (e : Expr) : m Var

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdRingM : MonadSetTermId RingM

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdRingM = { setTermId := fun (e : Lean.Expr) => Lean.Meta.Grind.Arith.CommRing.setTermRingId e }

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadMkVarRingM : Sym.Arith.MonadMkVar RingM

Every term reified by the ring solver has been internalized, together with its subterms, before reification: the internalize hook runs after the core has created the ENodes of a term and its arguments, and solver-built terms are internalized where they are built.

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getOne : RingM Expr

The numeral 1 of the current ring, internalized as a ring term of the current goal. The term is cached in the Sym.Arith record and thus shared by all goals, but internalization is per goal. The term may already be known to the core (e.g., as a subterm of a product) without having been registered by the ring solver, so the check is against the ring's own denote map.

Equations

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