proposition: Lemma decidable_atom : forall a, { convert_atom a } + { not (convert_atom a) }.
proof: Proof. Proof with auto with typeclass_instances. intros [[l|] e [u|]|x y l u|x y|x y|fmt x|fmt x] ; simpl. destruct (Rle_lt_dec (convert_expr l) (convert_expr e)) as [Hl|Hl]. destruct (Rle_lt_dec (convert_expr e) (convert_expr u)) as [Hu|Hu]. now left ; split. right. intros (_,H). now apply Rlt_not_le with (1 := Hu). right. intros (H,_). now apply Rlt_not_le with (1 := Hl). destruct (Rle_lt_dec (convert_expr l) (convert_expr e)) as [Hl|Hl]. now left. right. now apply Rlt_not_le. destruct (Rle_lt_dec (convert_expr e) (convert_expr u)) as [Hu|Hu]. now left. right. now apply Rlt_not_le. now left. destruct (Req_EM_T (convert_expr y) 0) as [Zy|Zy]. destruct (Req_EM_T (convert_expr x) 0) as [Zx|Zx]. destruct (Rle_lt_dec (convert_expr l) (convert_expr u)) as [H|H]. left. exists (convert_expr l). split. split. apply Rle_refl. exact H. now rewrite Zy, Rmult_0_l. right. intros (eps,((H1,H2),_)). apply Rlt_not_le with (1 := H). now apply Rle_trans with eps. right. intros (eps,(_,H')). now rewrite Zy, Rmult_0_l in H'. destruct (Rle_lt_dec (convert_expr l) (convert_expr x / convert_expr y - 1)) as [Hl|Hl]. destruct (Rle_lt_dec (convert_expr x / convert_expr y - 1) (convert_expr u)) as [Hu|Hu]. left. exists (convert_expr x / convert_expr y - 1)%R. split. now split. now field. right. intros (eps,((_,H),H')). apply Rlt_not_le with (1 := Hu). rewrite H'. now replace (convert_expr y * (1 + eps) / convert_expr y - 1)%R with eps ; [idtac | field]. right. intros (eps,((H,_),H')). apply Rlt_not_le with (1 := Hl). rewrite H'. now replace (convert_expr y * (1 + eps) / convert_expr y - 1)%R with eps ; [idtac | field]. destruct (Rle_lt_dec (convert_expr x) (convert_expr y)) as [H|H]. now left. right. now apply Rlt_not_le. apply Req_EM_T. apply Req_EM_T. destruct fmt as [e|e p|p]. simpl. destruct (Req_EM_T (convert_expr x) (round radix2 (FIX_exp e) rndZR (convert_expr x))) as [H|H]. left. apply FIX_format_generic. rewrite H. apply generic_format_round... right. contradict H. apply sym_eq, round_generic... now apply generic_format_FIX. destruct (Z_lt_le_dec 0 p) as [Hp|Hp]. destruct (Req_EM_T (convert_expr x) (round radix2 (FLT_exp e p) rndZR (convert_expr x))) as [H|H]. left. apply FLT_format_generic. apply Hp. rewrite H. apply generic_format_round... right. contradict H. apply sym_eq, round_generic... now apply generic_format_FLT. destruct p. destruct (Req_EM_T (convert_expr x) 0) as [H|H]. left. rewrite H. exists (Float radix2 0 e). apply sym_eq, F2R_0. apply eq_refl. apply Z.le_refl. right. intros ((xm,xe),H1,H2,H3). simpl in H2. assert (xm = Z0). clear -H2 ; zify ; lia. now rewrite H0, F2R_0 in H1. now elim Hp. right. intros ((xm,xe),H1,H2,H3). apply Zlt_not_le with (1 := H2). apply Zabs_pos. destruct (Z_lt_le_dec 0 p) as [Hp|Hp]. destruct (Req_EM_T (convert_expr x) (round radix2 (FLX_exp p) rndZR (convert_expr x))) as [H|H]. left. apply FLX_format_generic. apply Hp. rewrite H. apply generic_format_round... right. contradict H. apply sym_eq, round_generic... now apply generic_format_FLX. destruct p. destruct (Req_EM_T (convert_expr x) 0) as [H|H]. left. rewrite H. exists (Float radix2 0 0). apply sym_eq, F2R_0. apply eq_refl. right. intros ((xm,xe),H1,H2). simpl in H2. assert (xm = Z0). clear -H2 ; zify ; lia. now rewrite H0, F2R_0 in H1. now elim Hp. right. intros ((xm,xe),H1,H2). apply Zlt_not_le with (1 := H2). apply Zabs_pos. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library