proposition: Lemma average_symmetry_Ropp: forall u v, format u -> format v -> average (-u) (-v) = - average u v.
proof: Proof. Proof with auto with typeclass_instances. assert (forall u v, 0 <= u -> format u -> format v -> average (-u) (-v) = - average u v). intros u v Hu Fu Fv; unfold average. rewrite 2!Rabs_Ropp. destruct Hu as [Hu|Hu]. rewrite Rle_bool_false. 2: apply Ropp_lt_cancel. 2: now rewrite Ropp_involutive, Ropp_0. rewrite (Rle_bool_true 0 u); [idtac|now left]. rewrite Rabs_right. 2: apply Rle_ge; now left. destruct (total_order_T 0 v) as [Hv|Hv];[destruct Hv as [Hv|Hv] |idtac]. rewrite Rle_bool_false. 2: apply Ropp_lt_cancel. 2: now rewrite Ropp_involutive, Ropp_0. rewrite (Rle_bool_true 0 v); [idtac|now left]. rewrite Rabs_right. 2: apply Rle_ge; now left. case (Rle_bool_spec u v);intros. apply avg_half_sub_symmetry_Ropp. apply avg_half_sub_symmetry_Ropp. rewrite <- Hv, Ropp_0, Rabs_R0. rewrite Rle_bool_true ;[idtac|now right]. rewrite Rle_bool_false; try exact Hu. unfold avg_naive, avg_half_sub. unfold Rminus; rewrite Ropp_0, Rplus_0_l, 2!Rplus_0_r. rewrite (round_generic _ _ _ u); trivial. rewrite (round_generic _ _ _ (-u)). 2: now apply generic_format_opp. rewrite <- round_NE_opp. rewrite <- round_NE_opp. rewrite (round_generic _ _ _ (round_flt (-(u/2)))). apply f_equal; field. apply generic_format_round... rewrite Rabs_left; trivial. rewrite Rle_bool_true. rewrite Rle_bool_false; trivial. apply avg_naive_symmetry_Ropp. rewrite <- Ropp_0; apply Ropp_le_contravar. now left. rewrite <- Hu, Ropp_0, Rabs_R0. rewrite Rle_bool_true. 2: now right. rewrite (Rle_bool_true 0 (Rabs v)). 2: apply Rabs_pos. destruct (total_order_T 0 v) as [Hv|Hv];[destruct Hv as [Hv|Hv] |idtac]. rewrite Rle_bool_false. rewrite Rle_bool_true. unfold avg_naive, avg_half_sub. unfold Rminus; rewrite Ropp_0, 2!Rplus_0_l, Rplus_0_r. rewrite (round_generic _ _ _ v); trivial. rewrite (round_generic _ _ _ (-v)). 2: now apply generic_format_opp. rewrite <- round_NE_opp. rewrite <- round_NE_opp. rewrite (round_generic _ _ _ (round_flt (-(v/2)))). apply f_equal; field. apply generic_format_round... now left. rewrite <- Ropp_0; now apply Ropp_lt_contravar. rewrite <- Hv, Ropp_0. rewrite Rle_bool_true. 2: now right. unfold avg_half_sub. replace (0-0) with 0 by ring; rewrite round_0... unfold Rdiv; rewrite Rmult_0_l, round_0, Rplus_0_l... rewrite round_0... ring. rewrite Rle_bool_true. rewrite Rle_bool_false. unfold avg_naive, avg_half_sub. unfold Rminus; rewrite Ropp_0, 2!Rplus_0_l, Rplus_0_r. rewrite (round_generic _ _ _ v); trivial. rewrite (round_generic _ _ _ (-v)). 2: now apply generic_format_opp. rewrite <- round_NE_opp. rewrite (round_generic _ _ _ (round_flt (-v/2))). apply f_equal; field. apply generic_format_round... exact Hv. rewrite <- Ropp_0; apply Ropp_le_contravar; now left. intros u v Fu Fv. case (Rle_or_lt 0 u). intros Hu; now apply H. intros Hu. apply trans_eq with (- average (--u) (--v)). rewrite (H (-u) (-v)). ring. rewrite <- Ropp_0; apply Ropp_le_contravar; now left. apply generic_format_opp... apply generic_format_opp... apply f_equal, f_equal2; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)