proposition: Lemma roundN_eq : forall r f, ( forall m, (0 <= m)%Z -> forall b c, rneg r (rnd_record_mk (ZtoN m) b c) = andb b (orb c (negb (f (- (m + 1))%Z))) ) -> ( forall m, (0 <= m)%Z -> forall b c, rpos r (rnd_record_mk (ZtoN m) b c) = andb b (orb c (f m)) ) -> forall x, rndG r x = Znearest f x.
proof: Proof. Proof with auto with typeclass_instances. intros r f Hn Hp x. simpl. destruct (Req_dec (IZR (Zfloor x)) x) as [H1|H1]. rewrite <- H1. rewrite 2!Zrnd_IZR... unfold rndG. case Rcompare_spec ; intros H2. rewrite hrndG_N. 2: apply rneg_good. rewrite Znearest_opp, Z.opp_involutive. unfold Znearest. case Rcompare ; trivial. rewrite Hn. simpl. replace (- (- (Zfloor x + 1) + 1))%Z with (Zfloor x) by ring. now rewrite negb_involutive. cut (Zfloor x < 0)%Z. lia. apply lt_IZR. apply Rle_lt_trans with (2 := H2). apply Zfloor_lb. intros b. rewrite Hn. apply andb_true_r. apply Zfloor_lub. apply Rlt_le. now apply Ropp_0_gt_lt_contravar. rewrite H2. apply sym_eq. apply Zrnd_IZR... rewrite hrndG_N. 2: apply rpos_good. unfold Znearest. case Rcompare ; trivial. rewrite Hp. apply refl_equal. apply Zfloor_lub. now apply Rlt_le. intros b. rewrite Hp. apply andb_true_r. apply Zfloor_lub. now apply Rlt_le. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux