.. _tac_ring:

ring
====

Summary
-------

The ``ring`` tactic proves identities in commutative rings such as ``(x+y)^2=x^2+2*x*y+y^2``. It works on concrete rings such as ``ℝ`` and abstract rings, and will also prove some results in "semirings" such as ``ℕ``. 

Note that ``ring`` does not and cannot look at hypotheses. See the examples for various ways of working around this. 

Examples
--------

1) A basic example is

.. code-block::

   example (x y : ℝ) : x^3-y^3=(x-y)*(x^2+x*y+y^2) :=
   begin
     ring
   end

2) Note that ``ring`` cannot use hypotheses -- the goal has to be an
identity. For example faced with

.. code-block::

   x y : ℝ
   h : x = y ^ 2
   ⊢ x ^ 2 = y ^ 4

the ``ring`` tactic will not close the goal, because it does not know about ``h``. The way to solve this goal is ``rw h, ring``. 

3) Sometimes you are in a situation where you cannot ``rw`` the hypothesis you want to use. For example if the tactic state is

.. code-block::

   x y : ℝ
   h : x ^ 2 = y ^ 2
   ⊢ x ^ 4 = y ^ 4

then ``rw h`` will fail (of course we know that ``x^4=(x^2)^2``, but ``rw`` works up to syntactic equality and it cannot see an ``x^2`` in the goal). In this situation we can use ``ring`` to prove an intermediate result and then rewrite our way out of trouble. For example this goal can be solved in the following way.

.. code-block::

   example (x y : ℝ) (h : x^2 = y^2) : x^4 = y^4 :=
   begin
     have h2 : x^4=(x^2)^2, -- introduce a new goal
     { ring }, -- proves ``h2``; note that the `{...}` brackets are good practice 
               -- when there is more than one goal
     rw h2, -- goal now ``⊢ (x ^ 2) ^ 2 = y ^ 4``...
     rw h, -- ...so ``rw h`` now works, giving us ``⊢ (y ^ 2) ^ 2 = y ^ 4``
     ring,
   end

Further notes
-------------

There's a variant of ``ring`` called ``ring!`` but I don't know a concrete example where one works and the other doesn't.

``ring`` is a "finishing tactic"; this means that it should only be used to close goals. If ``ring`` does not close a goal it will issue a warning that you should use the related tactic ``ring_nf``.

``ring`` might not work sometimes with variable exponents like ``x^n``. The variant ``ring_exp`` is better at dealing with them.

The algorithm used in the ``ring`` tactic is based on the 2005 paper "Proving Equalities in a Commutative Ring Done Right in Coq" by Benjamin Grégoire and Assia Mahboubi.