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.MonadRing (m : Type → Type) : Type

• getRing : m Ring
• modifyRing : (Ring → Ring) → m Unit
• canonExpr : Expr → m Expr

  Helper function for removing dependency on GoalM. In RingM and SemiringM, this is just sharedCommon (← canon e) When printing counterexamples, we are at MetaM, and this is just the identity function.

• synthInstance? : Expr → m (Option Expr)

  Helper function for removing dependency on GoalM. During search we want to track the instances synthesized by grind, and this is Grind.synthInstance.

@[always_inline]

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.MonadRing.synthInstance {m : Type → Type} [Monad m] [MonadError m] [MonadRing m] (type : Expr) : m Expr

Equations

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

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

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.instMonadRingRingM : MonadRing RingM

Equations

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

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

• semiringId : Nat

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.SemiringM.run semiringId x = x { semiringId := semiringId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.getSemiringId : SemiringM Nat

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getSemiring : SemiringM Semiring

Equations

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

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

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingSemiringM : MonadRing SemiringM

Equations

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

@[inline]

def Lean.Meta.Grind.Arith.CommRing.modifySemiring (f : Semiring → Semiring) : SemiringM 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.getTermSemiringId? (e : Expr) : GoalM (Option Nat)

Equations

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

def Lean.Meta.Grind.Arith.CommRing.setTermSemiringId (e : Expr) : SemiringM 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] [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] [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.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.Meta.Grind.Arith.CommRing.isField : RingM Bool

Equations

• Lean.Meta.Grind.Arith.CommRing.isField = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing 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.getRing 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.

def Lean.Meta.Grind.Arith.CommRing.getAddFn {m : Type → Type} [MonadError m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getSubFn {m : Type → Type} [MonadError m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getMulFn {m : Type → Type} [MonadError m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getNegFn {m : Type → Type} [MonadError m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getInvFn {m : Type → Type} [MonadError m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getIntCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadRing m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getOne {m : Type → Type} [Monad m] [MonadRing m] [MonadLiftT GoalM m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getAddFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getMulFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getPowFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getNatCastFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getToQFn : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getAddRightCancelInst? : SemiringM (Option Expr)

Equations

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