proposition: Lemma xreal_to_real : forall (P1 : ExtendedR -> Prop) (P2 : R -> Prop), (P1 Xnan -> forall r, P2 r) -> (forall r, P1 (Xreal r) -> P2 r) -> forall prog terms n, P1 (nth n (eval_ext prog (map Xreal terms)) Xnan) -> P2 (nth n (eval_real prog terms) 0%R).
proof: Proof. intros P1 P2 HP1 HP2 prog terms n. unfold eval_ext, eval_real. refine (_ (eval_inductive_prop _ _ (fun a b => match a with Xreal a => a = b | _ => True end) ext_operations real_operations _ _ (map Xreal terms) terms _ prog n)). simpl. case (nth n (eval_generic ext_operations prog (map Xreal terms)) Xnan). intros _ H. now apply HP1. intros y H. rewrite H. apply HP2. destruct a as [|a]. now destruct o. intros b H. rewrite H. destruct o ; try easy ; simpl ; unfold Xinv'. now case (is_zero b). unfold Xtan'. now case (is_zero (cos b)). unfold Xln'. now case (is_positive b). generalize (Xpower_int_correct n0 (Xreal b)). simpl. now case Xpower_int'. destruct a1 as [|a1]. now destruct o. destruct a2 as [|a2]. now destruct o. intros b1 b2 H1 H2. rewrite H1 H2. destruct o ; try easy ; simpl ; unfold Xdiv'. now destruct (is_zero b2). intros k. rewrite (nth_map 0). now destruct le_lt_dec as [H|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