Commit 3e6b76a1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

New release.

parent ce00e568
Guillaume Melquiond <guillaume.melquiond@inria.fr>
Authors of the CoqApprox files are:
Érik Martin-Dorel <erik.martin-dorel@ens-lyon.org>
Micaela Mayero <micaela.mayero@lipn.univ-paris13.fr>
Ioana Pasca <ioana.pasca@iut-nimes.fr>
Laurence Rideau <laurence.rideau@inria.fr>
Laurent Théry <laurent.thery@inria.fr>
This diff is collapsed.
......@@ -2,8 +2,9 @@ Prerequisites
-------------
You will need the Coq proof assistant (>= 8.4) with a Reals theory compiled
in. You will need the Flocq library (http://flocq.gforge.inria.fr/) to be
installed too.
in. You will also need the Flocq library (>= 2.4, http://flocq.gforge.inria.fr/)
and the Ssreflect and Mathematical Components libraries
(http://ssr.msr-inria.inria.fr/).
The .tar.gz file is distributed with a working set of configure files. They
are not in the git repository though. Consequently, if you are building from
......
Version 2.0.0:
- added support for Taylor models (i_bisect_taylor)
- added support for logarithm
- improved tactic so that it handles hypotheses with non floating-point bounds
Version 1.1.0:
- moved to Flocq 2.4
- added support for disequalities to the tactic
......
......@@ -3,8 +3,8 @@ 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). Author is Guillaume Melquiond <guillaume.melquiond@inria.fr>.
under the terms of CeCILL-C Free Software License (see the COPYING file).
Main author is Guillaume Melquiond <guillaume.melquiond@inria.fr>.
I. Invocation
......@@ -35,10 +35,10 @@ The complete list of recognized goals is as follows:
(e1 <> e2)%R handled as (e1 - e2 <> 0)%R
Operators recognized by the tactic are: PI, Ropp, Rabs, Rinv, Rsqr, sqrt,
cos, sin, tan, atan, exp, pow, powerRZ, Rplus, Rminus, Rmult, Rdiv. There
are a some restrictions on the domain of a few functions: pow and powerRZ
should be written with a numeric exponent; the input of cos and sin
should be between -2*PI and 2*PI; the input of tan should be between
cos, sin, tan, atan, exp, ln, pow, powerRZ, Rplus, Rminus, Rmult, Rdiv.
There are some restrictions on the domain of a few functions: pow and
powerRZ should be written with a numeric exponent; the input of cos and
sin should be between -2*PI and 2*PI; the input of tan should be between
-PI/2 and PI/2.
A helper tactic "interval_intro e" is also available. Instead of proving
......@@ -64,9 +64,9 @@ 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^n 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
i_bisect_diff (x:R) same as i_bisect, but studies variations along x too
i_bisect_taylor (x:R) (d:nat)
same as bisect_diff, but computes degree-d Talor
same as i_bisect_diff, but computes degree-d Taylor
models instead of performing automatic differentiation
For both tactics, performing a bisection of depth 1 is not much slower
......
AC_INIT([Interval], [1.1.0],
AC_INIT([Interval], [2.0.0],
[Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[interval])
......
......@@ -348,8 +348,8 @@ https://github.com/apenwarr/redo for an implementation and some comprehensive do
\section sec-licensing Licensing
@author Guillaume Melquiond
@version 0.11
@date 2012-2013
@version 0.12
@date 2012-2014
@copyright
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
......@@ -2063,7 +2063,7 @@ static bool still_need_rebuild(std::string const &target)
/**
* Handle job completion.
*/
static void complete_job(int job_id, bool success)
static void complete_job(int job_id, bool success, bool started = true)
{
DEBUG << "Completing job " << job_id << '\n';
job_map::iterator i = jobs.find(job_id);
......@@ -2071,14 +2071,15 @@ static void complete_job(int job_id, bool success)
string_list const &targets = i->second.rule.targets;
if (success)
{
if (show_targets) std::cout << "Finished";
bool show = show_targets && started;
if (show) std::cout << "Finished";
for (string_list::const_iterator j = targets.begin(),
j_end = targets.end(); j != j_end; ++j)
{
update_status(*j);
if (show_targets) std::cout << ' ' << *j;
if (show) std::cout << ' ' << *j;
}
if (show_targets) std::cout << std::endl;
if (show) std::cout << std::endl;
}
else
{
......@@ -2378,7 +2379,7 @@ static void complete_request(client_t &client, bool success)
assert(i != jobs.end());
if (still_need_rebuild(i->second.rule.targets.front()))
run_script(client.job_id, i->second);
else complete_job(client.job_id, true);
else complete_job(client.job_id, true, false);
}
else complete_job(client.job_id, false);
}
......
Require Import Reals Interval_tactic.
Local Open Scope R_scope.
(* Define a bound "b" a bit less than PI/2 *)
Notation b := (157 / 100) (only parsing).
Goal forall x : R, Rabs x <= b -> 0 <= sin (Rabs x).
intros x Hx.
(* BEGIN bookkeeping *)
interval_intro b upper as Hr.
apply Rle_trans with (2 := Hr) in Hx.
(* END bookkeeping *)
interval_intro (sin (Rabs x)) lower
with (i_bisect_taylor x 0, i_depth 1, i_prec 32) as test.
(* test : -1 * / 4294967296 <= sin (Rabs x) *)
clear test.
interval with (i_depth 0, i_prec 0).
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment