proposition: Lemma change_rel_prop : stable_atom change_rel_func.
proof: Proof. unfold change_rel_func. intros [l v u|x y l u|v w|v w|f x|f x] ; try easy. destruct v as [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; try easy. destruct o ; try easy. destruct x as [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; try easy. destruct o ; try easy. destruct w as [u|u|u v|u v|o u|o u v|u|u|u|u|u|u|f m u] ; try easy. destruct o ; try easy. destruct v as [v|v|v w|v w|o v|o v w|v|v|v|v|v|v|f m v] ; try easy. destruct o ; try easy. case_eq (RExpr_beq y v) ; try easy. intros Hb. rewrite <- internal_RExpr_dec_bl with (1 := Hb). assert (H := get_float2_bound_correct u). destruct (get_float2_bound u) as [u1|u1|m e|u1 u2|o u1|o u1 u2|u1|u1|u1|u1|u1|u1|f u1] ; try easy. destruct m as [|m|m] ; try easy. simpl in H |- *. change (Float2 (Zneg m) e) with (Gappa_dyadic.Fopp2 (Float2 (Zpos m) e)). rewrite Gappa_dyadic.Fopp2_correct. rewrite H. split ; intro H'. now apply <- change_rel_aux. apply -> change_rel_aux. split. rewrite <- H. now apply (Gappa_dyadic.Fpos0_correct (Float2 (Zpos m) e)). exact H'. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library