proposition: Lemma StepFun_P22 : forall (a b:R) (f g:R -> R) (lf lg:list R), a <= b -> is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg).
proof: Proof. unfold is_subdivision; intros a b f g lf lg Hyp X X0; elim X; elim X0; clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. } assert (Hyp_max : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. } apply existT with (FF (cons_ORlist lf lg) f); unfold adapted_couple in p, p0; decompose [and] p; decompose [and] p0; clear p p0; rewrite Hyp_min in H6; rewrite Hyp_min in H1; rewrite Hyp_max in H0; rewrite Hyp_max in H5; unfold adapted_couple; repeat split. - apply RList_P2; assumption. - rewrite Hyp_min; symmetry ; apply Rle_antisym. 2:{ induction lf as [| r lf Hreclf]. { simpl; right; assumption. } assert (H8 : In a (cons_ORlist (cons r lf) lg)). { elim (RList_P9 (cons r lf) lg a); intros; apply H10; left; elim (RList_P3 (cons r lf) a); intros; apply H12; exists 0%nat; split; [ symmetry ; assumption | simpl; apply Nat.lt_0_succ ]. } apply RList_P5; [ apply RList_P2; assumption | assumption ]. } induction lf as [| r lf Hreclf]. { simpl; right; symmetry ; assumption. } assert (H10 : In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)). { elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10; apply H10; exists 0%nat; split; [ reflexivity | rewrite RList_P11; simpl; apply Nat.lt_0_succ ]. } elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H12 _; assert (H13 := H12 H10); elim H13; intro. { elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H11 _; assert (H14 := H11 H8); elim H14; intros; elim H15; clear H15; intros; rewrite H15; rewrite <- H6; elim (RList_P6 (cons r lf)); intros; apply H17; [ assumption | apply Nat.le_0_l | assumption ]. } elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H11 _; assert (H14 := H11 H8); elim H14; intros; elim H15; clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg); intros; apply H17; [ assumption | apply Nat.le_0_l | assumption ]. - rewrite Hyp_max; apply Rle_antisym. 2:{ induction lf as [| r lf Hreclf]. { simpl; right; symmetry ; assumption. } assert (H8 : In b (cons_ORlist (cons r lf) lg)). { elim (RList_P9 (cons r lf) lg b); intros; apply H10; left; elim (RList_P3 (cons r lf) b); intros; apply H12; exists (pred (length (cons r lf))); split; [ symmetry ; assumption | simpl; apply Nat.lt_succ_diag_r ]. } apply RList_P7; [ apply RList_P2; assumption | assumption ]. } induction lf as [| r lf Hreclf]. { simpl; right; assumption. } assert (H8 : In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (length (cons_ORlist (cons r lf) lg)))) (cons_ORlist (cons r lf) lg)). { elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (length (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; exists (pred (length (cons_ORlist (cons r lf) lg))); split; [ reflexivity | rewrite RList_P11; simpl; apply Nat.lt_succ_diag_r ]. } elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (length (cons_ORlist (cons r lf) lg))))); intros H10 _. assert (H11 := H10 H8); elim H11; intro. { elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (length (cons_ORlist (cons r lf) lg))))); intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros; rewrite H15; rewrite <- H5; elim (RList_P6 (cons r lf)); intros; apply H17; [ assumption | simpl; simpl in H14; apply Nat.lt_succ_r; assumption | simpl; apply Nat.lt_succ_diag_r ]. } elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (length (cons_ORlist (cons r lf) lg))))); intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros. rewrite H15; assert (H17 : length lg = S (pred (length lg))). { symmetry; apply Nat.lt_succ_pred with 0%nat. apply Nat.neq_0_lt_0; red; intro; rewrite H17 in H16; elim (Nat.nlt_0_r _ H16). } rewrite <- H0; elim (RList_P6 lg); intros; apply H18; [ assumption | rewrite H17 in H16; apply Nat.lt_succ_r; assumption | apply Nat.lt_pred_l; rewrite H17; intros Heq; discriminate ]. - apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl; apply Nat.lt_0_succ. - intros; unfold constant_D_eq, open_interval; intros; cut (exists l : R, constant_D_eq f (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l). + intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : exists r : R, (exists r0 : list R, cons_ORlist lf lg = cons r r0)). { apply RList_P19; red; intro; rewrite H13 in H8; elim (Nat.nlt_0_r _ H8). } elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF; rewrite RList_P12. 2:{ rewrite RList_P14; rewrite Hyp_cons in H8; simpl in H8; apply H8. } change (f x = f (pos_Rl (mid_Rlist (cons r r0) r) (S i))); rewrite <- Hyp_cons; rewrite RList_P13. 2:{ apply H8. } assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro. 2:{ elim H10; intros; rewrite H14 in H15; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H16 H15)). } unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10); assert (H15 : pos_Rl (cons_ORlist lf lg) i < (pos_Rl (cons_ORlist lf lg) i + pos_Rl (cons_ORlist lf lg) (S i)) / 2 < pos_Rl (cons_ORlist lf lg) (S i)) by lra. rewrite (H11 _ H15); reflexivity. + assert (H11 : a < b). { apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i). 2:apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). - rewrite <- H6; rewrite <- (RList_P15 lf lg). + elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. * apply RList_P2; assumption. * apply Nat.le_0_l. * apply Nat.lt_trans with (pred (length (cons_ORlist lf lg))); [ assumption | apply Nat.lt_pred_l; apply Nat.neq_0_lt_0; apply Nat.neq_0_lt_0; red; intro; rewrite H13 in H8; elim (Nat.nlt_0_r _ H8) ]. + assumption. + assumption. + rewrite H1; assumption. - elim H10; intros; apply Rlt_trans with x; assumption. - rewrite <- H5; rewrite <- (RList_P16 lf lg); try assumption. { elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. - apply RList_P2; assumption. - apply Nat.lt_succ_r; apply -> Nat.succ_lt_mono; assumption. - apply Nat.lt_pred_l; red; intro; rewrite H13 in H8; elim (Nat.nlt_0_r _ H8). } rewrite H0; assumption. } set (I := fun j:nat => pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < length lf)%nat); assert (H12 : Nbound I). { unfold Nbound; exists (length lf); intros; unfold I in H12; elim H12; intros; apply Nat.lt_le_incl; assumption. } assert (H13 : exists n : nat, I n). { exists 0%nat; unfold I; split. 2:{ apply Nat.neq_0_lt_0; red; intro; rewrite H13 in H5; rewrite <- H6 in H11; rewrite <- H5 in H11; elim (Rlt_irrefl _ H11). } apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). { right; symmetry . apply RList_P15; try assumption; rewrite H1; assumption. } elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13. - apply RList_P2; assumption. - apply Nat.le_0_l. - lia. } assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14; exists (pos_Rl lf0 x0); unfold constant_D_eq, open_interval; intros; assert (H16 := H9 x0); assert (H17 : (x0 < pred (length lf))%nat). { elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros; apply Nat.succ_lt_mono; replace (S (pred (length lf))) with (length lf). { inversion H18. 2: apply -> Nat.succ_lt_mono; assumption. assert (x0 = pred (length lf)). { rewrite <- H20; reflexivity. } rewrite H19 in H14; rewrite H5 in H14; cut (pos_Rl (cons_ORlist lf lg) i < b). - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)). - apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). { elim H10; intros; apply Rlt_trans with x; assumption. } rewrite <- H5; apply Rle_trans with (pos_Rl (cons_ORlist lf lg) (pred (length (cons_ORlist lf lg)))). + elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. * apply RList_P2; assumption. * apply Nat.lt_succ_r; apply -> Nat.succ_lt_mono; assumption. * apply Nat.lt_pred_l; red; intro; rewrite H23 in H8; elim (Nat.nlt_0_r _ H8). + right; apply RList_P16; try assumption; rewrite H0; assumption. } symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H19 in H18; elim (Nat.nlt_0_r _ H18). } assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18; rewrite (H18 x1). { reflexivity. } elim H15; clear H15; intros; elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros; split. { apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption. } apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). { assumption. } assert (H22 : (S x0 < length lf)%nat) by lia. elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0. * assert (H23 : (S x0 <= x0)%nat). { apply H20; unfold I; split; assumption. } elim (Nat.nle_succ_diag_l _ H23). * assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)) by auto with real. clear a0; apply RList_P17; try assumption. { apply RList_P2; assumption. } elim (RList_P9 lf lg (pos_Rl lf (S x0))); intros; apply H25; left; elim (RList_P3 lf (pos_Rl lf (S x0))); intros; apply H27; exists (S x0); split; [ reflexivity | apply H22 ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra