proposition: Lemma continuous_eval_ext : forall prog vars x m, no_floor_prog prog = true -> notXnan (nth m (eval_ext prog (Xreal x :: map Xreal vars)) Xnan) -> continuous (fun x => nth m (eval_real prog (x :: vars)) 0%R) x.
proof: Proof. intros prog vars x. rewrite /eval_ext /eval_real. intros m Hf H. eapply proj2. revert Hf m H. apply: (eval_inductive_prop_floor_fun _ _ (fun (f : R -> R) v => notXnan v -> v = Xreal (f x) /\ continuous f x)) => //. intros f1 f2 Heq b H Hb. case: (H Hb) => {H} H H'. split. by rewrite -Heq. now eapply continuous_ext. move => unop a b Hb HnotXnan. exact: continuous_unary. case => a1 a2 b1 b2 Ha1 Ha2 HnotXnan /=. - move: HnotXnan Ha1 Ha2. case: b1 => [|b1] // ;case: b2 => [|b2] // . move => _ [] // -> Hconta1 [] // -> Hconta2. by split => //; apply: continuous_plus. - move: HnotXnan Ha1 Ha2. case: b1 => [|b1] // ;case: b2 => [|b2] // . move => _ [] // -> Hconta1 [] // -> Hconta2. by split => //; apply: continuous_minus. - move: HnotXnan Ha1 Ha2. case: b1 => [|b1] // ;case: b2 => [|b2] // . move => _ [] // -> Hconta1 [] // -> Hconta2. by split => //; apply: continuous_mult. - move: HnotXnan Ha1 Ha2. case: b1 => [|b1] // ;case: b2 => [|b2] // . move => HnotXnan [] // Heq1 Hconta1 [] // Heq2 Hconta2. split => // . + move: HnotXnan. rewrite /= /Xdiv'. case: (is_zero b2) => // . by inversion Heq1; inversion Heq2. + apply: continuous_mult => // . apply: continuous_Rinv_comp => // Habs . by move: Heq2 HnotXnan => ->; rewrite /= /Xdiv' Habs is_zero_0. intros [|n]. simpl. intros _. apply (conj eq_refl). apply continuous_id. simpl. rewrite (nth_map 0). destruct le_lt_dec. easy. intros _. apply (conj eq_refl). apply continuous_const. 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