proposition: Theorem generateCProp_taylor_correct {Tl T} : forall (t : ArithExpr Tl T), ArrayFree t -> forall (lM : evalExprTypeRounded_list Tl) md hyps P, md <> mode_NA -> let lR := M2R_list lM in let l := toList lR in generateCProp_taylor t md (length l) hyps = P -> Reify.eval_hyps hyps l (CPropToProp P l -> wellBehaved t lM md).
proof: Proof. intros t IAF lM md hyps P Hmd lR l <-. apply (IH.R.eval_hyps_bnd_correct prec). generalize (extractCProp_correct t IAF lM md). unfold generateCProp_taylor. set (p0 := extractCProp _ _). destruct_tuple_obj p0. set (unsolved := snd p0). intros [Hm Hm'] Hh Hg; [easy |]. apply Hm'. revert Hm Hg. set (tointerval := BTreeToList (fst p0)). set (goals := map (fun p => AtomToGoal p) tointerval). set (lexpr := map (fun p => CArithExprToTree (getCArithExpr p)) tointerval). generalize (extract_list_correct lexpr l). destruct extract_list as [|prog consts]; [easy |]. intros H. unfold eval_real_nth in H. set (bounds := IH.compute_inputs prec hyps consts). destruct bounds as [| xi li] eqn:Hbounds; [easy |]. intros Hm Hg. eapply par_construct_mergerest. split; [| exact Hg]. apply (IH.app_merge_hyps_eval_bnd _ _ _ consts) in Hh. fold bounds in Hh. set (l' := l ++ map (fun c : Tree.expr => Tree.eval c nil) consts). fold l' in H, Hh. clear Hm' Hg. rewrite Hbounds in Hh. destruct Hh as [Hl Hh]. destruct l' as [| x l']; [easy |]. assert (Hh' : IH.A.contains_all li l'). { split. - now injection Hl. - intros n. apply (Hh (S n)). } generalize (fun n => IH.A.TaylorValuator.eval_correct prec degree prog li l' Hh' n xi xi x (Hh 0%nat)). intros H'. clearbody tointerval. clear p0 unsolved. unfold goals. clear goals. clear T t IAF. fold lR l. clearbody l. clear Tl lM lR. clearbody bounds. revert H'. generalize ((IH.A.TaylorValuator.eval prec degree xi prog (IH.A.TaylorValuator.TM.var :: map IH.A.TaylorValuator.TM.const li))). intros l0 H'. set (l0' := (map (fun p : IH.A.TaylorValuator.TM.T => IH.A.TaylorValuator.TM.eval (prec, degree) p xi xi) l0)). cut (forall k, nth k (compareResults (map (fun p : Atom => AtomToGoal p) tointerval) l0') false = true -> AtomToProp (nth k tointerval (InInt32 (CInt 0))) l). { generalize l0'. clear. induction tointerval; [easy |]. intros l0' H''. simpl. destruct l0' as [| i l0']; [easy |]. simpl in H''. generalize (H'' O). destruct IH.R.eval_goal_bnd; intros Ha. - split; [| now apply Ha]. apply IHtointerval. intros k. apply (H'' (S k)). - apply IHtointerval. intros k. apply (H'' (S k)). } intros k Hk. destruct (Nat.lt_ge_cases k (length tointerval)) as [Hkl | Hkl]. 2: { rewrite nth_overflow in Hk; [easy |]. clearbody l0'. clear -Hkl. revert l0' k Hkl. induction tointerval; [easy |]. simpl. intros l0' k Hkl. destruct l0' as [| i l0']; [apply Nat.le_0_l |]. simpl. destruct k as [| k]; [easy |]. apply le_n_S, (IHtointerval l0' k). now apply le_S_n in Hkl. } apply AtomToGoal_correct with (i := (nth k l0' Iaux.nai)) (1 := (Hm k)). - specialize (H' k). rewrite H in H' by (unfold lexpr; now rewrite map_length). unfold lexpr in H'. rewrite (Eval.nth_map_lt (InInt32 (CInt 0))) in H' by easy. revert Hk Hkl. unfold l0'. clear -H'. revert tointerval l0 H'. induction k. + intros [| a tointerval] [| x0 l0]; easy. + intros [| a tointerval] [| x0 l0]; try easy. simpl. intros H' Hk Hkl. apply IHk. 3: now apply Nat.succ_lt_mono. easy. easy. - clearbody l0'. clear -Hk Hkl. revert l0' k Hk Hkl. induction tointerval; [easy |]. simpl. intros [| i l0']; [now intros [|] |]. simpl. intros [| k]; [easy |]. simpl. intros Hk Hkl. apply IHtointerval; [easy |]. now apply Nat.succ_lt_mono. Qed.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr