Commit afd74a8d authored by BOLDO Sylvie's avatar BOLDO Sylvie
parents b53d2295 8e2f24a0
......@@ -5,10 +5,11 @@ config.log
config.status
configure
install-sh
Makefile.in
Makefile
missing
Remakefile
.remake
remake
remake.exe
html
src/Flocq_version.v
*.vo
*.vd
*.glob
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.2) with a Reals theory
You will need the Coq proof assistant (>= 8.3) with a Reals theory
compiled in.
The .tar.gz file is distributed with a working set of configure files.
They are not in the SVN repository though. Consequently, if you are
building from SVN, you will need autoconf (>= 2.59) and automake (>= 1.8).
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).
Configuring, compiling and installing
......@@ -14,14 +14,15 @@ Configuring, compiling and installing
Ideally, you should just have to type:
$ ./configure && make && make install
$ ./configure && ./remake && ./remake install
The environment variable "COQC" can be set to the Coq compiler command.
The configure script defaults to "coqc".
The environment variable COQC can be passed to the configure script in order
to set the Coq compiler command. The configure script defaults to "coqc".
Similarly, COQDEP can be used to specify the location of "coqdep". The
COQBIN environment variable can be used to set both variables at once.
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/Flocq".
The files are compiled at a logical location starting with "Flocq". This
default prefix can be removed with the "--disable-prefix" option.
The files are compiled at a logical location starting with "Flocq".
SUBDIRS = src
EXTRA_DIST = autogen.sh
......@@ -28,45 +28,53 @@ FILES = \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v
EXTRA_DIST = $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob)
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
datadir = $(libdir)
all: $(OBJS)
all: $(FILES:=o)
Remakefile: Remakefile.in config.status
./config.status Remakefile
.v.vo:
@echo COQC $<
@$(COQC) $(COQRFLAG) -dont-load-proofs $<
configure config.status: configure.in
autoconf
./config.status --recheck
.v.vd:
@echo COQDEP $<
@$(COQDEP) -I Core -I Calc -I Prop -I Appli $< > $@
%.vo: %.v
@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
@COQC@ -R src Flocq -dont-load-proofs $<
SUFFIXES = .v .vo .vd
clean:
rm -f $(OBJS) src/*.glob
install-data-local:
@$(NORMAL_INSTALL)
@test -z "$(datadir)" || \
for p in Core Calc Prop Appli; do \
$(MKDIR_P) "$(DESTDIR)$(datadir)/$$p"; \
done
@list='$(FILES:=o)'; test -n "$(datadir)" || list=; \
for p in $$list; do \
if test -f "$$p"; then d=; else d="$(srcdir)/"; fi; \
echo "$$d$$p" "$(DESTDIR)$(datadir)/$$p"; \
done | \
while read src dst; do \
echo " $(INSTALL_DATA) $$src $$dst"; \
$(INSTALL_DATA) "$$src" "$$dst" || exit $$?; \
done
html/index.html: $(OBJS)
rm -rf html
mkdir -p html
@COQDOC@ -toc -interpolate -utf8 -html -g -R src Flocq -d html \
--coqlib http://coq.inria.fr/distrib/current/stdlib/ \
$(addprefix src/,$(FILES))
uninstall-local:
@$(NORMAL_UNINSTALL)
test -z "$(datadir)" || rm -rf "$(DESTDIR)$(datadir)/$$p"
doc: html/index.html
html: $(FILES:=o)
@mkdir -p ../html
$(COQDOC) -toc -g -R . Flocq -d ../html -t 'Flocq' --coqlib 'http://coq.inria.fr/library/' $(FILES)
install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop Appli; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
-include $(FILES:=d)
EXTRA_DIST = \
configure
dist: $(EXTRA_DIST)
PACK=@PACKAGE_TARNAME@-@PACKAGE_VERSION@
DIRS=`git ls-tree -d -r --name-only HEAD`
FILES=`git ls-tree -r --name-only HEAD`
rm -rf $PACK.tar.gz $PACK
mkdir $PACK
for d in $DIRS; do mkdir $PACK/$d; done
for f in $FILES $(EXTRA_DIST); do cp $f $PACK/$f; done
git log --pretty="format:%ad %s" --date=short > $PACK/ChangeLog
cat /dev/null > $PACK/ChangeLog
rm `find $PACK -name .gitignore`
tar czf $PACK.tar.gz $PACK
rm -rf $PACK
AC_INIT([Flocq], [2.1.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
AM_INIT_AUTOMAKE
m4_divert_push(99)
if test "$ac_init_help" = "long"; then
......@@ -14,22 +13,43 @@ Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Flocq@:>@])
m4_divert_pop([HELP_ENABLE])
AC_PROG_CXX
AC_ARG_VAR(COQBIN, [path to Coq executables [empty]])
if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
AC_CHECK_TOOL(COQC, coqc)
AC_MSG_CHECKING([for coqc])
if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
AC_MSG_RESULT([$COQC])
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_CHECK_TOOL(COQDEP, coqdep)
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then COQDEP=`which ${COQBIN}coqdep`; fi
AC_MSG_RESULT([$COQDEP])
AC_ARG_VAR(COQDOC, [Coq documentation tool [coqdoc]])
AC_CHECK_TOOL(COQDOC, coqdoc)
AC_ARG_VAR(COQDOC, [Coq documentation generator command [coqdoc]])
AC_MSG_CHECKING([for coqdoc])
if test ! "$COQDOC"; then COQDOC=`which ${COQBIN}coqdoc`; fi
AC_MSG_RESULT([$COQDOC])
if test "$libdir" = '${exec_prefix}/lib'; then
libdir='`$(COQC) -where`/user-contrib/Flocq'
libdir="`$COQC -where`/user-contrib/Flocq"
fi
AC_SUBST(COQRFLAG, ['-R . Flocq'])
AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into a Flocq module]),
[if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
AC_CONFIG_FILES([Makefile src/Makefile src/Flocq_version.v])
AC_MSG_NOTICE([building remake...])
case `uname -s` in
MINGW*)
$CXX -Wall -O2 -o remake.exe remake.cpp -lws2_32
if test $? != 0; then AC_MSG_FAILURE([failed]); fi
AC_SUBST([REMAKE], [./remake.exe])
;;
*)
$CXX -Wall -O2 -o remake remake.cpp
if test $? != 0; then AC_MSG_FAILURE([failed]); fi
AC_SUBST([REMAKE], [./remake])
;;
esac
AC_CONFIG_FILES([Remakefile src/Flocq_version.v])
AC_OUTPUT
This diff is collapsed.
......@@ -33,7 +33,7 @@ Section AnyRadix.
Inductive full_float :=
| F754_zero : bool -> full_float
| F754_infinity : bool -> full_float
| F754_nan : full_float
| F754_nan : bool -> positive -> full_float
| F754_finite : bool -> positive -> Z -> full_float.
Definition FF2R beta x :=
......@@ -67,16 +67,20 @@ Definition bounded m e :=
Definition valid_binary x :=
match x with
| F754_finite _ m e => bounded m e
| F754_nan _ pl => (Z_of_nat' (S (digits2_Pnat pl)) <? prec)%Z
| _ => true
end.
(** Basic type used for representing binary FP numbers.
Note that there is exactly one such object per FP datum.
NaNs do not have any payload. They cannot be distinguished. *)
Definition nan_pl := {pl | (Z_of_nat' (S (digits2_Pnat pl)) <? prec)%Z = true}.
Inductive binary_float :=
| B754_zero : bool -> binary_float
| B754_infinity : bool -> binary_float
| B754_nan : binary_float
| B754_nan : bool -> nan_pl -> binary_float
| B754_finite : bool ->
forall (m : positive) (e : Z), bounded m e = true -> binary_float.
......@@ -85,7 +89,7 @@ Definition FF2B x :=
| F754_finite s m e => B754_finite s m e
| F754_infinity s => fun _ => B754_infinity s
| F754_zero s => fun _ => B754_zero s
| F754_nan => fun _ => B754_nan
| F754_nan b pl => fun H => B754_nan b (exist _ pl H)
end.
Definition B2FF x :=
......@@ -93,7 +97,7 @@ Definition B2FF x :=
| B754_finite s m e _ => F754_finite s m e
| B754_infinity s => F754_infinity s
| B754_zero s => F754_zero s
| B754_nan => F754_nan
| B754_nan b (exist pl _) => F754_nan b pl
end.
Definition radix2 := Build_radix 2 (refl_equal true).
......@@ -108,30 +112,30 @@ Theorem FF2R_B2FF :
forall x,
FF2R radix2 (B2FF x) = B2R x.
Proof.
now intros [sx|sx| |sx mx ex Hx].
now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx].
Qed.
Theorem B2FF_FF2B :
forall x Hx,
B2FF (FF2B x Hx) = x.
Proof.
now intros [sx|sx| |sx mx ex] Hx.
now intros [sx|sx|sx plx|sx mx ex] Hx.
Qed.
Theorem valid_binary_B2FF :
forall x,
valid_binary (B2FF x) = true.
Proof.
now intros [sx|sx| |sx mx ex Hx].
now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx].
Qed.
Theorem FF2B_B2FF :
forall x H,
FF2B (B2FF x) H = x.
Proof.
intros [sx|sx| |sx mx ex Hx] H ; try easy.
apply f_equal.
apply eqbool_irrelevance.
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] H ; try easy.
simpl. apply f_equal, f_equal, eqbool_irrelevance.
apply f_equal, eqbool_irrelevance.
Qed.
Theorem FF2B_B2FF_valid :
......@@ -146,7 +150,7 @@ Theorem B2R_FF2B :
forall x Hx,
B2R (FF2B x Hx) = FF2R radix2 x.
Proof.
now intros [sx|sx| |sx mx ex] Hx.
now intros [sx|sx|sx plx|sx mx ex] Hx.
Qed.
Theorem match_FF2B :
......@@ -154,17 +158,17 @@ Theorem match_FF2B :
match FF2B x Hx return T with
| B754_zero sx => fz sx
| B754_infinity sx => fi sx
| B754_nan => fn
| B754_nan b (exist p _) => fn b p
| B754_finite sx mx ex _ => ff sx mx ex
end =
match x with
| F754_zero sx => fz sx
| F754_infinity sx => fi sx
| F754_nan => fn
| F754_nan b p => fn b p
| F754_finite sx mx ex => ff sx mx ex
end.
Proof.
now intros T fz fi fn ff [sx|sx| |sx mx ex] Hx.
now intros T fz fi fn ff [sx|sx|sx plx|sx mx ex] Hx.
Qed.
Theorem canonic_canonic_mantissa :
......@@ -189,7 +193,7 @@ Theorem generic_format_B2R :
forall x,
generic_format radix2 fexp (B2R x).
Proof.
intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0.
intros [sx|sx|sx plx|sx mx ex Hx] ; try apply generic_format_0.
simpl.
apply generic_format_canonic.
apply canonic_canonic_mantissa.
......@@ -210,7 +214,7 @@ Theorem B2FF_inj :
B2FF x = B2FF y ->
x = y.
Proof.
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] [sy|sy|sy [ply Hply]|sy my ey Hy] ; try easy.
(* *)
intros H.
now inversion H.
......@@ -221,11 +225,18 @@ now inversion H.
intros H.
inversion H.
clear H.
revert Hplx.
rewrite H2.
intros Hx.
apply f_equal, f_equal, eqbool_irrelevance.
(* *)
intros H.
inversion H.
clear H.
revert Hx.
rewrite H2, H3.
intros Hx.
apply f_equal.
apply eqbool_irrelevance.
apply f_equal, eqbool_irrelevance.
Qed.
Definition is_finite_strict f :=
......@@ -299,37 +310,71 @@ Theorem is_finite_FF_B2FF :
forall x,
is_finite_FF (B2FF x) = is_finite x.
Proof.
now intros [| |? []|].
Qed.
Definition is_nan f :=
match f with
| B754_nan _ _ => true
| _ => false
end.
Definition is_nan_FF f :=
match f with
| F754_nan _ _ => true
| _ => false
end.
Theorem is_nan_FF2B :
forall x Hx,
is_nan (FF2B x Hx) = is_nan_FF x.
Proof.
now intros [| | |].
Qed.
Definition Bopp x :=
Theorem is_nan_FF_B2FF :
forall x,
is_nan_FF (B2FF x) = is_nan x.
Proof.
now intros [| |? []|].
Qed.
Definition Bopp opp_nan x :=
match x with
| B754_nan => x
| B754_nan sx plx =>
let '(sres, plres) := opp_nan sx plx in B754_nan sres plres
| B754_infinity sx => B754_infinity (negb sx)
| B754_finite sx mx ex Hx => B754_finite (negb sx) mx ex Hx
| B754_zero sx => B754_zero (negb sx)
end.
Theorem Bopp_involutive :
forall x, Bopp (Bopp x) = x.
forall opp_nan x,
is_nan x = false ->
Bopp opp_nan (Bopp opp_nan x) = x.
Proof.
now intros [sx|sx| |sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive.
now intros opp_nan [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive.
Qed.
Theorem B2R_Bopp :
forall x,
B2R (Bopp x) = (- B2R x)%R.
forall opp_nan x,
B2R (Bopp opp_nan x) = (- B2R x)%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; apply sym_eq ; try apply Ropp_0.
intros opp_nan [sx|sx|sx plx|sx mx ex Hx]; apply sym_eq ; try apply Ropp_0.
simpl. destruct opp_nan. apply Ropp_0.
simpl.
rewrite <- F2R_opp.
now case sx.
Qed.
Theorem is_finite_Bopp: forall x,
is_finite (Bopp x) = is_finite x.
Theorem is_finite_Bopp :
forall opp_nan x,
is_finite (Bopp opp_nan x) = is_finite x.
Proof.
now intros [| | |].
intros opp_nan [| | |] ; try easy.
intros s pl.
simpl.
now case opp_nan.
Qed.
Theorem bounded_lt_emax :
......@@ -367,7 +412,7 @@ Theorem abs_B2R_lt_emax :
forall x,
(Rabs (B2R x) < bpow radix2 emax)%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
intros [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
rewrite <- F2R_Zabs, abs_cond_Zopp.
now apply bounded_lt_emax.
Qed.
......@@ -644,7 +689,7 @@ Definition binary_round_aux mode sx mx ex lx :=
match shr_m mrs'' with
| Z0 => F754_zero sx
| Zpos m => if Zle_bool e'' (emax - prec) then F754_finite sx m e'' else binary_overflow mode sx
| _ => F754_nan (* dummy *)
| _ => F754_nan false xH (* dummy *)
end.
Theorem binary_round_aux_correct :
......@@ -826,7 +871,7 @@ Qed.
Definition Bsign x :=
match x with
| B754_nan => false
| B754_nan s _ => s
| B754_zero s => s
| B754_infinity s => s
| B754_finite s _ _ _ => s
......@@ -834,7 +879,7 @@ Definition Bsign x :=
Definition sign_FF x :=
match x with
| F754_nan => false
| F754_nan s _ => s
| F754_zero s => s
| F754_infinity s => s
| F754_finite s _ _ => s
......@@ -844,7 +889,7 @@ Theorem Bsign_FF2B :
forall x H,
Bsign (FF2B x H) = sign_FF x.
Proof.
now intros [sx|sx| |sx mx ex] H.
now intros [sx|sx|sx plx|sx mx ex] H.
Qed.
(** Multiplication *)
......@@ -902,15 +947,15 @@ apply Rlt_bool_false.
now apply F2R_ge_0_compat.
Qed.
Definition Bmult m x y :=
Definition Bmult mult_nan m x y :=
let f pl := B754_nan (fst pl) (snd pl) in
match x, y with
| B754_nan, _ => x
| _, B754_nan => y
| B754_nan _ _, _ | _, B754_nan _ _ => f (mult_nan x y)
| B754_infinity sx, B754_infinity sy => B754_infinity (xorb sx sy)
| B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy)
| B754_finite sx _ _ _, B754_infinity sy => B754_infinity (xorb sx sy)
| B754_infinity _, B754_zero _ => B754_nan
| B754_zero _, B754_infinity _ => B754_nan
| B754_infinity _, B754_zero _ => f (mult_nan x y)
| B754_zero _, B754_infinity _ => f (mult_nan x y)
| B754_finite sx _ _ _, B754_zero sy => B754_zero (xorb sx sy)
| B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy)
| B754_zero sx, B754_zero sy => B754_zero (xorb sx sy)
......@@ -919,14 +964,14 @@ Definition Bmult m x y :=
end.
Theorem Bmult_correct :
forall m x y,
forall mult_nan m x y,
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 emax) then
B2R (Bmult m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\
is_finite (Bmult m x y) = andb (is_finite x) (is_finite y)
B2R (Bmult mult_nan m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\
is_finite (Bmult mult_nan m x y) = andb (is_finite x) (is_finite y)
else
B2FF (Bmult m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
B2FF (Bmult mult_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ;
intros mult_nan m [sx|sx|sx plx|sx mx ex Hx] [sy|sy|sy ply|sy my ey Hy] ;
try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ split ; apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ).
simpl.
case Bmult_correct_aux.
......@@ -940,15 +985,15 @@ intros H2.
now rewrite B2FF_FF2B.
Qed.
Definition Bmult_FF m x y :=
Definition Bmult_FF mult_nan m x y :=
let f pl := F754_nan (fst pl) (snd pl) in
match x, y with
| F754_nan, _ => x
| _, F754_nan => y
| F754_nan _ _, _ | _, F754_nan _ _ => f (mult_nan x y)
| F754_infinity sx, F754_infinity sy => F754_infinity (xorb sx sy)
| F754_infinity sx, F754_finite sy _ _ => F754_infinity (xorb sx sy)
| F754_finite sx _ _, F754_infinity sy => F754_infinity (xorb sx sy)
| F754_infinity _, F754_zero _ => F754_nan
| F754_zero _, F754_infinity _ => F754_nan
| F754_infinity _, F754_zero _ => f (mult_nan x y)
| F754_zero _, F754_infinity _ => f (mult_nan x y)
| F754_finite sx _ _, F754_zero sy => F754_zero (xorb sx sy)
| F754_zero sx, F754_finite sy _ _ => F754_zero (xorb sx sy)
| F754_zero sx, F754_zero sy => F754_zero (xorb sx sy)
......@@ -957,14 +1002,20 @@ Definition Bmult_FF m x y :=
end.
Theorem B2FF_Bmult :
forall mult_nan mult_nan_ff,
forall m x y,
B2FF (Bmult m x y) = Bmult_FF m (B2FF x) (B2FF y).
mult_nan_ff (B2FF x) (B2FF y) = (let '(sr, exist plr _) := mult_nan x y in (sr, plr)) ->
B2FF (Bmult mult_nan m x y) = Bmult_FF mult_nan_ff m (B2FF x) (B2FF y).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
intros mult_nan mult_nan_ff m x y Hmult_nan.
unfold Bmult_FF. rewrite Hmult_nan.
destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Hx], y as [sy|sy|sy [ply Hply]|sy my ey Hy] ;
simpl; try match goal with |- context [mult_nan ?x ?y] =>
destruct (mult_nan x y) as [? []] end;
try easy.
apply B2FF_FF2B.
Qed.
Definition shl_align mx ex ex' :=
match (ex' - ex)%Z with
| Zneg d => (shift_pos d mx, ex')
......@@ -1129,12 +1180,12 @@ now apply F2R_lt_0_compat.
Qed.
(** Addition *)
Definition Bplus m x y :=
Definition Bplus plus_nan m x y :=
let f pl := B754_nan (fst pl) (snd pl) in
match x, y with
| B754_nan, _ => x
| _, B754_nan => y
| B754_nan _ _, _ | _, B754_nan _ _ => f (plus_nan x y)
| B754_infinity sx, B754_infinity sy =>
if Bool.eqb sx sy then x else B754_nan
if Bool.eqb sx sy then x else f (plus_nan x y)
| B754_infinity _, _ => x
| _, B754_infinity _ => y
| B754_zero sx, B754_zero sy =>
......@@ -1149,16 +1200,16 @@ Definition Bplus m x y :=
end.
Theorem Bplus_correct :
forall m x y,
forall plus_nan m x y,
is_finite x = true ->
is_finite y = true ->
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x + B2R y))) (bpow radix2 emax) then
B2R (Bplus m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\
is_finite (Bplus m x y) = true
B2R (Bplus plus_nan m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\
is_finite (Bplus plus_nan m x y) = true
else
(B2FF (Bplus m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
(B2FF (Bplus plus_nan m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
Proof with auto with typeclass_instances.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy.
intros plus_nan m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy.
(* *)
rewrite Rplus_0_r, round_0, Rabs_R0, Rlt_bool_true...
simpl.
......@@ -1279,26 +1330,25 @@ now apply f_equal.
apply Sz.
Qed.
Definition Bminus m x y := Bplus m x (Bopp y).
Definition Bminus minus_nan m x y := Bplus minus_nan m x (Bopp pair y).
Theorem Bminus_correct :
forall m x y,
forall minus_nan<