Commit 77736b4a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improved directory structure.

parent 05f80333
Guillaume Melquiond <guillaume.melquiond@inria.fr>
Prerequisites
-------------
You will need to have the Coq proof assistant (>= 8.1) with a Reals theory
compiled in.
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
GIT, you will need autoconf (>= 2.59) and automake (>= 1.8).
Configuring, compiling and installing
-------------------------------------
Ideally, you should just have to type:
$ ./configure && make && make install
The environment variable "COQC" can be set to the Coq compiler command. The
configure script defaults to "coqc".
The option "--libdir=DIR" can be set to the directory where the compiled
library files should be installed by "make install". By default, the target
directory is "`$COQC -where`/user-contrib/Interval".
The files are compiled at a logical location starting with "Interval". This
default prefix can be removed with the "--disable-prefix" option.
PACKAGE=interval
VERSION=0.10
##########################
# #
# Variables definitions. #
# #
##########################
OPT=
COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQC=$(COQBIN)coqc
COQDOC=$(COQBIN)coqdoc
COQDEP=$(COQBIN)coqdep -c
DISTDIR=$(PACKAGE)-$(VERSION)
#########################
# #
# Libraries definition. #
# #
#########################
OCAMLLIBS=-I .
COQLIBS=-I .
###################################
# #
# Definition of the "all" target. #
# #
###################################
VFILES=bigint_carrier.v\
bisect.v\
definitions.v\
float_sig.v\
generic_ops.v\
generic_proof.v\
generic.v\
interval.v\
interval_float.v\
interval_float_full.v\
missing.v\
specific_ops.v\
specific_sig.v\
stdz_carrier.v\
tactics.v\
transcend.v\
xreal.v\
xreal_derive.v
VOFILES=$(VFILES:.v=.vo)
VIFILES=$(VFILES:.v=.vi)
GFILES=$(VFILES:.v=.g)
HTMLFILES=$(VFILES:.v=.html)
GHTMLFILES=$(VFILES:.v=.g.html)
all: $(VOFILES)
html: $(HTMLFILES)
all.ps: $(VFILES)
$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
all-gal.ps: $(VFILES)
$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
####################
# #
# Special targets. #
# #
####################
.PHONY: all opt byte archclean clean install depend html
.SUFFIXES: .v .vo .html .tex
.v.vo:
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
.v.tex:
$(COQDOC) -latex $< -o $@
.v.html:
$(COQDOC) -html $< -o $@
byte:
$(MAKE) all "OPT="
opt:
$(MAKE) all "OPT=-opt"
include .depend
.depend depend:
rm -f .depend
$(COQDEP) -i $(COQLIBS) $(VFILES) >.depend
$(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend
install:
mkdir -p `$(COQC) -where`/user-contrib
cp -f $(VOFILES) `$(COQC) -where`/user-contrib
clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) *~
rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
dist:
mkdir $(DISTDIR)
cp $(VFILES) Makefile README COPYING $(DISTDIR)
tar czf $(DISTDIR).tar.gz $(DISTDIR)
rm -r $(DISTDIR)
SUBDIRS = src
EXTRA_DIST = autogen.sh
......@@ -94,7 +94,7 @@ III. Examples
(** BEGIN **)
Require Import Reals.
Require Import tactics.
Require Import Interval_tactic.
Goal
forall x, (-1 <= x <= 1)%R ->
......
AC_INIT([Interval], [0.10],
[Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[interval])
AM_INIT_AUTOMAKE
m4_divert_push(99)
if test "$ac_init_help" = "long"; then
ac_init_help=short
fi
m4_divert_pop(99)
m4_divert_push([HELP_ENABLE])
Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Interval@:>@])
m4_divert_pop([HELP_ENABLE])
AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
AC_CHECK_TOOL(COQC, coqc)
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_CHECK_TOOL(COQDEP, coqdep)
if test "$libdir" = '${exec_prefix}/lib'; then
libdir='`$(COQC) -where`/user-contrib/Interval'
fi
AC_SUBST(COQRFLAG, ['-R . Interval'])
AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into an Interval module]),
[if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
AC_CONFIG_FILES([Makefile src/Makefile])
AC_OUTPUT
Require Import BigN.
Require Import BigZ.
Require Import Bool.
Require Import definitions.
Require Import generic.
Require Import specific_sig.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_specific_sig.
Module BigIntRadix2 <: FloatCarrier.
......
Require Import Bool.
Require Import List.
Require Import Reals.
Require Import missing.
Require Import xreal.
Require Import xreal_derive.
Require Import definitions.
Require Import generic_proof.
Require Import interval.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_xreal_derive.
Require Import Interval_definitions.
Require Import Interval_generic_proof.
Require Import Interval_interval.
Module IntervalAlgos (I : IntervalOps).
......
Require Import Reals.
Require Import ZArith.
Require Import xreal.
Require Import missing.
Require Import Interval_xreal.
Require Import Interval_missing.
Inductive rounding_mode : Set :=
rnd_UP | rnd_DN | rnd_ZR | rnd_NE.
......
Require Import ZArith.
Require Import missing.
Require Import xreal.
Require Import definitions.
Require Import generic.
Require Import generic_proof.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Module Type FloatOps.
......
Require Import Reals.
Require Import Bool.
Require Import ZArith.
Require Import xreal.
Require Import definitions.
Require Import Interval_xreal.
Require Import Interval_definitions.
Inductive float (radix : positive) : Set :=
| Fnan : float radix
......
Require Import ZArith.
Require Import missing.
Require Import xreal.
Require Import definitions.
Require Import generic.
Require Import generic_proof.
Require Import float_sig.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Require Import Interval_float_sig.
Module Type Radix.
Parameter val : positive.
......
Require Import Reals.
Require Import missing.
Require Import Interval_missing.
Require Import Bool.
Require Import ZArith.
Require Import xreal.
Require Import definitions.
Require Import generic.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_generic.
Definition exp_factor radix e :=
match e with
......
Require Import Bool.
Require Import Reals.
Require Import missing.
Require Import xreal.
Require Import definitions.
Require Import float_sig.
Require Import generic.
Require Import generic_proof.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_float_sig.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Inductive interval : Set :=
| Inan : interval
......
Require Import Bool.
Require Import Reals.
Require Import missing.
Require Import xreal.
Require Import definitions.
Require Import generic.
Require Import generic_proof.
Require Import float_sig.
Require Import interval.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Require Import Interval_float_sig.
Require Import Interval_interval.
Inductive f_interval (A : Type) : Type :=
| Inan : f_interval A
......@@ -24,8 +24,8 @@ Definition precision := F.precision.
Definition convert_bound x := FtoX (F.toF x).
Definition convert xi :=
match xi with
| Inan => interval.Inan
| Ibnd l u => interval.Ibnd (convert_bound l) (convert_bound u)
| Inan => Interval_interval.Inan
| Ibnd l u => Interval_interval.Ibnd (convert_bound l) (convert_bound u)
end.
Definition nai := @Inan F.type.
......@@ -33,12 +33,12 @@ Definition bnd := @Ibnd F.type.
Lemma bnd_correct :
forall l u,
convert (bnd l u) = interval.Ibnd (convert_bound l) (convert_bound u).
convert (bnd l u) = Interval_interval.Ibnd (convert_bound l) (convert_bound u).
split.
Qed.
Lemma nai_correct :
convert nai = interval.Inan.
convert nai = Interval_interval.Inan.
split.
Qed.
......@@ -416,7 +416,7 @@ Qed.
Theorem subset_correct :
forall xi yi : type,
subset xi yi = true -> interval.subset (convert xi) (convert yi).
subset xi yi = true -> Interval_interval.subset (convert xi) (convert yi).
intros xi yi.
case xi ; case yi ; try (simpl ; intros ; try exact I ; discriminate).
intros yl yu xl xu H.
......@@ -493,7 +493,7 @@ now apply Rmin_best.
Qed.
Definition bounded_prop xi :=
convert xi = interval.Ibnd (convert_bound (lower xi)) (convert_bound (upper xi)).
convert xi = Interval_interval.Ibnd (convert_bound (lower xi)) (convert_bound (upper xi)).
Theorem lower_bounded_correct :
forall xi,
......
Require Import Reals.
Require Import xreal.
Require Import definitions.
Require Import float_sig.
Require Import interval.
Require Import interval_float.
Require Import transcend.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_float_sig.
Require Import Interval_interval.
Require Import Interval_interval_float.
Require Import Interval_transcend.
Module FloatIntervalFull (F : FloatOps with Definition even_radix := true) <: IntervalOps.
......
Require Import ZArith.
Require Import Bool.
Require Import missing.
Require Import xreal.
Require Import definitions.
Require Import generic.
Require Import generic_proof.
Require Import float_sig.
Require Import specific_sig.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Require Import Interval_float_sig.
Require Import Interval_specific_sig.
Inductive s_float (smantissa_type exponent_type : Type) : Type :=
| Fnan : s_float smantissa_type exponent_type
......@@ -28,20 +28,20 @@ Definition type := s_float smantissa_type exponent_type.
Definition toF (x : type) :=
match x with
| Fnan => generic.Fnan radix
| Fnan => Interval_generic.Fnan radix
| Float m e =>
match mantissa_sign m with
| Mzero => generic.Fzero radix
| Mnumber s p => generic.Float radix s (MtoP p) (EtoZ e)
| Mzero => Interval_generic.Fzero radix
| Mnumber s p => Interval_generic.Float radix s (MtoP p) (EtoZ e)
end
end.
Definition fromF (f : generic.float radix) :=
Definition fromF (f : Interval_generic.float radix) :=
match f with
| generic.Fnan => Fnan
| generic.Fzero => Float mantissa_zero exponent_zero
| generic.Float false m e => Float (ZtoM (Zpos m)) (ZtoE e)
| generic.Float true m e => Float (ZtoM (Zneg m)) (ZtoE e)
| Interval_generic.Fnan => Fnan
| Interval_generic.Fzero => Float mantissa_zero exponent_zero
| Interval_generic.Float false m e => Float (ZtoM (Zpos m)) (ZtoE e)
| Interval_generic.Float true m e => Float (ZtoM (Zneg m)) (ZtoE e)
end.
Definition precision := exponent_type.
......@@ -54,10 +54,10 @@ Definition incr_prec x y := exponent_add x (ZtoE (Zpos y)).
Definition zero := Float mantissa_zero exponent_zero.
Definition nan := @Fnan smantissa_type exponent_type.
Definition nan_correct := refl_equal (generic.Fnan radix).
Definition nan_correct := refl_equal (Interval_generic.Fnan radix).
Lemma zero_correct :
toF zero = generic.Fzero radix.
toF zero = Interval_generic.Fzero radix.
generalize (mantissa_sign_correct mantissa_zero).
simpl.
case (mantissa_sign mantissa_zero).
......@@ -79,7 +79,7 @@ Definition mag (x : type) :=
Definition real (f : type) := match f with Fnan => false | _ => true end.
Lemma real_correct :
forall f, match toF f with generic.Fnan => real f = false | _ => real f = true end.
forall f, match toF f with Interval_generic.Fnan => real f = false | _ => real f = true end.
intros.
case f ; simpl.
apply refl_equal.
......@@ -149,7 +149,7 @@ Definition float_aux s m e : type :=
Lemma toF_float :
forall s p e, valid_mantissa p ->
toF (float_aux s p e) = generic.Float radix s (MtoP p) (EtoZ e).
toF (float_aux s p e) = Interval_generic.Float radix s (MtoP p) (EtoZ e).
intros.
simpl.
generalize (mantissa_sign_correct ((if s then mantissa_neg else mantissa_pos) p)).
......@@ -196,7 +196,7 @@ destruct x as [| m e].
apply refl_equal.
simpl.
rewrite (match_helper_1 _ _ (fun (s : bool) p => Float ((if s then mantissa_pos else mantissa_neg) p) e) (fun a => FtoX (toF a))).
rewrite (match_helper_1 _ _ (fun s p => generic.Float radix s (MtoP p) (EtoZ e)) (fun a => FtoX (Fneg a))).
rewrite (match_helper_1 _ _ (fun s p => Interval_generic.Float radix s (MtoP p) (EtoZ e)) (fun a => FtoX (Fneg a))).
generalize (mantissa_sign_correct m).
case_eq (mantissa_sign m).
simpl.
......@@ -231,7 +231,7 @@ destruct x as [| m e].
apply refl_equal.
simpl.
rewrite (match_helper_1 _ _ (fun (s : bool) p => Float (mantissa_pos p) e) (fun a => FtoX (toF a))).
rewrite (match_helper_1 _ _ (fun s p => generic.Float radix s (MtoP p) (EtoZ e)) (fun a => FtoX (Fabs a))).
rewrite (match_helper_1 _ _ (fun s p => Interval_generic.Float radix s (MtoP p) (EtoZ e)) (fun a => FtoX (Fabs a))).
generalize (mantissa_sign_correct m).
case_eq (mantissa_sign m).
simpl.
......@@ -479,7 +479,7 @@ Axiom round_aux_correct :
forall mode p sign m1 e1 pos,
valid_mantissa m1 ->
FtoX (toF (round_aux mode p sign m1 e1 pos)) =
FtoX (Fround_at_prec mode (prec p) (generic.Ufloat radix sign (MtoP m1) (EtoZ e1) pos)).
FtoX (Fround_at_prec mode (prec p) (Interval_generic.Ufloat radix sign (MtoP m1) (EtoZ e1) pos)).
Definition round mode prec (f : type) :=
match f with
......@@ -599,8 +599,8 @@ now case (mantissa_sign my).
intros sx px Hx (Hx1, Hx2).
rewrite (match_helper_1 _ _ (fun s py => round_aux mode p (Datatypes.xorb sx s) (mantissa_mul px py)
(exponent_add ex ey) pos_Eq) (fun a => FtoX (toF a))).
rewrite (match_helper_1 _ _ (fun s p => generic.Float radix s (MtoP p) (EtoZ ey))
(fun a => FtoX (Fmul mode (prec p) (generic.Float radix sx (MtoP px) (EtoZ ex)) a))).
rewrite (match_helper_1 _ _ (fun s p => Interval_generic.Float radix s (MtoP p) (EtoZ ey))
(fun a => FtoX (Fmul mode (prec p) (Interval_generic.Float radix sx (MtoP px) (EtoZ ex)) a))).
simpl.
generalize (mantissa_sign_correct my).
case (mantissa_sign my).
......
Require Import ZArith.
Require Import definitions.
Require Import generic.
Require Import generic_proof.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Inductive signed_number (A : Type) :=
| Mzero : signed_number A
......
Require Import ZArith.
Require Import Bool.
Require Import definitions.
Require Import generic.
Require Import specific_sig.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_specific_sig.
Module StdZRadix2 <: FloatCarrier.
......
Require Import Reals.
Require Import List.
Require Import missing.
Require Import Interval_missing.
Require Import ZArith.
Require Import BigN.
Require Import BigZ.
Require Import xreal.
Require Import definitions.
Require Import generic.
Require Import generic_proof.
(*Require Import stdz_carrier.*)
Require Import bigint_carrier.
Require Import specific_ops.
Require Import interval.
Require Import interval_float_full.
Require Import bisect.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_generic.
Require Import Interval_generic_proof.
(*Require Import Interval_stdz_carrier.*)
Require Import Interval_bigint_carrier.
Require Import Interval_specific_ops.
Require Import Interval_interval.
Require Import Interval_interval_float_full.
Require Import Interval_bisect.
(*Module C := StdZRadix2.*)
Module C := BigIntRadix2.
......@@ -44,7 +44,7 @@ Ltac get_float t :=
end in
let e := aux d in
let m := get_mantissa n in
eval vm_compute in (F.fromF (generic.Float 2 s m (Zneg e))) in
eval vm_compute in (F.fromF (Interval_generic.Float 2 s m (Zneg e))) in
let get_float_integer s t :=
let rec aux m e :=
match m with
......@@ -56,7 +56,7 @@ Ltac get_float t :=
let m := get_mantissa t in
let v := aux m Z0 in
match v with
| (?m, ?e) => eval vm_compute in (F.fromF (generic.Float 2 s m e))
| (?m, ?e) => eval vm_compute in (F.fromF (Interval_generic.Float 2 s m e))
end in
match t with
| 0%R => F.zero
......@@ -73,7 +73,7 @@ Lemma Rabs_contains :
forall f v,
contains (I.convert (I.bnd (F.neg f) f)) (Xreal v) ->
match F.toF f with
| generic.Float false m e => (Rabs v <= FtoR F.radix false m e)%R
| Interval_generic.Float false m e => (Rabs v <= FtoR F.radix false m e)%R
| _ => True
end.
intros [|m e] v (H1, H2).
......@@ -96,7 +96,7 @@ Qed.
Lemma Rabs_contains_rev :
forall f v,
match F.toF f with
| generic.Float false m e => (Rabs v <= FtoR F.radix false m e)%R
| Interval_generic.Float false m e => (Rabs v <= FtoR F.radix false m e)%R
| _ => False
end ->
contains (I.convert (I.bnd (F.neg f) f)) (Xreal v).
......@@ -320,7 +320,7 @@ Qed.
Lemma interval_helper_bisection :
forall bounds output formula prec depth n,
match bounds with
| cons (V.Bproof _ (interval_float.Ibnd l u) _) tail =>
| cons (V.Bproof _ (Interval_interval_float.Ibnd l u) _) tail =>
V.Algos.bisect_1d (fun b => nth n (V.eval_bnd prec formula (b :: map V.interval_from_bp tail)) I.nai) l u output depth = true
| _ => False
end ->
......@@ -347,7 +347,7 @@ Qed.
Lemma interval_helper_bisection_diff :
forall bounds output formula prec depth n,
match bounds with
| cons (V.Bproof _ (interval_float.Ibnd l u) _) tail =>
| cons (V.Bproof _ (Interval_interval_float.Ibnd l u) _) tail =>
V.Algos.bisect_1d (fun b => V.eval_diff prec formula (map V.interval_from_bp tail) n b) l u output depth = true
| _ => False
end ->
......@@ -493,7 +493,7 @@ Ltac do_interval_intro_eval extend bounds formula prec depth :=
Ltac do_interval_intro_bisect extend bounds formula prec depth :=
eval vm_compute in
(match bounds with
| cons (V.Bproof _ (interval_float.Ibnd l u) _) tail =>
| cons (V.Bproof _ (Interval_interval_float.Ibnd l u) _) tail =>
V.Algos.lookup_1d (fun b => nth 0 (V.eval_bnd prec formula (b :: map V.interval_from_bp tail)) I.nai) l u extend depth
| _ => I.nai
end).
......@@ -501,7 +501,7 @@ Ltac do_interval_intro_bisect extend bounds formula prec depth :=
Ltac do_interval_intro_bisect_diff extend bounds formula prec depth :=
eval vm_compute in
(match bounds with
| cons (V.Bproof _ (interval_float.Ibnd l u) _) tail =>
| cons (V.Bproof _ (Interval_interval_float.Ibnd l u) _) tail =>
V.Algos.lookup_1d (fun b => V.eval_diff prec formula (map V.interval_from_bp tail) 0 b) l u extend depth
| _ => I.nai
end).
......
Require Import Reals.
Require Import missing.
Require Import xreal.
Require Import definitions.
Require Import float_sig.
Require Import generic.
Require Import generic_proof.
Require Import interval.
Require Import interval_float.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_definitions.
Require Import Interval_float_sig.
Require Import Interval_generic.
Require Import Interval_generic_proof.
Require Import Interval_interval.
Require Import Interval_interval_float.
Module TranscendentalFloatFast (F : FloatOps with Definition even_radix := true).
......@@ -863,9 +863,9 @@ Definition tan_fast prec x :=
end.
Definition semi_extension f fi :=
forall x, interval.contains (I.convert (fi x)) (f (FtoX (F.toF x))).
forall x, contains (I.convert (fi x)) (f (FtoX (F.toF x))).
Axiom pi4_correct : forall prec, interval.contains (I.convert (pi4 prec)) (Xreal (PI/4)).
Axiom pi4_correct : forall prec, contains (I.convert (pi4 prec)) (Xreal (PI/4)).
Definition cos_correct : forall prec, semi_extension Xcos (cos_fast prec) := cos_fast_correct.
Definition sin_correct : forall prec, semi_extension Xsin (sin_fast prec) := sin_fast_correct.
Axiom tan_correct : forall prec, semi_extension Xtan (tan_fast prec).
......@@ -1099,8 +1099,8 @@ Qed.
End TranscendentalFloatFast.
(*
Require Import specific_ops.
Require Import stdz_carrier.
Require Import Interval_specific_ops.
Require Import Interval_stdz_carrier.
Module F := SpecificFloat StdZRadix2.
Module A := TranscendentalFloatFast F.
Time Eval vm_compute in (A.exp_fast 50%Z (Float 201%Z (-8)%Z)).
......
Require Import Reals.
Require Import Bool.
Require Import missing.
Require Import Interval_missing.
(*
* Rcompare
......