# Interval 4.5, now with root finding

**URL:** <https://discourse.rocq-prover.org/t/interval-4-5-now-with-root-finding/1620>\
**Category:** Announcements\
**Created:** [March 31, 2022, 7:51am UTC](https://discourse.rocq-prover.org/t/interval-4-5-now-with-root-finding/1620 "2022-03-31T07:51:11Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [March 31, 2022, 7:51am UTC](https://discourse.rocq-prover.org/t/interval-4-5-now-with-root-finding/1620/1 "2022-03-31T07:51:11Z")

</div>

The 4.5.0 release of [Interval](https://coqinterval.gitlabpages.inria.fr/) 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.

```coq
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.

```coq
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`.

```coq
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.

```coq
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:

```coq
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)).

```

---

<div class="post-metadata">

**Author:** ![MSoegtrop](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@MSoegtrop](https://discourse.rocq-prover.org/u/MSoegtrop)\
**Post date:** [March 31, 2022, 8:20am UTC](https://discourse.rocq-prover.org/t/interval-4-5-now-with-root-finding/1620/2 "2022-03-31T08:20:06Z")

</div>

Very nice and very useful. Thank you!