Library Why2Gappa

Require Export Gappa_tactic.
Require Export Gappa_round.
Require Export Veltkamp.
Require Export WhyFloats.
Require Export WhyFloatsStrictLegacy.

Hint Resolve psGreaterThanOne psGivesBound pdGreaterThanOne pdGivesBound EvenClosestRoundedModeP
  RND_EvenClosest_correct RND_EvenClosest_canonic (FcanonicBound 2%Z).

Section Equiv.
Variable b : Fbound.
Variable p : nat.

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat 2%Z p.
Hypothesis precisionNotZero : 1 < p.

Lemma equiv_RNDs_aux1: forall f, Fbounded b f ->
  (generic_format radix2 (FLT_exp (-dExp b) p) (FtoRradix f)).

Lemma equiv_RNDs_aux2: forall r,
  (generic_format radix2 (FLT_exp (-dExp b) p) r)
  -> exists f, FtoRradix f = r /\ Fbounded b f.

Lemma equiv_RNDs_aux3: forall z, Zeven z = true -> Even z.

Lemma equiv_RNDs_aux4: forall f, Fcanonic 2 b f -> FtoRradix f <> 0 ->
  canonic radix2 (FLT_exp (- dExp b) p)
    (Float radix2 (Float.Fnum f) (Float.Fexp f)).

Lemma equiv_RNDs: forall (r:R),
   (FtoR 2%Z (RND_EvenClosest b 2 p r)
     = round radix2 (FLT_exp (-dExp b) p) rndNE r).

Lemma max_double_eq: (max_double = 9007199254740991*powerRZ 2 971)%R.

End Equiv.

Ltac destruct2 h :=
    let c:=fresh h "_C" in let r1:=fresh h "_e" in let r2:=fresh h "_m" in
    destruct h as (h, c, r1,r2) .

Ltac simpl_mk_double := match goal with
   |- context [df (mk_double ?f ?C ?r1 ?r2)] =>
                  (simpl (df (mk_double f C r1 r2)))
| |- context [double_exact (mk_double ?f ?C ?r1 ?r2)] =>
                  (simpl (double_exact (mk_double f C r1 r2)))
| |- context [double_model (mk_double ?f ?C ?r1 ?r2)] =>
                  (simpl (double_model (mk_double f C r1 r2)))
| h: context [df (mk_double ?f ?C ?r1 ?r2)] |- _ =>
                  (simpl (df (mk_double f C r1 r2)) in h)
| h: context [double_exact (mk_double ?f ?C ?r1 ?r2)] |- _ =>
                  (simpl (double_exact (mk_double f C r1 r2)) in h)
| h: context [double_model (mk_double ?f ?C ?r1 ?r2)] |- _ =>
                  (simpl (double_model (mk_double f C r1 r2)) in h)
| h: context [mk_double ?f ?C ?r1 ?r2 = ?d] |- _ =>
    (assert (FtoR radix f = FtoR radix (df d)) by (rewrite <- h; reflexivity);
       assert (r1 = double_exact d) by (rewrite <- h; reflexivity);
        assert (r2 = double_model d) by (rewrite <- h; reflexivity);
         clear h)
  end.

Ltac simpl_mk_single := match goal with
| |- context [sf (mk_single ?f ?C ?r1 ?r2)] =>
                  (simpl (sf (mk_single f C r1 r2)))
| |- context [single_exact (mk_single ?f ?C ?r1 ?r2)] =>
                  (simpl (single_exact (mk_single f C r1 r2)))
| |- context [single_model (mk_single ?f ?C ?r1 ?r2)] =>
                  (simpl (single_model (mk_single f C r1 r2)))
| h: context [sf (mk_single ?f ?C ?r1 ?r2)] |- _ =>
                  (simpl (sf (mk_single f C r1 r2)) in h)
| h: context [single_exact (mk_single ?f ?C ?r1 ?r2)] |- _ =>
                  (simpl (single_exact (mk_single f C r1 r2)) in h)
| h: context [single_model (mk_single ?f ?C ?r1 ?r2)] |- _ =>
                  (simpl (single_model (mk_single f C r1 r2)) in h)
| h: context [mk_single ?f ?C ?r1 ?r2 = ?d] |- _ =>
    (assert (FtoR radix f = FtoR radix (sf d)) by (rewrite <- h; reflexivity);
       assert (r1 = single_exact d) by (rewrite <- h; reflexivity);
        assert (r2 = single_model d) by (rewrite <- h; reflexivity);
         clear h)
  end.

Ltac destruct2_ds := match goal with
    h : double |- _ => destruct2 h
  | h : single |- _ => destruct2 h end.

Ltac simpl_IZR_aux := match goal with
  |- context [ IZR ?i ] =>
         (rewrite <- Z2R_IZR; simpl (Z2R i))
  | h: context [ IZR ?i ] |- _ =>
        (rewrite <- Z2R_IZR in h; simpl (Z2R i) in h)
  end.

Ltac simpl_IZR_aux2 := match goal with
  |- context [ (-(?n))%Z ] => (simpl (-(n))%Z)
  | h: context [ (-(?n))%Z ] |- _ => (simpl (-(n))%Z in h)
  end.

Ltac simpl_IZR := repeat simpl_IZR_aux; repeat simpl_IZR_aux2.

Lemma Rabs_eq: forall x y:R, (Rabs (x-y)=0 -> x=y).

Ltac Rabs_eq_transform := match goal with
  h : ( Rabs ( ?x - ?y ) = R0 ) |-_ =>
    (let hh:=fresh "h" in
           generalize h; clear h; intros hh;
          assert (h:x=y);[apply Rabs_eq; exact hh|clear hh])
  end.

Ltac simpl_post :=
  let h1:=fresh "H" in let h2:=fresh "H" in
    match goal with
  h: add_double_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: sub_double_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: mul_double_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: div_double_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: sqrt_double_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: neg_double_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: abs_double_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: double_of_real_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: add_single_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: sub_single_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: mul_single_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: div_single_post _ _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: sqrt_single_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: neg_single_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: abs_single_post _ _ _ |- _ => destruct h as (h,(h1,h2))
| h: single_of_real_post _ _ _ |- _ => destruct h as (h,(h1,h2))
end.

Ltac why2float := repeat simpl_post;
                  unfold double_round_error, double_total_error, no_overflow_double,
                      single_round_error, single_total_error, no_overflow_single,
                      round_double, round_double_aux, round_single, round_single_aux,
                      double_value, single_value
                  in * ;
                   repeat destruct2_ds;
                   repeat simpl_mk_double; repeat simpl_mk_single;
                   repeat Rabs_eq_transform;
                    fold FtoRradix in *.

Lemma equiv_RNDs_d: forall (r:R),
   (FtoR radix (RND_EvenClosest bdouble radix 53 r)
     = round radix2 (FLT_exp (-1074) 53) rndNE r)%R.

Lemma equiv_RNDs_s: forall (r:R),
   (FtoR radix (RND_EvenClosest bsingle radix 24 r)
    = round radix2 (FLT_exp (-149) 24) rndNE r)%R.

Ltac why2gappa := simpl_IZR; why2float ;
                 repeat rewrite equiv_RNDs_d in * |- *;
                 repeat rewrite equiv_RNDs_s in * |- *;
                 repeat rewrite max_double_eq in * |- *; unfold radix.