ring tactic

A tactic for solving equations in commutative (semi)rings, where the exponents can also contain variables. Based on http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf .

More precisely, expressions of the following form are supported:

• constants (non-negative integers)
• variables
• coefficients (any rational number, embedded into the (semi)ring)
• addition of expressions
• multiplication of expressions (a * b)
• scalar multiplication of expressions (n • a; the multiplier must have type ℕ)
• exponentiation of expressions (the exponent must have type ℕ)
• subtraction and negation of expressions (if the base is a full ring)

The normalization procedure is implemented in Mathlib.Tactic.Ring.Common.

Tags

ring, semiring, exponent, power

class Mathlib.Tactic.Ring.CSLift (α : Type u) (β : outParam (Type u)) : Type u

CSLift α β is a typeclass used by ring for lifting operations from α (which is not a commutative semiring) into a commutative semiring β by using an injective map lift : α → β.

• lift : α → β

  lift is the "canonical injection" from α to β

• inj : Function.Injective lift

  lift is an injective function

class Mathlib.Tactic.Ring.CSLiftVal {α : Type u} {β : outParam (Type u)} [CSLift α β] (a : α) (b : outParam β) : Prop

CSLiftVal a b means that b = lift a. This is used by ring to construct an expression b from the input expression a, and then run the usual ring algorithm on b.

• eq : b = CSLift.lift a

  The output value b is equal to the lift of a. This can be supplied by the default instance which sets b := lift a, but ring will treat this as an atom so it is more useful when there are other instances which distribute addition or multiplication.

@[instance 100]

instance Mathlib.Tactic.Ring.instCSLiftValLift {α β : Type u_1} [CSLift α β] (a : α) : CSLiftVal a (CSLift.lift a)

theorem Mathlib.Tactic.Ring.of_lift {α β : Type u_1} [inst : CSLift α β] {a b : α} {a' b' : β} [h1 : CSLiftVal a a'] [h2 : CSLiftVal b b'] (h : a' = b') : a = b

theorem Mathlib.Tactic.Ring.of_eq {α : Sort u_1} {a b c : α} : a = c → b = c → a = b

opaque Mathlib.Tactic.Ring.ringCleanupRef : IO.Ref (Lean.Expr → Lean.MetaM Lean.Expr)

This is a routine which is used to clean up the unsolved subgoal of a failed ring1 application. It is overridden in Mathlib/Tactic/Ring/RingNF.lean to apply the ring_nf simp set to the goal.

def Mathlib.Tactic.Ring.proveEq (g : Lean.MVarId) : AtomM Unit

Frontend of ring1: attempt to close a goal g, assuming it is an equation of semirings.

def Mathlib.Tactic.Ring.ring1 : Lean.ParserDescr

ring1 solves the goal when it is an equality in commutative (semi)rings, allowing variables in the exponent.

This version of ring fails if the target is not an equality.

• ring1! uses a more aggressive reducibility setting to determine equality of atoms.

Extensions:

• • ring1_nf additionally uses ring_nf to simplify in atoms.
  • ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.

def Mathlib.Tactic.Ring.tacticRing1! : Lean.ParserDescr

ring1 solves the goal when it is an equality in commutative (semi)rings, allowing variables in the exponent.

This version of ring fails if the target is not an equality.

• ring1! uses a more aggressive reducibility setting to determine equality of atoms.

Extensions:

• • ring1_nf additionally uses ring_nf to simplify in atoms.
  • ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.