.. _tac_norm_num:

norm_num
========

Summary
-------

The ``norm_num`` tactic solves equalities and inequalities which involve only normalised numerical expressions. It doesn't deal with variables, but it will prove things like ``A = B``, ``A ≤ B``, ``A < B`` and ``A ≠ B``, as long as ``A`` and ``B`` involve only numbers like ``-37/5``. 

Examples
--------

(with ``data.real.basic`` imported to get the reals, and of course ``tactic`` imported to get the tactics)

.. code-block::

   example : (1 : ℝ) + 1 = 2 :=
   begin
     norm_num,
   end

   example : (1 : ℝ) + 1 ≤ 3 :=
   begin
     norm_num,
   end

   example : (1 : ℝ) + 1 < 4 :=
   begin
     norm_num,
   end

   example : (1 : ℝ) + 1 ≠ 5 :=
   begin
     norm_num,
   end

I put a comma after ``norm_num`` so that I can check that the "goals accomplished" message is there.

``norm_num`` also knows about a few other things; for example it seems to know about the absolute value on the real numbers.

.. code-block::

   example : |(3 : ℝ) - 7| = 4 :=
   begin
     norm_num,
   end