proposition: Lemma unary_diff_bnd_correct : forall prec o f f', let u x := unary (diff_operations _ ext_operations) o (f x, f' x) in forall yi yi' xi, (forall x, contains xi x -> contains (I.convert yi) (f x)) -> (forall x, contains xi x -> contains (I.convert yi') (f' x)) -> let v := unary (diff_operations _ (BndValuator.operations prec)) o (yi, yi') in (forall x, contains xi x -> contains (I.convert (snd v)) (snd (u x))).
proof: Proof. intros prec o f f' u yi yi' xi Hf Hf' v x Hx. destruct o ; simpl ; repeat first [ now rewrite I.nai_correct | apply I.neg_correct | apply I.abs_correct | apply I.inv_correct | apply I.sqr_correct | apply I.sqrt_correct | apply I.cos_correct | apply I.sin_correct | apply I.tan_correct | apply I.atan_correct | apply I.exp_correct | apply I.ln_correct | apply I.power_int_correct | apply I.add_correct | apply I.mul_correct | apply I.div_correct | apply I.fromZ_correct | refine (I.add_correct _ _ _ (Xreal 1%R) _ _ _) | refine (I.mul_correct _ _ _ (Xreal (IZR _)) _ _ _) ] ; try now first [ apply Hf | apply Hf' ]. specialize (Hf _ Hx). generalize (I.sign_strict_correct yi). case I.sign_strict ; try rewrite I.nai_correct ; try easy. intros H. specialize (H _ Hf). rewrite (proj1 H). simpl. rewrite Rcompare_Lt. apply I.neg_correct. now apply Hf'. apply H. intros H. specialize (H _ Hf). rewrite (proj1 H). simpl. rewrite Rcompare_Gt. now apply Hf'. apply H. specialize (Hf _ Hx). generalize (I.sign_strict_correct yi). case I.sign_strict ; try rewrite I.nai_correct ; try easy. intros H. specialize (H _ Hf). rewrite {1}(proj1 H). simpl. rewrite Rcompare_Gt. apply I.div_correct. now apply Hf'. exact Hf. apply H. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog