Commit f5fd1738 authored by François Bobot's avatar François Bobot
Browse files

Add factorization for ADT as congruence closure

parent 1ab6cf58
......@@ -2,5 +2,5 @@
(prelude extraction)
(extracted_modules BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version
Defs Operations)
Defs Operations Op)
(theories Farith2))
......@@ -7,6 +7,10 @@ module Pos =
let rec add_carry = fun p q -> Farith_Big.succ (Farith_Big.add p q)
(** val pred : Farith_Big.big_int -> Farith_Big.big_int **)
let pred = fun n -> Farith_Big.max Farith_Big.one (Farith_Big.pred n)
type mask = Pos.mask =
| IsNul
| IsPos of Farith_Big.big_int
......@@ -79,6 +83,11 @@ module Pos =
(fun _ -> IsNeg)
x
(** val sub :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let sub = fun n m -> Farith_Big.max Farith_Big.one (Farith_Big.sub n m)
(** val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1 **)
let rec iter f x n =
......
......@@ -5,6 +5,8 @@ module Pos :
val add_carry :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
val pred : Farith_Big.big_int -> Farith_Big.big_int
type mask = Pos.mask =
| IsNul
| IsPos of Farith_Big.big_int
......@@ -20,6 +22,8 @@ module Pos :
val sub_mask_carry : Farith_Big.big_int -> Farith_Big.big_int -> mask
val sub : Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1
val div2 : Farith_Big.big_int -> Farith_Big.big_int
......
open BinInt
open BinPos
open Bool
open Datatypes
open Defs
......@@ -6,6 +7,7 @@ open Operations
open Round
open SpecFloat
open Zaux
open Zpower
type binary_float =
| B754_zero of bool
......@@ -47,6 +49,15 @@ let is_nan _ _ = function
| B754_nan -> true
| _ -> false
(** val coq_Bopp :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float **)
let coq_Bopp _ _ x = match x with
| B754_zero sx -> B754_zero (Pervasives.not sx)
| B754_infinity sx -> B754_infinity (Pervasives.not sx)
| B754_nan -> x
| B754_finite (sx, mx, ex) -> B754_finite ((Pervasives.not sx), mx, ex)
(** val coq_Babs :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float **)
......@@ -392,3 +403,11 @@ let coq_Bsqrt prec emax m x = match x with
else coq_SF2B prec emax
(let (p, lz) = coq_SFsqrt_core_binary prec emax mx ex in
let (mz, ez) = p in binary_round_aux prec emax m false mz ez lz)
(** val coq_Bmax_float :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float **)
let coq_Bmax_float prec emax =
coq_SF2B prec emax (S754_finite (false,
(Pos.sub (shift_pos (Z.to_pos prec) Farith_Big.one) Farith_Big.one),
(Farith_Big.sub emax prec)))
open BinInt
open BinPos
open Bool
open Datatypes
open Defs
......@@ -6,6 +7,7 @@ open Operations
open Round
open SpecFloat
open Zaux
open Zpower
type binary_float =
| B754_zero of bool
......@@ -24,6 +26,9 @@ val coq_Bsign :
val is_nan : Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool
val coq_Bopp :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
val coq_Babs :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
......@@ -101,3 +106,5 @@ val coq_Bdiv :
val coq_Bsqrt :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float
val coq_Bmax_float : Farith_Big.big_int -> Farith_Big.big_int -> binary_float
......@@ -4,6 +4,7 @@ open BinarySingleNaN
open Bits
open Datatypes
open Interval
open Op
open Qextended
open SpecFloat
......@@ -200,15 +201,20 @@ module GenericFloat =
let abs x =
mk_with x (coq_Babs (cprec x.mw) (cemax x.ew) x.value)
(** val succ : t -> t **)
let succ x =
mk_with x (coq_Fsucc (cprec x.mw) (cemax x.ew) x.value)
(** val pred : t -> t **)
let pred x =
mk_with x (coq_Fpred (cprec x.mw) (cemax x.ew) x.value)
(** val neg : t -> t **)
let neg x =
mk_with x
(match x.value with
| B754_zero s -> B754_zero (Pervasives.not s)
| B754_infinity s -> B754_infinity (Pervasives.not s)
| B754_nan -> B754_nan
| B754_finite (s, m, e) -> B754_finite ((Pervasives.not s), m, e))
mk_with x (coq_Fneg (cprec x.mw) (cemax x.ew) x.value)
(** val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int **)
......
......@@ -4,6 +4,7 @@ open BinarySingleNaN
open Bits
open Datatypes
open Interval
open Op
open Qextended
open SpecFloat
......@@ -86,6 +87,10 @@ module GenericFloat :
val abs : t -> t
val succ : t -> t
val pred : t -> t
val neg : t -> t
val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int
......
open BinInt
open BinPos
open BinarySingleNaN
open SpecFloat
open Zpower
type float = binary_float
(** val coq_Fsucc :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float **)
let coq_Fsucc prec emax x = match x with
| B754_zero _ -> B754_finite (false, Farith_Big.one, (emin prec emax))
| B754_infinity s ->
if s then coq_Bopp prec emax (coq_Bmax_float prec emax) else x
| B754_nan -> x
| B754_finite (s, m, e) ->
if s
then if Farith_Big.identity (Farith_Big.eq e (emin prec emax))
then if Farith_Big.identity (Farith_Big.lt Farith_Big.one m)
then B754_finite (true, (Pos.pred m), e)
else B754_zero true
else let m0 = Farith_Big.pred m in
if Farith_Big.identity (Farith_Big.lt (coq_Zdigits2 m0) prec)
then B754_finite (true,
(Pos.sub (shift_pos (Z.to_pos prec) Farith_Big.one)
Farith_Big.one), (Farith_Big.sub e Farith_Big.one))
else B754_finite (true, (Z.to_pos m0), e)
else let m0 = Farith_Big.succ m in
if Farith_Big.identity (Farith_Big.lt prec (digits2_pos m0))
then if Farith_Big.identity
(Farith_Big.eq e (Farith_Big.sub emax prec))
then B754_infinity false
else B754_finite (false,
(Z.to_pos
(Farith_Big.shiftl Farith_Big.one
(Farith_Big.sub prec Farith_Big.one))),
(Farith_Big.add e Farith_Big.one))
else B754_finite (false, m0, e)
(** val coq_Fneg :
Farith_Big.big_int -> Farith_Big.big_int -> float -> float **)
let coq_Fneg _ _ = function
| B754_zero s -> B754_zero (Pervasives.not s)
| B754_infinity s -> B754_infinity (Pervasives.not s)
| B754_nan -> B754_nan
| B754_finite (s, m, e) -> B754_finite ((Pervasives.not s), m, e)
(** val coq_Fpred :
Farith_Big.big_int -> Farith_Big.big_int -> float -> float **)
let coq_Fpred prec emax x =
coq_Fneg prec emax (coq_Fsucc prec emax (coq_Fneg prec emax x))
open BinInt
open BinPos
open BinarySingleNaN
open SpecFloat
open Zpower
type float = binary_float
val coq_Fsucc :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
val coq_Fneg : Farith_Big.big_int -> Farith_Big.big_int -> float -> float
val coq_Fpred : Farith_Big.big_int -> Farith_Big.big_int -> float -> float
type 'a coq_sig = 'a
(* singleton inductive, whose constructor was exist *)
type 'a coq_sig = 'a
(* singleton inductive, whose constructor was exist *)
......@@ -44,3 +44,5 @@
(rule (action (copy ../extract/Defs.mli Defs.mli)) (mode promote))
(rule (action (copy ../extract/Operations.ml Operations.ml)) (mode promote))
(rule (action (copy ../extract/Operations.mli Operations.mli)) (mode promote))
(rule (action (copy ../extract/Op.ml Op.ml)) (mode promote))
(rule (action (copy ../extract/Op.mli Op.mli)) (mode promote))
......@@ -47,9 +47,7 @@ module F = struct
include GenericFloat
let mw t = Z.to_int t.mw
let ew t = Z.to_int t.ew
let pp_sign fmt b = Format.pp_print_string fmt (if b then "-" else "+")
type binary_float = BinarySingleNaN.binary_float =
......@@ -83,26 +81,18 @@ module F = struct
match String.index s 'p' with
| Some k ->
let m = String.sub s ~pos:0 ~len:k in
let e = String.sub s (succ k) (String.length s - k - 1) in
let e = String.sub s (Int.succ k) (String.length s - k - 1) in
(Z.of_string m, Z.of_string e)
| None -> (Z.of_string s, Z.zero)
let of_q ~mw ~ew ~mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
let of_bits ~mw ~ew z = of_bits (Z.of_int mw) (Z.of_int ew) z
let to_bits t = to_bits t
let nan ~mw ~ew = nan (Z.of_int mw) (Z.of_int ew)
let zero ~mw ~ew b = zero (Z.of_int mw) (Z.of_int ew) b
let inf ~mw ~ew b = inf (Z.of_int mw) (Z.of_int ew) b
let is_zero t = match t.value with B754_zero _ -> true | _ -> false
let is_infinite t = match t.value with B754_infinity _ -> true | _ -> false
let is_nan t = match t.value with B754_nan -> true | _ -> false
let is_negative t =
......@@ -139,7 +129,6 @@ module I = struct
type t = interval generic [@@deriving eq, ord, hash]
let mw t = Z.to_int t.mw
let ew t = Z.to_int t.ew
let pp fmt (t : t) =
......
......@@ -66,6 +66,10 @@ module F : sig
val neg : t -> t
val pred : t -> t
val succ : t -> t
val of_bits : mw:int -> ew:int -> Z.t -> t
val to_bits : t -> Z.t
......
......@@ -142,6 +142,12 @@ Proof.
now destruct H as [<- [Hf _]], (Bplus _ _ _).
Qed.
Lemma Bmult_correct :
forall (m : mode) (x y : float),
is_nan (Bmult m x y) = false ->
B2Rx (Bmult m x y) = round m (mult (B2Rx x) (B2Rx y)).
Admitted.
Theorem Bplus_le_mono_l:
forall m (a b c : float),
is_nan (Bplus m a c) = false ->
......
From Flocq Require Import Core.Core IEEE754.BinarySingleNaN IEEE754.Bits.
From Coq Require Import Program ZArith Bool Lia Reals Qreals ZBits.
Require Import Assert Utils Interval Qextended Rextended.
Require Import Assert Utils Interval Qextended Rextended Op.
Definition cprec mw := (Z.succ mw)%Z.
......@@ -203,13 +203,14 @@ Module GenericFloat.
Definition abs (x : t) : t :=
mk_with x (@Babs _ _ (value x)).
Definition succ (x : t) : t :=
mk_with x (@Op.Fsucc _ _ (Hprec x) (Hemax x) (value x)).
Definition pred (x : t) : t :=
mk_with x (@Op.Fpred _ _ (Hprec x) (Hemax x) (value x)).
Definition neg (x : t) : t :=
mk_with x (match value x with
| B754_nan => B754_nan
| B754_zero s => B754_zero (negb s)
| B754_infinity s => B754_infinity (negb s)
| B754_finite s m e H => B754_finite (negb s) m e H
end).
mk_with x (@Op.Fneg _ _ (value x)).
Fixpoint least_bit_Pnat (n : positive) :=
match n with
......
......@@ -484,4 +484,29 @@ Proof.
* apply (Bleb_trans y x h1 (Beqb_Bleb _ _ _ _ (Beqb_symm _ _ _ _ Hxy)) Hx').
Qed.
Definition Iopp' (I1 : Interval') : Interval' :=
match I1 with
| Inan => Inan
| Intv l h n =>
let opp1 := Bopp l in
let opp2 := Bopp h in
Intv opp2 opp1 n
end.
Program Definition Iopp (I1 : Interval) : Interval :=
Iopp' I1.
Admit Obligations.
Program Definition union' (I1 I2 : Interval') : Interval' :=
match I1, I2 with
| Inan, Inan => Inan
| Inan, Intv _ _ true => I2
| Inan, Intv l h false => Intv l h true
| Intv _ _ true, Inan => I1
| Intv l h false, Inan => Intv l h true
| Intv lo1 hi1 nan1, Intv lo2 hi2 nan2 =>
(Intv (Bmin lo1 lo2) (Bmax hi1 hi2) (nan1 || nan2))
end.
End Finterval.
From Flocq Require Import Core.Core IEEE754.BinarySingleNaN IEEE754.Bits.
From Coq Require Import Program ZArith Bool Lia Reals Qreals ZBits SpecFloat.
Require Import Assert Utils Interval Qextended Rextended.
Section Op.
Variable prec : Z.
Variable emax : Z.
Context (Hprec : FLX.Prec_gt_0 prec).
Context (Hemax : Prec_lt_emax prec emax).
Definition float := binary_float prec emax.
Lemma split_bounded_emin:
forall m e, bounded prec emax m e = true <->
( e = emin prec emax /\ (Z.pos (digits2_pos m) <= prec)%Z )
\/ ( (emin prec emax < e)%Z /\ (e <= emax-prec)%Z /\ (Z.pos (digits2_pos m) = prec)%Z ).
Proof.
intros m e; split.
- intros H.
unfold bounded in H.
unfold canonical_mantissa in H.
unfold SpecFloat.fexp in H.
destruct (Z_ge_lt_dec (emin prec emax) (Z.pos (digits2_pos m) + e - prec)).
* left.
rewrite Z.max_r in H.
apply andb_prop in H.
rewrite <- Zeq_is_eq_bool in H.
rewrite <- Zle_is_le_bool in H.
split; lia.
lia.
* right.
rewrite Z.max_l in H.
apply andb_prop in H.
rewrite <- Zeq_is_eq_bool in H.
rewrite <- Zle_is_le_bool in H.
split; [lia | split ; lia ].
lia.
- intro H.
destruct H as [[H1 H2]|[H1 [H2 H3]]]; unfold bounded; unfold canonical_mantissa; unfold SpecFloat.fexp; apply andb_true_intro.
+ split.
* rewrite Z.max_r.
rewrite <- Zeq_is_eq_bool.
lia.
lia.
* rewrite <- Zle_is_le_bool.
unfold emin in H1.
unfold Prec_gt_0 in Hprec.
unfold Prec_lt_emax in Hemax.
lia.
+ split.
* rewrite Z.max_l.
rewrite <- Zeq_is_eq_bool.
lia.
lia.
* rewrite <- Zle_is_le_bool.
unfold emin in H1.
unfold Prec_gt_0 in Hprec.
unfold Prec_lt_emax in Hemax.
lia.
Qed.
Lemma max_mantissa_has_length_prec:
Z.pos (digits2_pos (shift_pos (Z.to_pos prec) 1 - 1)) = prec.
Proof.
rewrite Zpos_digits2_pos, Pos2Z.inj_sub.
- rewrite shift_pos_correct, Z.mul_1_r.
assert (P2pm1 : (0 <= 2 ^ prec - 1)%Z).
{ apply (Zplus_le_reg_r _ _ 1); ring_simplify.
change 1%Z with (2 ^ 0)%Z; change 2%Z with (radix2 : Z).
apply Zpower_le; unfold Prec_gt_0 in Hprec; lia. }
apply Zdigits_unique;
rewrite Z.pow_pos_fold, Z2Pos.id; [|exact Hprec]; simpl; split.
+ rewrite (Z.abs_eq _ P2pm1).
replace prec with (prec - 1 + 1)%Z at 2 by ring.
rewrite Zpower_plus; [| unfold Prec_gt_0 in Hprec; lia|lia].
simpl; unfold Z.pow_pos; simpl.
assert (1 <= 2 ^ (prec - 1))%Z; [|lia].
change 1%Z with (2 ^ 0)%Z; change 2%Z with (radix2 : Z).
apply Zpower_le; simpl; unfold Prec_gt_0 in Hprec; lia.
+ now rewrite Z.abs_eq; [lia|].
- change (_ < _)%positive
with (Z.pos 1 < Z.pos (shift_pos (Z.to_pos prec) 1))%Z.
rewrite shift_pos_correct, Z.mul_1_r, Z.pow_pos_fold.
rewrite Z2Pos.id; [|exact Hprec].
change 1%Z with (2 ^ 0)%Z; change 2%Z with (radix2 : Z).
apply Zpower_lt; unfold Prec_gt_0 in Hprec; lia.
Qed.
Lemma min_normal_mantissa_has_length_prec:
Z.pos (digits2_pos (Z.to_pos (Z.shiftl 1 (prec - 1)%Z)))%positive = prec.
Proof.
unfold Prec_gt_0 in Hprec.
rewrite Zpos_digits2_pos.
rewrite Z.shiftl_mul_pow2.
rewrite Z2Pos.id.
rewrite Z.mul_1_l.
rewrite Zdigits_Zpower.
- lia.
- lia.
- assert (H2 : (0 < 2)%Z) by lia.
assert (H3 : (0 <= (prec - 1))%Z) by lia.
assert (H := (Z.pow_pos_nonneg 2 (prec - 1) H2 H3)%Z).
lia.
- lia.
Qed.
Lemma max_prec_is_canonical:
forall e, ((SpecFloat.emin prec emax) <= e)%Z -> (e <= emax - prec)%Z ->
canonical_mantissa prec emax (shift_pos (Z.to_pos prec) 1 - 1) e = true.
Proof.
intros e Hege Hele.
unfold canonical_mantissa; apply Zeq_bool_true.
assert (H := max_mantissa_has_length_prec).
set (p := Z.pos (digits2_pos _)) in *.
unfold SpecFloat.fexp, FLT_exp; rewrite H, Z.max_l; [ring|].
unfold emin in *.
(* generalize (prec_gt_0 prec) (prec_lt_emax prec emax). *)
lia.
Qed.
Lemma min_normal_prec_is_canonical:
forall e, ((SpecFloat.emin prec emax) <= e)%Z -> (e <= emax - prec)%Z ->
canonical_mantissa prec emax (Z.to_pos (Z.shiftl 1 (prec - 1)%Z))%positive e = true.
Proof.
intros e Hege Hele.
unfold canonical_mantissa; apply Zeq_bool_true.
assert (H := min_normal_mantissa_has_length_prec).
set (p := Z.pos (digits2_pos _)) in *.
unfold SpecFloat.fexp, FLT_exp; rewrite H, Z.max_l; [ring|].
unfold emin in *.
(* generalize (prec_gt_0 prec) (prec_lt_emax prec emax). *)
lia.
Qed.
Lemma Bmax_float_proof :
valid_binary prec emax
(S754_finite false (shift_pos (Z.to_pos prec) 1 - 1) (emax - prec))
= true.
Proof.
unfold valid_binary, bounded; apply andb_true_intro; split.
- apply max_prec_is_canonical.
+ unfold emin.
unfold Prec_gt_0 in Hprec.
unfold Prec_lt_emax in Hemax.
lia.
+ lia.
- apply Zle_bool_true; unfold emin; unfold Prec_gt_0 in Hprec; lia.
Qed.
Lemma bounded_is_bigger_than_emin:
forall m0 e, bounded prec emax m0 e = true -> (emin prec emax <= e)%Z.
Proof.
intros m0 e H.
apply andb_prop in H.
unfold canonical_mantissa in H.
unfold SpecFloat.fexp in H.
assert (Hmax := Z.le_max_r (Z.pos (digits2_pos m0) + e - prec) (emin prec emax)).
rewrite <- Zeq_is_eq_bool in H.
lia.
Qed.
Program Definition Fsucc x :=
match x with
| B754_zero _ => B754_finite false 1%positive (SpecFloat.emin prec emax) (Bulp_correct_aux _ _ Hprec Hemax)
| B754_infinity false => x
| B754_infinity true => Bopp Bmax_float
| B754_nan => x
| B754_finite false m e H =>
let m := (Pos.succ m) in
if dec (Z.ltb prec (Z.pos(SpecFloat.digits2_pos m)))%Z then
if dec (Z.eqb e (emax - prec))%Z then
B754_infinity false
else B754_finite false (Z.to_pos (Z.shiftl 1 (prec - 1)%Z)) (e+1)%Z _
else B754_finite false m e _
| B754_finite true m e H =>
if dec (e =? (SpecFloat.emin prec emax))%Z then
if dec (1 <? Z.pos m)%Z then
B754_finite true (Pos.pred m) e _
else
B754_zero true
else
let m0 := (Z.pred (Z.pos m))%Z in
if dec ((Zdigits2 m0) <? prec)%Z then
B754_finite true (shift_pos (Z.to_pos prec) 1 - 1) (e-1)%Z _
else
B754_finite true (Z.to_pos m0) e _
end.
Next Obligation.
apply andb_true_intro.
split.
- apply min_normal_prec_is_canonical.
+ apply bounded_is_bigger_than_emin in H.
lia.
+ apply andb_prop in H.
rewrite Z.leb_le in H.
lia.
- rewrite Z.leb_le in *.
rewrite Z.eqb_neq in H1.
apply andb_prop in H.
rewrite Z.leb_le in H.
lia.
Qed.
Next Obligation.
rewrite split_bounded_emin in *.
destruct H.
* left.
apply Z.ltb_nlt in H0.
split; lia.
* right.