proposition: Lemma eval_diff_correct : forall prog terms n x, let v := nth n (eval_generic (diff_operations _ ext_operations) prog ((x, Xmask (Xreal 1) x) :: map (fun v => (Xreal v, Xmask (Xreal 0) x)) terms)) (Xnan, Xnan) in nth n (eval_ext prog (x :: map Xreal terms)) Xnan = fst v /\ Xderive_pt (fun x => nth n (eval_ext prog (x :: map Xreal terms)) Xnan) x (snd v).
proof: Proof. intros prog terms n x. refine (eval_inductive_prop_fun _ _ (fun a b => a x = fst b /\ Xderive_pt a x (snd b)) _ _ _ _ _ _ _ _ _ _). intros a1 a2 Heq (bl, br). simpl. intros (Hl, Hr). split. now rewrite <- Heq. apply Xderive_pt_eq_fun with (2 := Hr). intros. now apply sym_eq. intros o a (bl, br) (Hl, Hr). simpl in Hl. rewrite <- Hl. now apply unary_diff_correct. intros o a1 a2 (bl1, br1) (bl2, br2) (Hl1, Hr1) (Hl2, Hr2). simpl in Hl1, Hl2. rewrite <- Hl1, <- Hl2. now apply binary_diff_correct. clear n. intros [|n]. simpl. repeat split. apply Xderive_pt_identity. simpl. split. rewrite <- (map_nth (@fst ExtendedR ExtendedR)). rewrite map_map. apply (f_equal (fun v => nth n v _)). now apply map_ext. rewrite <- map_nth. rewrite map_map. simpl. rewrite (nth_map 0). destruct le_lt_dec as [H|H]. rewrite nth_overflow. now case x. now rewrite map_length. rewrite -> (nth_map_lt 0) by easy. apply Xderive_pt_constant. 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