proposition: Lemma StepFun_P40 : forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:list R), a < b -> b < c -> adapted_couple f a b l1 lf1 -> adapted_couple f b c l2 lf2 -> adapted_couple f a c (app l1 l2) (FF (app l1 l2) f).
proof: Proof. intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; unfold adapted_couple in H1, H2; unfold adapted_couple; decompose [and] H1; decompose [and] H2; clear H1 H2; repeat split. - apply RList_P25; try assumption. rewrite H10; rewrite H4; unfold Rmin, Rmax; case (Rle_dec a b) as [|[]]; case (Rle_dec b c) as [|[]]; (right; reflexivity) || (left; assumption). - rewrite RList_P22. { rewrite H5; unfold Rmin, Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec a b) as [|[]]; [ reflexivity | left; assumption | apply Rle_trans with b; left; assumption | left; assumption ]. } red; intro; rewrite H1 in H6; discriminate. - rewrite RList_P24. { rewrite H9; unfold Rmin, Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec b c) as [|[]]; [ reflexivity | left; assumption | apply Rle_trans with b; left; assumption | left; assumption ]. } red; intro; rewrite H1 in H11; discriminate. - apply StepFun_P20. rewrite app_length; apply Nat.neq_0_lt_0; red; intro. assert (List.length l1 = 0)%nat as H12 by now destruct (List.length l1); inversion H1. rewrite H12 in H6; discriminate. - unfold constant_D_eq, open_interval; intros; elim (Nat.le_gt_cases (S (S i)) (length l1)); intro. + assert (H14 : pos_Rl (app l1 l2) i = pos_Rl l1 i). { apply RList_P26; apply Nat.succ_lt_mono; apply Nat.lt_succ_r; apply Nat.succ_le_mono; apply Nat.le_trans with (length l1); [ assumption | apply Nat.le_succ_diag_r ]. } assert (H15 : pos_Rl (app l1 l2) (S i) = pos_Rl l1 (S i)). { apply RList_P26; apply Nat.succ_lt_mono; apply Nat.lt_succ_r; assumption. } rewrite H14 in H2; rewrite H15 in H2; assert (H16 : (2 <= length l1)%nat). { apply Nat.le_trans with (S (S i)); [ repeat apply -> Nat.succ_le_mono; apply Nat.le_0_l | assumption ]. } elim (RList_P20 _ H16); intros r1 [r2 [r3 H17]]; rewrite H17; change (f x = pos_Rl (map f (mid_Rlist (app (cons r2 r3) l2) r1)) i) ; rewrite RList_P12. { induction i as [| i Hreci]. { simpl; assert (H18 := H8 0%nat); unfold constant_D_eq, open_interval in H18; assert (H19 : (0 < pred (length l1))%nat). { rewrite H17; simpl; apply Nat.lt_0_succ. } assert (H20 := H18 H19); repeat rewrite H20. { reflexivity. } { assert (H21 : r1 <= r2). { rewrite H17 in H3; apply (H3 0%nat). simpl; apply Nat.lt_0_succ. } elim H21; intro. { split. { rewrite H17; simpl; apply Rmult_lt_reg_l with 2; [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } rewrite H17; simpl; apply Rmult_lt_reg_l with 2; [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite (Rplus_comm r1); rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } elim H2; intros; rewrite H17 in H23; rewrite H17 in H24; simpl in H24; simpl in H23; rewrite H22 in H23; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)). } assumption. } clear Hreci; rewrite RList_P13. { rewrite H17 in H14; rewrite H17 in H15; change (pos_Rl (app (cons r2 r3) l2) i = pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; rewrite H14; change (pos_Rl (app (cons r2 r3) l2) (S i) = pos_Rl (cons r1 (cons r2 r3)) (S (S i))) in H15; rewrite H15; assert (H18 := H8 (S i)); unfold constant_D_eq, open_interval in H18; assert (H19 : (S i < pred (length l1))%nat). { apply -> Nat.lt_succ_lt_pred; apply Nat.succ_lt_mono; apply Nat.lt_succ_r; assumption. } assert (H20 := H18 H19); repeat rewrite H20. { reflexivity. } { rewrite <- H17; assert (H21 : pos_Rl l1 (S i) <= pos_Rl l1 (S (S i))). { apply (H3 (S i)); lia. } elim H21; intro. { split. { apply Rmult_lt_reg_l with 2; [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } apply Rmult_lt_reg_l with 2; [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l1 (S i))); rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } elim H2; intros; rewrite H22 in H23; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)). } assumption. } simpl; rewrite H17 in H1; simpl in H1; apply Nat.succ_lt_mono; assumption. } rewrite RList_P14; rewrite H17 in H1; simpl in H1; apply H1. + inversion H12. { assert (H16 : pos_Rl (app l1 l2) (S i) = b). { rewrite RList_P29. { rewrite H15; rewrite Nat.sub_diag; rewrite H10; unfold Rmin; case (Rle_dec b c) as [|[]]; [ reflexivity | left; assumption ]. } { rewrite H15; apply le_n. } induction l1 as [| r l1 Hrecl1]. { simpl in H15; discriminate. } clear Hrecl1; simpl in H1; simpl; apply -> Nat.succ_lt_mono; assumption. } assert (H17 : pos_Rl (app l1 l2) i = b). { rewrite RList_P26. { replace i with (pred (length l1)); [ rewrite H4; unfold Rmax; case (Rle_dec a b) as [|[]]; [ reflexivity | left; assumption ] | rewrite H15; reflexivity ]. } rewrite H15; apply Nat.lt_succ_diag_r. } rewrite H16 in H2; rewrite H17 in H2; elim H2; intros; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H14 H18)). } assert (H16 : pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1)). { apply RList_P29. { apply Nat.succ_le_mono; assumption. } apply Nat.lt_le_trans with (pred (length (app l1 l2))); [ assumption | apply Nat.le_pred_l ]. } assert (H17 : pos_Rl (app l1 l2) (S i) = pos_Rl l2 (S (i - length l1))). { replace (S (i - length l1)) with (S i - length l1)%nat. { apply RList_P29. { apply le_S_n; apply Nat.le_trans with (S i); [ assumption | apply Nat.le_succ_diag_r ]. } induction l1 as [| r l1 Hrecl1]. { simpl in H6; discriminate. } clear Hrecl1; simpl in H1; simpl; apply -> Nat.succ_lt_mono; assumption. } apply Nat.sub_succ_l, Nat.succ_le_mono; assumption. } assert (H18 : (2 <= length l1)%nat). { clear f c l2 lf2 H0 H3 H8 H7 H10 H9 H11 H13 i H1 x H2 H12 m H14 H15 H16 H17; induction l1 as [| r l1 Hrecl1]. { discriminate. } clear Hrecl1; induction l1 as [| r0 l1 Hrecl1]. { simpl in H5; simpl in H4; assert (H0 : Rmin a b < Rmax a b). { unfold Rmin, Rmax; case (Rle_dec a b) as [|[]]; [ assumption | left; assumption ]. } rewrite <- H5 in H0; rewrite <- H4 in H0; elim (Rlt_irrefl _ H0). } clear Hrecl1; simpl; repeat apply -> Nat.succ_le_mono; apply Nat.le_0_l. } elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19; change (f x = pos_Rl (map f (mid_Rlist (app (cons r2 r3) l2) r1)) i) ; rewrite RList_P12. 2:{ rewrite RList_P14; rewrite H19 in H1; simpl in H1; simpl; apply H1. } induction i as [| i Hreci]. { assert (H20 := le_S_n _ _ H15); assert (H21 := Nat.le_trans _ _ _ H18 H20); elim (Nat.nle_succ_0 _ H21). } clear Hreci; rewrite RList_P13. 2:{ simpl; rewrite H19 in H1; simpl in H1; apply Nat.succ_lt_mono; assumption. } rewrite H19 in H16; rewrite H19 in H17; change (pos_Rl (app (cons r2 r3) l2) i = pos_Rl l2 (S i - length (cons r1 (cons r2 r3)))) in H16; rewrite H16; change (pos_Rl (app (cons r2 r3) l2) (S i) = pos_Rl l2 (S (S i - length (cons r1 (cons r2 r3))))) in H17; rewrite H17; assert (H20 := H13 (S i - length l1)%nat); unfold constant_D_eq, open_interval in H20; assert (H21 : (S i - length l1 < pred (length l2))%nat). { apply Nat.lt_succ_lt_pred; rewrite <- Nat.sub_succ_l. { apply Nat.add_lt_mono_l with (length l1); rewrite Nat.add_comm, Nat.sub_add. { rewrite H19 in H1; simpl in H1; rewrite H19; simpl; rewrite app_length in H1; apply -> Nat.succ_lt_mono; assumption. } apply Nat.le_trans with (S i); [ apply Nat.succ_le_mono; assumption | apply Nat.le_succ_diag_r ]. } apply Nat.succ_le_mono; assumption. } assert (H22 := H20 H21); repeat rewrite H22. { reflexivity. } { rewrite <- H19; assert (H23 : pos_Rl l2 (S i - length l1) <= pos_Rl l2 (S (S i - length l1))). { apply H7; apply Nat.lt_succ_lt_pred. rewrite <- Nat.sub_succ_l. { apply Nat.add_lt_mono_l with (length l1); rewrite Nat.add_comm, Nat.sub_add. { rewrite H19 in H1; simpl in H1; rewrite H19; simpl; rewrite app_length in H1; apply -> Nat.succ_lt_mono; assumption. } apply Nat.le_trans with (S i); [ apply Nat.succ_le_mono; assumption | apply Nat.le_succ_diag_r ]. } apply Nat.succ_le_mono; assumption. } elim H23; intro. { split. { apply Rmult_lt_reg_l with 2; [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } apply Rmult_lt_reg_l with 2; [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - length l1))); rewrite <-Rplus_diag; apply Rplus_lt_compat_l; assumption | discrR ] ]. } rewrite <- H19 in H16; rewrite <- H19 in H17; elim H2; intros; rewrite H19 in H25; rewrite H19 in H26; simpl in H25; simpl in H16; rewrite H16 in H25; simpl in H26; simpl in H17; rewrite H17 in H26; simpl in H24; rewrite H24 in H25; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H25 H26)). } assert (H23 : pos_Rl (app l1 l2) (S i) = pos_Rl l2 (S i - length l1)). { rewrite H19; simpl; simpl in H16; apply H16. } assert (H24 : pos_Rl (app l1 l2) (S (S i)) = pos_Rl l2 (S (S i - length l1))). { rewrite H19; simpl; simpl in H17; apply H17. } rewrite <- H23; rewrite <- H24; assumption. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra