proposition: Lemma incircle2d_spec : forall x1 y1 x2 y2 x3 y3 x4 y4, generic_format radix2 fxp x1 -> generic_format radix2 fxp y1 -> generic_format radix2 fxp x2 -> generic_format radix2 fxp y2 -> generic_format radix2 fxp x3 -> generic_format radix2 fxp y3 -> generic_format radix2 fxp x4 -> generic_format radix2 fxp y4 -> let Nx := norm3d (x1 - x4) (x2 - x4) (x3 - x4) in let Ny := norm3d (y1 - y4) (y2 - y4) (y3 - y4) in let M := (Nx * Ny * Rmax (Rsqr Nx) (Rsqr Ny))%R in let m := Rmin (Rmin (Rsqr Nx) (Rsqr Ny)) M in hombnd' m M (incircle2d x1 y1 x2 y2 x3 y3 x4 y4) (incircle2d_exact x1 y1 x2 y2 x3 y3 x4 y4) (Float radix2 449891379454319880216566500258074099295902168735244158654493060906025297480090105222776999487941175938788545391377857876066937154874210214115994952429543498973192 (-583)) (Float radix2 12 0).
proof: Proof. intros x1 y1 x2 y2 x3 y3 x4 y4 Fx1 Fy1 Fx2 Fy2 Fx3 Fy3 Fx4 Fy4. assert (X1 := hombnd_sub_init x1 x4 Fx1 Fx4). assert (Y1 := hombnd_sub_init y1 y4 Fy1 Fy4). assert (X2 := hombnd_sub_init x2 x4 Fx2 Fx4). assert (Y2 := hombnd_sub_init y2 y4 Fy2 Fy4). assert (X3 := hombnd_sub_init x3 x4 Fx3 Fx4). assert (Y3 := hombnd_sub_init y3 y4 Fy3 Fy4). apply (hombnd_fact' (Rmax_l _ (Rabs (x2 - x4)))) in X1. apply (hombnd_fact' (Rmax_l _ (Rabs (x3 - x4)))) in X1. apply (hombnd_fact' (Rmax_l _ (Rabs (y2 - y4)))) in Y1. apply (hombnd_fact' (Rmax_l _ (Rabs (y3 - y4)))) in Y1. apply (hombnd_fact' (Rmax_r (Rabs (x1 - x4)) _)) in X2. apply (hombnd_fact' (Rmax_l _ (Rabs (x3 - x4)))) in X2. apply (hombnd_fact' (Rmax_r (Rabs (y1 - y4)) _)) in Y2. apply (hombnd_fact' (Rmax_l _ (Rabs (y3 - y4)))) in Y2. apply (hombnd_fact' (Rmax_r (Rabs (x2 - x4)) _)) in X3. apply (hombnd_fact' (Rmax_r (Rabs (x1 - x4)) _)) in X3. apply (hombnd_fact' (Rmax_r (Rabs (y2 - y4)) _)) in Y3. apply (hombnd_fact' (Rmax_r (Rabs (y1 - y4)) _)) in Y3. rewrite Rmax_assoc in X3. rewrite Rmax_assoc in Y3. assert (M12 := hombnd_mul X1 Y2). assert (M21 := hombnd_mul X2 Y1). assert (M23 := hombnd_mul X2 Y3). assert (M32 := hombnd_mul X3 Y2). assert (M31 := hombnd_mul X3 Y1). assert (M13 := hombnd_mul X1 Y3). apply hombnd_rnd'' in M12. apply hombnd_rnd'' in M21. apply hombnd_rnd'' in M23. apply hombnd_rnd'' in M32. apply hombnd_rnd'' in M31. apply hombnd_rnd'' in M13. assert (D12 := hombnd_sub M12 M21). assert (D23 := hombnd_sub M23 M32). assert (D31 := hombnd_sub M31 M13). apply hombnd_rnd' in D12. apply hombnd_rnd' in D23. apply hombnd_rnd' in D31. rewrite Rmin_left in D12 by apply Rle_refl. rewrite Rmin_left in D23 by apply Rle_refl. rewrite Rmin_left in D31 by apply Rle_refl. clear M12 M21 M23 M32 M31 M13. assert (M1x := hombnd_mul X1 X1). assert (M1y := hombnd_mul Y1 Y1). assert (M2x := hombnd_mul X2 X2). assert (M2y := hombnd_mul Y2 Y2). assert (M3x := hombnd_mul X3 X3). assert (M3y := hombnd_mul Y3 Y3). clear X1 Y1 X2 Y2 X3 Y3. apply hombnd_rnd'' in M1x. apply hombnd_rnd'' in M1y. apply hombnd_rnd'' in M2x. apply hombnd_rnd'' in M2y. apply hombnd_rnd'' in M3x. apply hombnd_rnd'' in M3y. apply (hombnd_cond'' (Rmin_l _ (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4))))) in M1x. apply (hombnd_cond'' (Rmin_r (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) _)) in M1y. apply (hombnd_fact' (Rmax_l _ (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4))))) in M1x. apply (hombnd_fact' (Rmax_r (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) _)) in M1y. apply (hombnd_cond'' (Rmin_l _ (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4))))) in M2x. apply (hombnd_cond'' (Rmin_r (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) _)) in M2y. apply (hombnd_fact' (Rmax_l _ (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4))))) in M2x. apply (hombnd_fact' (Rmax_r (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) _)) in M2y. apply (hombnd_cond'' (Rmin_l _ (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4))))) in M3x. apply (hombnd_cond'' (Rmin_r (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) _)) in M3y. apply (hombnd_fact' (Rmax_l _ (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4))))) in M3x. apply (hombnd_fact' (Rmax_r (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) _)) in M3y. assert (Z1 := hombnd_add M1x M1y). assert (Z2 := hombnd_add M2x M2y). assert (Z3 := hombnd_add M3x M3y). clear M1x M1y M2x M2y M3x M3y. apply hombnd_rnd' in Z1. apply hombnd_rnd' in Z2. apply hombnd_rnd' in Z3. rewrite Rmin_max in Z1. rewrite Rmin_max in Z2. rewrite Rmin_max in Z3. apply (hombnd_cond'' (Rmin_l _ (Rmin (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4)))))) in D12. apply (hombnd_cond'' (Rmin_l _ (Rmin (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4)))))) in D23. apply (hombnd_cond'' (Rmin_l _ (Rmin (Rsqr (norm3d (x1 - x4) (x2 - x4) (x3 - x4))) (Rsqr (norm3d (y1 - y4) (y2 - y4) (y3 - y4)))))) in D31. apply (hombnd_cond'' (Rmin_r (norm3d (x1 - x4) (x2 - x4) (x3 - x4) * norm3d (y1 - y4) (y2 - y4) (y3 - y4)) _)) in Z1. apply (hombnd_cond'' (Rmin_r (norm3d (x1 - x4) (x2 - x4) (x3 - x4) * norm3d (y1 - y4) (y2 - y4) (y3 - y4)) _)) in Z2. apply (hombnd_cond'' (Rmin_r (norm3d (x1 - x4) (x2 - x4) (x3 - x4) * norm3d (y1 - y4) (y2 - y4) (y3 - y4)) _)) in Z3. assert (M1 := hombnd_mul D12 Z3). assert (M2 := hombnd_mul D23 Z1). assert (M3 := hombnd_mul D31 Z2). clear D12 D23 D31 Z1 Z2 Z3. apply hombnd_rnd' in M1. apply hombnd_rnd' in M2. apply hombnd_rnd' in M3. assert (A1 := hombnd_add M1 M2). clear M1 M2. apply hombnd_rnd' in A1. rewrite Rmin_min in A1. assert (A2 := hombnd_add A1 M3). apply hombnd_rnd' in A2. clear A1 M3. rewrite Rmin_min in A2. rewrite (Rmin_right (Rmult _ _)) in A2. exact A2. clear. unfold Rmin. destruct Rle_dec as [H|H]. apply Rsqr_incr_0 in H. apply Rmult_le_compat_l with (2 := H). repeat apply Rmax_case ; apply Rabs_pos. unfold norm3d ; repeat apply Rmax_case ; apply Rabs_pos. unfold norm3d ; repeat apply Rmax_case ; apply Rabs_pos. apply Rnot_le_lt in H. apply Rlt_le in H. apply Rsqr_incr_0 in H. apply Rmult_le_compat_r with (2 := H). repeat apply Rmax_case ; apply Rabs_pos. unfold norm3d ; repeat apply Rmax_case ; apply Rabs_pos. unfold norm3d ; repeat apply Rmax_case ; apply Rabs_pos. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)