proposition: Lemma StepFun_P14 : forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), a <= b -> adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2.
proof: Proof. induction l1 as [ | r r0 H0]. { intros l2 lf1 lf2 a b Hyp H H0; unfold adapted_couple in H; decompose [and] H; clear H H0 H2 H3 H1 H6; simpl in H4; discriminate. } induction r0 as [|r1 r2 H]. { intros; case (Req_dec a b); intro. - unfold adapted_couple_opt in H2; elim H2; intros; rewrite (StepFun_P8 H4 H3); rewrite (StepFun_P8 H1 H3); reflexivity. - assert (H4 := StepFun_P9 H1 H3); simpl in H4; elim (Nat.nle_succ_0 _ (le_S_n _ _ H4)). } intros; clear H; unfold adapted_couple_opt in H3; elim H3; clear H3; intros; case (Req_dec a b); intro. { rewrite (StepFun_P8 H2 H4); rewrite (StepFun_P8 H H4); reflexivity. } assert (Hyp_min : Rmin a b = a). { unfold Rmin; decide (Rle_dec a b) with H1; reflexivity. } assert (Hyp_max : Rmax a b = b). { unfold Rmax; decide (Rle_dec a b) with H1; reflexivity. } elim (RList_P20 _ (StepFun_P9 H H4)); intros s1 [s2 [s3 H5]]; rewrite H5 in H; rewrite H5; induction lf1 as [| r3 lf1 Hreclf1]. { unfold adapted_couple in H2; decompose [and] H2; clear H H2 H4 H5 H3 H6 H8 H7 H11; simpl in H9; discriminate. } clear Hreclf1; induction lf2 as [| r4 lf2 Hreclf2]. { unfold adapted_couple in H; decompose [and] H; clear H H2 H4 H5 H3 H6 H8 H7 H11; simpl in H9; discriminate. } clear Hreclf2; assert (H6 : r = s1). { unfold adapted_couple in H, H2; decompose [and] H; decompose [and] H2; clear H H2; simpl in H13; simpl in H8; rewrite H13; rewrite H8; reflexivity. } assert (H7 : r3 = r4 \/ r = r1). { case (Req_dec r r1); intro. { right; assumption. } left; assert (r1 <= s2). { eapply StepFun_P13. - apply H4. - apply H2. - unfold adapted_couple_opt; split. + apply H. + rewrite H5 in H3; apply H3. } unfold adapted_couple in H2, H; decompose [and] H; decompose [and] H2; clear H H2; set (x := (r + r1) / 2); assert (H18 := H14 0%nat); assert (H20 := H19 0%nat); unfold constant_D_eq, open_interval in H18, H20; simpl in H18; simpl in H20; rewrite <- (H18 (Nat.lt_0_succ _) x). { rewrite <- (H20 (Nat.lt_0_succ _) x). { reflexivity. } assert (H21 := H13 0%nat (Nat.lt_0_succ _)); simpl in H21; elim H21; intro; [ idtac | elim H7; assumption ]; unfold x; lra. } rewrite <- H6; assert (H21 := H13 0%nat (Nat.lt_0_succ _)); simpl in H21; elim H21; intro; [ idtac | elim H7; assumption ]; unfold x; lra. } assert (H8 : r1 <= s2). { eapply StepFun_P13. - apply H4. - apply H2. - unfold adapted_couple_opt; split. + apply H. + rewrite H5 in H3; apply H3. } elim H7; intro. 2:{ simpl; rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rmult_0_r; rewrite Rplus_0_l; change (Int_SF lf1 (cons r1 r2) = Int_SF (cons r4 lf2) (cons s1 (cons s2 s3))) ; eapply H0. - apply H1. - assert (H10 : r = a). + unfold adapted_couple in H2; decompose [and] H2; clear H2; simpl in H12; rewrite H12; apply Hyp_min. + rewrite <- H9; rewrite H10; apply StepFun_P7 with a r r3; [ apply H1 | pattern a at 2; rewrite <- H10; pattern r at 2; rewrite H9; apply H2 ]. - rewrite H5 in H3; unfold adapted_couple_opt; split; assumption. } simpl; elim H8; intro. { replace (r4 * (s2 - s1)) with (r3 * (r1 - r) + r3 * (s2 - r1)); [ idtac | rewrite H9; rewrite H6; ring ]. rewrite Rplus_assoc; apply Rplus_eq_compat_l; change (Int_SF lf1 (cons r1 r2) = Int_SF (cons r3 lf2) (cons r1 (cons s2 s3))) ; apply H0 with r1 b. { unfold adapted_couple in H2; decompose [and] H2; clear H2; replace b with (Rmax a b); rewrite <- H12; apply RList_P7; [ assumption | simpl; right; left; reflexivity ]. } { eapply StepFun_P7. - apply H1. - apply H2. } unfold adapted_couple_opt; split. { apply StepFun_P7 with a a r3. { apply H1. } unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H; clear H H2; assert (H20 : r = a). { simpl in H13; rewrite H13; apply Hyp_min. } unfold adapted_couple; repeat split. - unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. { simpl; rewrite <- H20; apply (H11 0%nat). simpl; apply Nat.lt_0_succ. } induction i as [| i Hreci0]. { simpl; assumption. } change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)); apply (H15 (S i)); simpl; apply Nat.succ_lt_mono; assumption. - simpl; symmetry ; apply Hyp_min. - rewrite <- H17; reflexivity. - simpl in H19; simpl; rewrite H19; reflexivity. - intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. { simpl; apply (H16 0%nat). { simpl; apply Nat.lt_0_succ. } simpl in H2; rewrite <- H20 in H2; unfold open_interval; simpl; apply H2. } clear Hreci; induction i as [| i Hreci]. { simpl; simpl in H2; rewrite H9; apply (H21 0%nat). { simpl; apply Nat.lt_0_succ. } unfold open_interval; simpl; elim H2; intros; split. { apply Rle_lt_trans with r1; try assumption; rewrite <- H6; apply (H11 0%nat); simpl; apply Nat.lt_0_succ. } assumption. } clear Hreci; simpl; apply (H21 (S i)). { simpl; apply Nat.succ_lt_mono; assumption. } unfold open_interval; apply H2. } elim H3; clear H3; intros; split. { rewrite H9; change (forall i:nat, (i < pred (length (cons r4 lf2)))%nat -> pos_Rl (cons r4 lf2) i <> pos_Rl (cons r4 lf2) (S i) \/ f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r4 lf2) i) ; rewrite <- H5; apply H3. } rewrite H5 in H11; intros; simpl in H12; induction i as [| i Hreci]. { simpl; red; intro; rewrite H13 in H10; elim (Rlt_irrefl _ H10). } clear Hreci; apply (H11 (S i)); simpl; apply H12. } rewrite H9; rewrite H10; rewrite H6; apply Rplus_eq_compat_l; rewrite <- H10; apply H0 with r1 b. { unfold adapted_couple in H2; decompose [and] H2; clear H2; replace b with (Rmax a b). rewrite <- H12; apply RList_P7; [ assumption | simpl; right; left; reflexivity ]. } { eapply StepFun_P7. - apply H1. - apply H2. } unfold adapted_couple_opt; split. { apply StepFun_P7 with a a r3. { apply H1. } unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H; clear H H2; assert (H20 : r = a). { simpl in H13; rewrite H13; apply Hyp_min. } unfold adapted_couple; repeat split. - unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. { simpl; rewrite <- H20; apply (H11 0%nat); simpl; apply Nat.lt_0_succ. } rewrite H10; apply (H15 (S i)); simpl; assumption. - simpl; symmetry ; apply Hyp_min. - rewrite <- H17; rewrite H10; reflexivity. - simpl in H19; simpl; apply H19. - intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. { simpl; apply (H16 0%nat). { simpl; apply Nat.lt_0_succ. } simpl in H2; rewrite <- H20 in H2; unfold open_interval; simpl; apply H2. } clear Hreci; simpl; apply (H21 (S i)). { simpl; assumption. } rewrite <- H10; unfold open_interval; apply H2. } elim H3; clear H3; intros; split. - rewrite H5 in H3; intros; apply (H3 (S i)). simpl; replace (length lf2) with (S (pred (length lf2))). { apply -> Nat.succ_lt_mono; apply H12. } apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H13 in H12; elim (Nat.nlt_0_r _ H12). - intros; simpl in H12; rewrite H10; rewrite H5 in H11; apply (H11 (S i)); simpl; apply -> Nat.succ_lt_mono; apply H12. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra