proposition: Lemma eval_diff_bnd_correct : forall prec prog bounds vars, contains_all bounds vars -> forall n, let ff' x := nth n (eval_generic (diff_operations _ ext_operations) prog ((x, Xmask (Xreal 1) x) :: map (fun v => (Xreal v, Xmask (Xreal 0) x)) vars)) (Xnan, Xnan) in let ffi' xi := nth n (eval_generic (diff_operations _ (BndValuator.operations prec)) prog ((xi, I.mask (I.fromZ_small 1) xi) :: map (fun b => (b, I.mask I.zero xi)) bounds)) (I.nai, I.nai) in forall xi, nth n (BndValuator.eval prec prog (xi :: bounds)) I.nai = fst (ffi' xi) /\ (forall x, contains (I.convert xi) x -> contains (I.convert (snd (ffi' xi))) (snd (ff' x))).
proof: Proof. intros prec prog bounds vars Hv n ff' ffi' xi. split. unfold ffi', BndValuator.eval. apply (eval_inductive_prop _ (I.type * I.type) (fun a b => a = fst b)). intros o a (bl, br) H. rewrite H. now destruct o. intros o a1 a2 (bl1, br1) (bl2, br2) H1 H2. rewrite H1 H2. now destruct o. clear. intros [|n]. apply refl_equal. simpl. rewrite <- (map_nth (@fst I.type I.type)). rewrite map_map. simpl. apply sym_eq. exact (map_nth _ _ _ _). refine (let toto := _ in fun x Hx => proj2 (toto x Hx : contains (I.convert (fst (ffi' xi))) (fst (ff' x)) /\ _)). apply (eval_inductive_prop_fun (ExtendedR * _) (I.type * _) (fun a b => forall x, contains (I.convert xi) x -> contains (I.convert (fst b)) (fst (a x)) /\ contains (I.convert (snd b)) (snd (a x)))). intros f1 f2 Heq (yi, yi') H x Hx. rewrite <- Heq. now apply H. intros o f (yi, yi') H x Hx. rewrite (surjective_pairing (f x)). split. assert (Hf := proj1 (H x Hx)). destruct o ; simpl ; [ 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.nearbyint_correct | apply J.round_flt_correct' | apply I.error_flt_correct | apply J.round_fix_correct' | apply I.error_fix_correct ] ; exact Hf. apply (unary_diff_bnd_correct prec o (fun x => fst (f x)) (fun x => snd (f x))) with (3 := Hx). exact (fun x Hx => proj1 (H x Hx)). exact (fun x Hx => proj2 (H x Hx)). intros o f1 f2 (yi1, yi1') (yi2, yi2') H1 H2 x Hx. rewrite (surjective_pairing (f1 x)). rewrite (surjective_pairing (f2 x)). split. assert (Hf1 := proj1 (H1 x Hx)). assert (Hf2 := proj1 (H2 x Hx)). destruct o ; simpl ; [ apply I.add_correct | apply I.sub_correct | apply I.mul_correct | apply I.div_correct ] ; first [ exact Hf1 | exact Hf2 ]. apply (binary_diff_bnd_correct prec o (fun x => fst (f1 x)) (fun x => fst (f2 x)) (fun x => snd (f1 x)) (fun x => snd (f2 x))) with (5 := Hx). exact (fun x Hx => proj1 (H1 x Hx)). exact (fun x Hx => proj1 (H2 x Hx)). exact (fun x Hx => proj2 (H1 x Hx)). exact (fun x Hx => proj2 (H2 x Hx)). clear -Hv. intros [|n] x Hx ; simpl. split. exact Hx. apply I.mask_correct. now apply I.fromZ_small_correct. exact Hx. split. rewrite <- (map_nth (@fst I.type I.type)). rewrite <- (map_nth (@fst ExtendedR ExtendedR)). rewrite 2!map_map /= map_id. now apply contains_map_Xreal. rewrite <- (map_nth (@snd I.type I.type)). rewrite <- (map_nth (@snd ExtendedR ExtendedR)). rewrite 2!map_map /=. rewrite (nth_map I.nai). destruct le_lt_dec as [H|H]. rewrite nth_overflow. now rewrite I.nai_correct. rewrite map_length. now rewrite <- (proj1 Hv). rewrite (nth_map_lt 0). apply I.mask_correct. rewrite I.zero_correct. split ; apply Rle_refl. exact Hx. now rewrite <- (proj1 Hv). 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