proposition: Lemma StepFun_P38 : forall (l:list R) (a b:R) (f:R -> R), ordered_Rlist l -> pos_Rl l 0 = a -> pos_Rl l (pred (length l)) = b -> { g:StepFun a b | g b = f b /\ (forall i:nat, (i < pred (length l))%nat -> constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) (f (pos_Rl l i))) }.
proof: Proof. intros l a b f; generalize a; clear a; induction l as [|r l IHl]. { intros a H H0 H1; simpl in H0; simpl in H1; exists (mkStepFun (StepFun_P4 a b (f b))); split. { reflexivity. } intros; elim (Nat.nlt_0_r _ H2). } intros; destruct l as [| r1 l]. { simpl in H1; simpl in H0; exists (mkStepFun (StepFun_P4 a b (f b))); split. { reflexivity. } intros i H2; elim (Nat.nlt_0_r _ H2). } intros; assert (H2 : ordered_Rlist (cons r1 l)). { apply RList_P4 with r; assumption. } assert (H3 : pos_Rl (cons r1 l) 0 = r1). { reflexivity. } assert (H4 : pos_Rl (cons r1 l) (pred (length (cons r1 l))) = b). { rewrite <- H1; reflexivity. } elim (IHl r1 H2 H3 H4); intros g [H5 H6]. set (g' := fun x:R => match Rle_dec r1 x with | left _ => g x | right _ => f a end). assert (H7 : r1 <= b). { rewrite <- H4; apply RList_P7; [ assumption | left; reflexivity ]. } assert (H8 : IsStepFun g' a b). { unfold IsStepFun; assert (H8 := pre g); unfold IsStepFun in H8; elim H8; intros lg H9; unfold is_subdivision in H9; elim H9; clear H9; intros lg2 H9; split with (cons a lg); unfold is_subdivision; split with (cons (f a) lg2); unfold adapted_couple in H9; decompose [and] H9; clear H9; unfold adapted_couple; repeat split. - unfold ordered_Rlist; intros; simpl in H9; induction i as [| i Hreci]. { simpl; rewrite H12; replace (Rmin r1 b) with r1. { simpl in H0; rewrite <- H0; apply (H 0%nat); simpl; apply Nat.lt_0_succ. } unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. } apply (H10 i); apply Nat.succ_lt_mono. replace (S (pred (length lg))) with (length lg). { apply H9. } symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; intro; rewrite H14 in H9; elim (Nat.nlt_0_r _ H9). - simpl; assert (H14 : a <= b). { rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. } unfold Rmin; decide (Rle_dec a b) with H14; reflexivity. - assert (H14 : a <= b). { rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. } replace (Rmax a b) with (Rmax r1 b). { rewrite <- H11; induction lg as [| r0 lg Hreclg]. { simpl in H13; discriminate. } reflexivity. } unfold Rmax; decide (Rle_dec a b) with H14; decide (Rle_dec r1 b) with H7; reflexivity. - simpl; rewrite H13; reflexivity. - intros; simpl in H9; induction i as [| i Hreci]. { unfold constant_D_eq, open_interval; simpl; intros; assert (H16 : Rmin r1 b = r1). { unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. } rewrite H16 in H12; rewrite H12 in H14; elim H14; clear H14; intros _ H14; unfold g'; case (Rle_dec r1 x); intro r3. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H14)). } reflexivity. } change (constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i))) (pos_Rl lg2 i)); clear Hreci; assert (H16 := H15 i); assert (H17 : (i < pred (length lg))%nat). { apply Nat.succ_lt_mono. replace (S (pred (length lg))) with (length lg). { assumption. } symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H14 in H9; elim (Nat.nlt_0_r _ H9). } assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18; unfold constant_D_eq, open_interval; intros; assert (H19 := H18 _ H14); rewrite <- H19; unfold g'; case (Rle_dec r1 x) as [|[]]. { reflexivity. } replace r1 with (Rmin r1 b). { rewrite <- H12; elim H14; clear H14; intros H14 _; left; apply Rle_lt_trans with (pos_Rl lg i); try assumption. apply RList_P5. { assumption. } elim (RList_P3 lg (pos_Rl lg i)); intros; apply H21; exists i; split. { reflexivity. } apply Nat.lt_trans with (pred (length lg)); try assumption. apply Nat.lt_pred_l; red; intro; rewrite H22 in H17; elim (Nat.nlt_0_r _ H17). } unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. } exists (mkStepFun H8); split. { simpl; unfold g'; decide (Rle_dec r1 b) with H7; assumption. } intros; simpl in H9; induction i as [| i Hreci]. { unfold constant_D_eq, co_interval; simpl; intros; simpl in H0; rewrite H0; elim H10; clear H10; intros; unfold g'; case (Rle_dec r1 x); intro r3. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H11)). } reflexivity. } clear Hreci; change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i))) (f (pos_Rl (cons r1 l) i))); assert (H10 := H6 i); assert (H11 : (i < pred (length (cons r1 l)))%nat). { simpl; apply Nat.succ_lt_mono; assumption. } assert (H12 := H10 H11); unfold constant_D_eq, co_interval in H12; unfold constant_D_eq, co_interval; intros; rewrite <- (H12 _ H13); simpl; unfold g'; case (Rle_dec r1 x) as [|[]]. { reflexivity. } elim H13; clear H13; intros; apply Rle_trans with (pos_Rl (cons r1 l) i); try assumption; change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i); elim (RList_P6 (cons r1 l)); intros; apply H15; [ assumption | apply Nat.le_0_l | simpl; apply Nat.lt_trans with (length l); [ apply Nat.succ_lt_mono; assumption | apply Nat.lt_succ_diag_r ] ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra