proposition: Theorem TwoSum_correct: a+b=x+y.
proof: Proof. Proof with auto with typeclass_instances. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero x) as (fx,(Hfx,Hfx')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero y) as (fy,(Hfy,Hfy')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. pose (Iplus := fun (f g:Pff.float) => RND_Closest (make_bound radix2 prec emin) radix2 (Z.abs_nat prec) choice (FtoR radix2 f + FtoR radix2 g)). pose (Iminus := fun (f g:Pff.float) => RND_Closest (make_bound radix2 prec emin) radix2 (Z.abs_nat prec) choice (FtoR radix2 f - FtoR radix2 g)). assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)). clear -prec_gt_0_ precisionNotZero emin_neg; intros x y. unfold Iplus. apply trans_eq with (round radix2 (FLT_exp (- dExp (make_bound radix2 prec emin)) prec) (Znearest choice) (FtoR radix2 x + FtoR radix2 y)). apply pff_round_N_is_round; try assumption. now apply make_bound_p. rewrite make_bound_Emin; try assumption. now rewrite Z.opp_involutive. assert (H2: forall x y, FtoR 2 (Iminus x y) = round_flt (FtoR 2 x - FtoR 2 y)). clear -prec_gt_0_ precisionNotZero emin_neg; intros x y. unfold Iminus. apply trans_eq with (round radix2 (FLT_exp (- dExp (make_bound radix2 prec emin)) prec) (Znearest choice) (FtoR radix2 x - FtoR radix2 y)). apply pff_round_N_is_round; try assumption. now apply make_bound_p. rewrite make_bound_Emin; try assumption. now rewrite Z.opp_involutive. assert (K: FtoR 2 (Iplus (Iminus fx (Iminus (Iplus fx fy) (Iminus (Iplus fx fy) fx))) (Iminus fy (Iminus (Iplus fx fy) fx))) = FtoR 2 fx + FtoR 2 fy - FtoR 2 (Iplus fx fy)). apply Knuth with (make_bound radix2 prec emin) (Z.abs_nat prec); try assumption. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. intros p q Fp Fq. apply RND_Closest_correct. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. unfold FtoRradix. intros p q r s Fp Fq Fr Fs M1 M2. now rewrite 2!H1, M1, M2. intros p q. apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Z.abs_nat prec). apply radix_gt_1. apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. apply RND_Closest_canonic. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. apply RND_Closest_canonic. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. now rewrite 2!H1, Rplus_comm. intros p q. apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Z.abs_nat prec). apply radix_gt_1. apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. apply FcanonicFopp. apply RND_Closest_canonic. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. apply RND_Closest_canonic. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. rewrite Fopp_correct, 2!H1, 2!Fopp_correct, <- Ropp_plus_distr. now rewrite round_N_opp_sym. intros p q. apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Z.abs_nat prec). apply radix_gt_1. apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. apply RND_Closest_canonic. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. apply RND_Closest_canonic. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. rewrite H1, H2, Fopp_correct. f_equal; ring. generalize K; rewrite 2!H1, 5!H2, H1. change 2%Z with (radix_val radix2). rewrite Hfx, Hfy. fold a; fold x'; fold dx; fold dy; fold b. intros K'; rewrite K'; ring. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat