proposition: Lemma StepFun_P10 : forall (f:R -> R) (l lf:list R) (a b:R), a <= b -> adapted_couple f a b l lf -> exists l' : list R, (exists lf' : list R, adapted_couple_opt f a b l' lf').
proof: Proof. induction l as [ | r r0 H]. { intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4; discriminate. } intros; case (Req_dec a b); intro. { exists (cons a nil); exists nil; unfold adapted_couple_opt; unfold adapted_couple; unfold ordered_Rlist; repeat split; try (intros; simpl in H3; elim (Nat.nlt_0_r _ H3)). 1,2:simpl; rewrite <- H2; unfold Rmin,Rmax; case (Rle_dec a a); intro; reflexivity. } elim (RList_P20 _ (StepFun_P9 H1 H2)); intros t1 [t2 [t3 H3]]; induction lf as [| r1 lf Hreclf]. { unfold adapted_couple in H1; decompose [and] H1; rewrite H3 in H7; simpl in H7; discriminate. } clear Hreclf; assert (H4 : adapted_couple f t2 b r0 lf). { rewrite H3 in H1; assert (H4 := RList_P21 _ _ H3); simpl in H4; rewrite H4; eapply StepFun_P7; [ apply H0 | apply H1 ]. } assert (t2 <= b). { rewrite H3 in H1; clear H4; unfold adapted_couple in H1; decompose [and] H1; clear H1; clear H H7 H9; cut (Rmax a b = b); [ intro; rewrite H in H5; rewrite <- H5; apply RList_P7; [ assumption | simpl; right; left; reflexivity ] | unfold Rmax; decide (Rle_dec a b) with H0; reflexivity ]. } assert (H6 := H _ _ _ H5 H4); case (Req_dec t1 t2); intro Hyp_eq. { replace a with t2. { apply H6. } rewrite <- Hyp_eq; rewrite H3 in H1; unfold adapted_couple in H1; decompose [and] H1; clear H1; simpl in H9; rewrite H9; unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. } elim H6; clear H6; intros l' [lf' H6]; case (Req_dec t2 b); intro. { exists (cons a (cons b nil)); exists (cons r1 nil); unfold adapted_couple_opt; unfold adapted_couple; repeat split. - unfold ordered_Rlist; intros; simpl in H8; inversion H8; [ simpl; assumption | elim (Nat.nle_succ_0 _ H10) ]. - simpl; unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. - simpl; unfold Rmax; decide (Rle_dec a b) with H0; reflexivity. - intros; simpl in H8; inversion H8. + unfold constant_D_eq, open_interval; intros; simpl; simpl in H9; rewrite H3 in H1; unfold adapted_couple in H1; decompose [and] H1; apply (H16 0%nat). * simpl; apply Nat.lt_0_succ. * unfold open_interval; simpl; rewrite H7; simpl in H13; rewrite H13; unfold Rmin; decide (Rle_dec a b) with H0; assumption. + elim (Nat.nle_succ_0 _ H10). - intros; simpl in H8; elim (Nat.nlt_0_r _ H8). - intros; simpl in H8; inversion H8; [ simpl; assumption | elim (Nat.nle_succ_0 _ H10) ]. } assert (Hyp_min : Rmin t2 b = t2) by apply Rmin_left,H5. unfold adapted_couple in H6; elim H6; clear H6; intros; elim (RList_P20 _ (StepFun_P9 H6 H7)); intros s1 [s2 [s3 H9]]; induction lf' as [| r2 lf' Hreclf']. { unfold adapted_couple in H6; decompose [and] H6; rewrite H9 in H13; simpl in H13; discriminate. } clear Hreclf'; case (Req_dec r1 r2); intro. 1:case (Req_dec (f t2) r1); intro. - exists (cons t1 (cons s2 s3)); exists (cons r1 lf'); rewrite H3 in H1; rewrite H9 in H6; unfold adapted_couple in H6, H1; decompose [and] H1; decompose [and] H6; clear H1 H6; unfold adapted_couple_opt; unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H1; induction i as [| i Hreci]. { simpl; apply Rle_trans with s1. { replace s1 with t2. { apply (H12 0%nat). simpl; apply Nat.lt_0_succ. } simpl in H19; rewrite H19; symmetry ; apply Hyp_min. } apply (H16 0%nat); simpl; apply Nat.lt_0_succ. } change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)); apply (H16 (S i)); simpl; assumption. + simpl; simpl in H14; rewrite H14; reflexivity. + simpl; simpl in H18; rewrite H18; unfold Rmax; decide (Rle_dec a b) with H0; decide (Rle_dec t2 b) with H5; reflexivity. + simpl; simpl in H20; apply H20. + intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. { simpl; simpl in H6; destruct (total_order_T x t2) as [[Hlt|Heq]|Hgt]. - apply (H17 0%nat); [ simpl; apply Nat.lt_0_succ | unfold open_interval; simpl; elim H6; intros; split; assumption ]. - rewrite Heq; assumption. - rewrite H10; apply (H22 0%nat); [ simpl; apply Nat.lt_0_succ | unfold open_interval; simpl; replace s1 with t2; [ elim H6; intros; split; assumption | simpl in H19; rewrite H19; rewrite Hyp_min; reflexivity ] ]. } simpl; simpl in H6; apply (H22 (S i)); [ simpl; assumption | unfold open_interval; simpl; apply H6 ]. + intros; simpl in H1; rewrite H10; change (pos_Rl (cons r2 lf') i <> pos_Rl (cons r2 lf') (S i) \/ f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r2 lf') i) ; rewrite <- H9; elim H8; intros; apply H6; simpl; apply H1. + intros; induction i as [| i Hreci]. { simpl; red; intro; elim Hyp_eq; apply Rle_antisym. - apply (H12 0%nat); simpl; apply Nat.lt_0_succ. - rewrite <- Hyp_min; rewrite H6; simpl in H19; rewrite <- H19; apply (H16 0%nat); simpl; apply Nat.lt_0_succ. } elim H8; intros; rewrite H9 in H21; apply (H21 (S i)); simpl; simpl in H1; apply H1. - exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6; rewrite H3 in H1; unfold adapted_couple in H1, H6; decompose [and] H6; decompose [and] H1; clear H6 H1; unfold adapted_couple_opt; unfold adapted_couple; repeat split. + rewrite H9; unfold ordered_Rlist; intros; simpl in H1; induction i as [| i Hreci]. { simpl; replace s1 with t2. { apply (H16 0%nat); simpl; apply Nat.lt_0_succ. } simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. } change (pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i)) ; apply (H12 i); simpl; apply Nat.succ_lt_mono; assumption. + simpl; simpl in H19; apply H19. + rewrite H9; simpl; simpl in H13; rewrite H13; unfold Rmax; decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity. + rewrite H9; simpl; simpl in H15; rewrite H15; reflexivity. + intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. { simpl; rewrite H9 in H6; simpl in H6; apply (H22 0%nat). { simpl; apply Nat.lt_0_succ. } unfold open_interval; simpl. replace t2 with s1. { assumption. } simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. } change (f x = pos_Rl (cons r2 lf') i); clear Hreci; apply (H17 i). { simpl; rewrite H9 in H1; simpl in H1; apply Nat.succ_lt_mono; apply H1. } rewrite H9 in H6; unfold open_interval; apply H6. + intros; simpl in H1; induction i as [| i Hreci]. { simpl; rewrite H9; right; simpl; replace s1 with t2. { assumption. } simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. } elim H8; intros; apply (H6 i). simpl; apply Nat.succ_lt_mono; apply H1. + intros; rewrite H9; induction i as [| i Hreci]. { simpl; red; intro; elim Hyp_eq; apply Rle_antisym. { apply (H16 0%nat); simpl; apply Nat.lt_0_succ. } rewrite <- Hyp_min; rewrite H6; simpl in H14; rewrite <- H14; right; reflexivity. } elim H8; intros; rewrite <- H9; apply (H21 i); rewrite H9; rewrite H9 in H1; simpl; simpl in H1; apply Nat.succ_lt_mono; apply H1. - exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6; rewrite H3 in H1; unfold adapted_couple in H1, H6; decompose [and] H6; decompose [and] H1; clear H6 H1; unfold adapted_couple_opt; unfold adapted_couple; repeat split. + rewrite H9; unfold ordered_Rlist; intros; simpl in H1; induction i as [| i Hreci]. { simpl; replace s1 with t2. { apply (H15 0%nat); simpl; apply Nat.lt_0_succ. } simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity. } change (pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i)) ; apply (H11 i); simpl; apply Nat.succ_lt_mono; assumption. + simpl; simpl in H18; apply H18. + rewrite H9; simpl; simpl in H12; rewrite H12; unfold Rmax; decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity. + rewrite H9; simpl; simpl in H14; rewrite H14; reflexivity. + intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. { simpl; rewrite H9 in H6; simpl in H6; apply (H21 0%nat). { simpl; apply Nat.lt_0_succ. } unfold open_interval; simpl; replace t2 with s1. { assumption. } simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity. } change (f x = pos_Rl (cons r2 lf') i); clear Hreci; apply (H16 i). { simpl; rewrite H9 in H1; simpl in H1; apply Nat.succ_lt_mono; apply H1. } rewrite H9 in H6; unfold open_interval; apply H6. + intros; simpl in H1; induction i as [| i Hreci]. { simpl; left; assumption. } elim H8; intros; apply (H6 i). simpl; apply Nat.succ_lt_mono; apply H1. + intros; rewrite H9; induction i as [| i Hreci]. { simpl; red; intro; elim Hyp_eq; apply Rle_antisym. { apply (H15 0%nat); simpl; apply Nat.lt_0_succ. } rewrite <- Hyp_min; rewrite H6; simpl in H13; rewrite <- H13; right; reflexivity. } elim H8; intros; rewrite <- H9; apply (H20 i); rewrite H9; rewrite H9 in H1; simpl; simpl in H1; apply Nat.succ_lt_mono; apply H1. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra