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