The 4.5.0 release of Interval comes with a new pair of tactics: `root`

and `root_intro`

. Contrarily to the original tactics `interval`

and `integral`

(and their `*_intro`

counterparts), `root`

does not compute a new enclosure by forward interval analysis. Instead, it refines an existing enclosure according to a given equation using Newton’s method.

Let us illustrate the `root`

tactic with the quintic equation x^5 - x - 1 = 0, which has a single real root. It is well-known that this root is impossible to express with radicals.

```
From Coq Require Import Reals.
From Interval Require Import Tactic Plot.
Open Scope R_scope.
Plot ltac:(plot (fun x => x^5 - x - 1) 1.1 1.2).
```

Yet, we might need some information about this root. And a good way to start is to compute a very tight enclosure of it.

```
Notation "x = y ± z" := (Rle (Rabs (x - y)) z) (at level 70, y at next level).
Lemma quintic1 x : x * (x^4 - 1) = 1 -> x = 1.1673039782614185 ± 1e-14.
Proof.
intros H.
root H. (* Finished transaction in 0.021 secs *)
Qed.
```

We have cheated a bit in the example above, as x^5 - x was rewritten into x (x^4 - 1). Indeed, with the earlier form, the tactic struggles to prove that there is no root near +\infty, while it succeeds with the latter form. This issue could easily be solved by using the `ring`

tactic to switch between both forms at the start of the proof, but let us consider a different approach.

We split the problem into two separate sub-cases: x \le 2 and x \ge 2. In the first case, the `root`

tactic refines the hypothesis `H': x <= 2`

using the equation `H: x^5 - x = 1`

until it reaches a tight enclosure of x. In the second case, we prove that the polynomial is equivalent to x^5 near +\infty and thus has no large root, using `field`

and `interval`

.

```
Lemma quintic2 x : x^5 - x = 1 -> x = 1.1673039782614185 ± 1e-14.
Proof.
intros H.
destruct (Rle_or_lt x 2) as [H'|H'].
- root H.
- elim Rgt_not_eq with (2 := H).
replace (x^5 - x) with (x^5 * (1 - /x^4)) ; [|field] ; interval.
Qed.
```

As with the other tactics, `root`

also works for tactic-in-term definitions, for those of you who use Coq as a beefed-up pocket calculator.

```
Definition quintic3 x := ltac:(root (x * (x^4 - 1) - 1)).
(* quintic3 : forall x : R, x * (x ^ 4 - 1) - 1 = 0 ->
5257069761526221 / 4503599627370496 <= x <= 5257069761526224 / 4503599627370496 *)
Definition quintic4 x `(x <= 2) := ltac:(root (x^5 = x + 1)).
(* quintic4 : forall x : R, x <= 2 -> x ^ 5 = x + 1 ->
5257069761526221 / 4503599627370496 <= x <= 5257069761526225 / 4503599627370496 *)
```

The examples above are all about polynomials, but the tactic actually works with all the functions supported by the library:

```
Goal forall x:R, 999 <= x <= 1000 -> sin x = 0 -> x = 318 * PI ± 1e-20.
Proof.
intros x Hx Hs.
root Hs with (i_prec 100).
(* Finished transaction in 0.106 secs *)
Qed.
Definition equal_0_442854401002 x := ltac:(root (exp x = 2 - x)).
```