Interval package for Coq

This library provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

This package is free software; you can redistribute it and/or modify it under the terms of GNU Lesser General Public License (see the COPYING file in the archive).

Download: version 0.11.

As this library relies on the fast integer library, version 8.2 of Coq is expected for compiling it. By modifying the first lines of the tactics.v file and removing the offending files, the library might be usable with older versions of Coq. The library can be compiled by issuing the command make.

Invocation

In order to use the tactics of the library, one has to import the Interval_tactic file into a Coq proof script. The main tactic is named interval.

The tactic can be applied on a goal of the form (f1 <= e <= f2)%R with e an expression involving the usual arithmetic operators + - * / and sqrt. Sub-expressions not starting with such operators have to be, either terms t appearing in hypothesis inequalities (f3 <= t <= f4)%R or simple integers. The bounds f1 f2 ... are binary floating-point numbers: either relative integers or quotients of relative integers by power-of-two, e.g. (42)%R or (-17/8)%R. The following inequalities are also recognized:

• (e <= f)%R;
• (f <= e)%R;
• (Rabs e <= f)%R, handled as (-f <= e <= f)%R.

Hint: When trying to prove a proposition (e1 <= e2)%R where neither sides are floating-point numbers, applying Rminus_le will change the proposition to (e1 - e2 <= 0)%R, hence bringing out a floating-point bound.

A helper tactic interval_intro e is also available. Instead of proving the current goal, it computes an enclosure of the expression e passed as argument and it introduces the inequalities into the proof context. If only one bound is needed, the keywords lower and upper can be passed to the tactic, so that it does not perform useless computations. For example, interval_intro e lower introduces only a floating-point lower bound of e in the context.

Fine-tuning

The behavior of the tactics can be tuned by adding an optional set of parameters with (param1, param2, ...) at the end of the tactics. These parameters are parsed from left to right: If some parameters are conflicting, the earlier ones are discarded. Available parameter classes are: (with the type of their arguments, if any)

• i_prec (p:nat) sets precision of the floating-point computations;
• i_depth (n:nat) sets bisection depth (2ⁿ sub-intervals at most);
• i_bisect (x:R) splits input interval on x and repeat until proven;
• i_bisect_diff (x:R), same as bisect, but studies variations along x too;

Notes on bisection: For both tactics, performing a bisection of depth 1 is not much slower than performing no bisection. If the current goal can be proven by interval with a bisection of depth n, then increasing the depth to n + 1 will not have any noticeable effect. For interval_intro, increasing the depth from n to n + 1 can, however, double the computation time. Performing an i_bisect_diff bisection has a much higher cost per sub-interval, but it can considerably reduce the amount of sub-intervals considered. As a consequence, unless there is a huge amount of trivial propositions to prove, one should use this improved bisection.

The default parameters of the tactics are (i_prec 30) and no bisection. If the user enables a bisection, the default depth is (i_depth 15) for interval and (i_depth 5) for interval_intro.

Examples

(** BEGIN **)
Require Import Reals.
Require Import Interval_tactic.

Goal
  forall x, (-1 <= x <= 1)%R ->
  (sqrt (1 - x) <= 3/2)%R.
Proof.
  intros.
  interval.
Qed.

Goal
  forall x, (-1 <= x <= 1)%R ->
  (sqrt (1 - x) <= 141422/100000)%R.
Proof.
  intros.
  apply Rminus_le.
  interval.
Qed.

Goal
  forall x, (-1 <= x <= 1)%R ->
  (sqrt (1 - x) <= 141422/100000)%R.
Proof.
  intros.
  interval_intro (sqrt (1 - x)) upper.
  apply Rle_trans with (1 := H0).
  interval.
Qed.

Goal
  forall x, (3/2 <= x <= 2)%R ->
  forall y, (1 <= y <= 33/32)%R ->
  (Rabs (sqrt(1 + x/sqrt(x+y)) - 144/1000*x - 118/100) <= 71/32768)%R.
Proof.
  intros.
  interval with (i_prec 19, i_bisect x).
Qed.

Goal
  forall x, (1/2 <= x <= 2)%R ->
  (Rabs (sqrt x - (((((122 / 7397 * x + (-1733) / 13547) * x
                   + 529 / 1274) * x + (-767) / 999) * x
                   + 407 / 334) * x + 227 / 925))
    <= 5/65536)%R.
Proof.
  intros.
  interval with (i_bisect_diff x).
Qed.
(*** END ***)