Commit c8724c7d authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Add missing WhyType instances for Coq realizations of single and double floating-point arithmetic.

It should help with some Jessie failures related to arrays of floating-point numbers.
parent 5073ebc8
......@@ -11,3 +11,7 @@ exact (t 53 1024).
Defined.
Global Instance double_WhyType : WhyType double.
Proof.
apply t_WhyType.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZArith.
Require Import Rbase.
Require Import Rbasic_fun.
......@@ -34,6 +35,65 @@ Record t : Set := mk_fp {
model : R
}.
Lemma t_inv :
forall x xe xm y ye ym,
(x = y -> xe = ye -> xm = ym -> False) ->
(mk_fp x xe xm <> mk_fp y ye ym).
Proof.
intros x xe xm y ye ym H H'.
apply H.
exact (f_equal binary H').
exact (f_equal exact H').
exact (f_equal model H').
Qed.
Lemma t_WhyType : WhyType t.
Proof with
match goal with
| _ => try ( right ; apply t_inv ; easy )
end.
split.
split.
apply Fappli_IEEE.B754_zero.
exact false.
exact R0.
exact R0.
intros x y.
destruct x as (x,xv,xe,xm).
destruct y as (y,yv,ye,ym).
destruct (Req_EM_T xe ye) as [He|He]...
destruct (Req_EM_T xm ym) as [Hm|Hm]...
destruct x as [xs|xs| |xs xm' xe' xH] ;
destruct y as [ys|ys| |ys ym' ye' yH]...
destruct (Bool.bool_dec xs ys) as [Hs|Hs].
left.
apply f_equal3 ; try easy.
now apply f_equal.
right.
apply t_inv.
intros H.
now injection H.
destruct (Bool.bool_dec xs ys) as [Hs|Hs].
left.
apply f_equal3 ; try easy.
now apply f_equal.
right.
apply t_inv.
intros H.
now injection H.
left.
now apply f_equal3.
destruct (Req_EM_T xv yv) as [Hv|Hv].
left.
apply f_equal3 ; try easy.
now apply B2R_inj.
right.
apply t_inv.
intros H _ _.
apply Hv.
now apply f_equal.
Qed.
Record t_strict: Set := mk_fp_strict {
datum :> t;
finite : is_finite prec emax (binary datum) = true
......
......@@ -11,3 +11,7 @@ exact (t 24 128).
Defined.
Global Instance single_WhyType : WhyType single.
Proof.
apply t_WhyType.
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