diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 14:07:19 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 14:07:19 +0000 |
| commit | d9117de3db059a48e64eda154fa48cf16f8f83c8 (patch) | |
| tree | ff50acf5ab5803dbf5b37c18a59052f6482bf8f1 | |
| parent | 62638f9e6dc361ce3ad72bfc1e700f4794729a19 (diff) | |
Renommages dans RList
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3580 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/RList.v | 81 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt.v | 32 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 144 |
3 files changed, 128 insertions, 129 deletions
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 7f8a92d08..82c920621 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -20,15 +20,14 @@ Cases l of | nil => False | (cons a l') => ``x==a``\/(In x l') end. -Fixpoint longueur [l:Rlist] : nat := +Fixpoint Rlength [l:Rlist] : nat := Cases l of | nil => O -| (cons a l') => (S (longueur l')) end. +| (cons a l') => (S (Rlength l')) end. -(* Cette fonction renvoie le maximum des éléments d'une liste non vide *) Fixpoint MaxRlist [l:Rlist] : R := Cases l of - | nil => R0 (* valeur de retour si la liste de départ est vide *) + | nil => R0 | (cons a l1) => Cases l1 of | nil => a @@ -38,7 +37,7 @@ end. Fixpoint MinRlist [l:Rlist] : R := Cases l of - | nil => R1 (* valeur de retour si la liste de départ est vide *) + | nil => R1 | (cons a l1) => Cases l1 of | nil => a @@ -142,11 +141,11 @@ Fixpoint pos_Rl [l:Rlist] : nat->R := end end. -Lemma pos_Rl_P1 : (l:Rlist;a:R) (lt O (longueur l)) -> (pos_Rl (cons a l) (longueur l))==(pos_Rl l (pred (longueur l))). -Intros; Induction l; [Elim (lt_n_O ? H) | Simpl; Case (longueur l); [Reflexivity | Intro; Reflexivity]]. +Lemma pos_Rl_P1 : (l:Rlist;a:R) (lt O (Rlength l)) -> (pos_Rl (cons a l) (Rlength l))==(pos_Rl l (pred (Rlength l))). +Intros; Induction l; [Elim (lt_n_O ? H) | Simpl; Case (Rlength l); [Reflexivity | Intro; Reflexivity]]. Qed. -Lemma pos_Rl_P2 : (l:Rlist;x:R) (In x l)<->(EX i:nat | (lt i (longueur l))/\x==(pos_Rl l i)). +Lemma pos_Rl_P2 : (l:Rlist;x:R) (In x l)<->(EX i:nat | (lt i (Rlength l))/\x==(pos_Rl l i)). Intros; Induction l. Split; Intro; [Elim H | Elim H; Intros; Elim H0; Intros; Elim (lt_n_O ? H1)]. Split; Intro. @@ -160,7 +159,7 @@ Symmetry; Apply S_pred with O; Assumption. Exists (pred x0); Split; [Simpl in H1; Apply lt_S_n; Rewrite H5; Assumption | Rewrite <- H5 in H2; Simpl in H2; Assumption]. Qed. -Lemma Rlist_P1 : (l:Rlist;P:R->R->Prop) ((x:R)(In x l)->(EXT y:R | (P x y))) -> (EXT l':Rlist | (longueur l)=(longueur l')/\(i:nat) (lt i (longueur l))->(P (pos_Rl l i) (pos_Rl l' i))). +Lemma Rlist_P1 : (l:Rlist;P:R->R->Prop) ((x:R)(In x l)->(EXT y:R | (P x y))) -> (EXT l':Rlist | (Rlength l)=(Rlength l')/\(i:nat) (lt i (Rlength l))->(P (pos_Rl l i) (pos_Rl l' i))). Intros; Induction l. Exists nil; Intros; Split; [Reflexivity | Intros; Simpl in H0; Elim (lt_n_O ? H0)]. Assert H0 : (In r (cons r l)). @@ -176,7 +175,7 @@ Apply S_pred with O; Assumption. Rewrite H8; Simpl; Apply H6; Simpl in H7; Apply lt_S_n; Rewrite <- H8; Assumption. Qed. -Definition ordered_Rlist [l:Rlist] : Prop := (i:nat) (lt i (pred (longueur l))) -> (Rle (pos_Rl l i) (pos_Rl l (S i))). +Definition ordered_Rlist [l:Rlist] : Prop := (i:nat) (lt i (pred (Rlength l))) -> (Rle (pos_Rl l i) (pos_Rl l (S i))). Fixpoint insert [l:Rlist] : R->Rlist := [x:R] Cases l of @@ -232,12 +231,12 @@ Intros; Induction l. Simpl; Unfold ordered_Rlist; Intros; Simpl in H0; Elim (lt_n_O ? H0). Simpl; Case (total_order_Rle r a); Intro. Assert H1 : (ordered_Rlist l). -Unfold ordered_Rlist; Unfold ordered_Rlist in H; Intros; Assert H1 : (lt (S i) (pred (longueur (cons r l)))); [Simpl; Replace (longueur l) with (S (pred (longueur l))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Simpl in H0; Elim (lt_n_O ? H0)] | Apply (H ? H1)]. +Unfold ordered_Rlist; Unfold ordered_Rlist in H; Intros; Assert H1 : (lt (S i) (pred (Rlength (cons r l)))); [Simpl; Replace (Rlength l) with (S (pred (Rlength l))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Simpl in H0; Elim (lt_n_O ? H0)] | Apply (H ? H1)]. Assert H2 := (Hrecl H1); Unfold ordered_Rlist; Intros; Induction i. Simpl; Assert H3 := (RList_P0 l a); Elim H3; Intro. Rewrite H4; Assumption. Induction l; [Simpl; Assumption | Rewrite H4; Apply (H O); Simpl; Apply lt_O_Sn]. -Simpl; Apply H2; Simpl in H0; Apply lt_S_n; Replace (S (pred (longueur (insert l a)))) with (longueur (insert l a)); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H3 in H0; Elim (lt_n_O ? H0)]. +Simpl; Apply H2; Simpl in H0; Apply lt_S_n; Replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a)); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H3 in H0; Elim (lt_n_O ? H0)]. Unfold ordered_Rlist; Intros; Induction i; [Simpl; Auto with real | Change ``(pos_Rl (cons r l) i)<=(pos_Rl (cons r l) (S i))``; Apply H; Simpl in H0; Simpl; Apply (lt_S_n ? ? H0)]. Qed. @@ -245,7 +244,7 @@ Lemma RList_P2 : (l1,l2:Rlist) (ordered_Rlist l2) ->(ordered_Rlist (cons_ORlist Induction l1; [Intros; Simpl; Apply H | Intros; Simpl; Apply H; Apply RList_P1; Assumption]. Qed. -Lemma RList_P3 : (l:Rlist;x:R) (In x l) <-> (EX i:nat | x==(pos_Rl l i)/\(lt i (longueur l))). +Lemma RList_P3 : (l:Rlist;x:R) (In x l) <-> (EX i:nat | x==(pos_Rl l i)/\(lt i (Rlength l))). Intros; Split; Intro; Induction l. Elim H. Elim H; Intro; [Exists O; Split; [Apply H0 | Simpl; Apply lt_O_Sn] | Elim (Hrecl H0); Intros; Elim H1; Clear H1; Intros; Exists (S x0); Split; [Apply H1 | Simpl; Apply lt_n_S; Assumption]]. @@ -254,14 +253,14 @@ Simpl; Elim H; Intros; Elim H0; Clear H0; Intros; Induction x0; [Left; Apply H0 Qed. Lemma RList_P4 : (l1:Rlist;a:R) (ordered_Rlist (cons a l1)) -> (ordered_Rlist l1). -Intros; Unfold ordered_Rlist; Intros; Apply (H (S i)); Simpl; Replace (longueur l1) with (S (pred (longueur l1))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Elim (lt_n_O ? H0)]. +Intros; Unfold ordered_Rlist; Intros; Apply (H (S i)); Simpl; Replace (Rlength l1) with (S (pred (Rlength l1))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Elim (lt_n_O ? H0)]. Qed. Lemma RList_P5 : (l:Rlist;x:R) (ordered_Rlist l) -> (In x l) -> ``(pos_Rl l O)<=x``. Intros; Induction l; [Elim H0 | Simpl; Elim H0; Intro; [Rewrite H1; Right; Reflexivity | Apply Rle_trans with (pos_Rl l O); [Apply (H O); Simpl; Induction l; [Elim H1 | Simpl; Apply lt_O_Sn] | Apply Hrecl; [EApply RList_P4; Apply H | Assumption]]]]. Qed. -Lemma RList_P6 : (l:Rlist) (ordered_Rlist l)<->((i,j:nat)(le i j)->(lt j (longueur l))->``(pos_Rl l i)<=(pos_Rl l j)``). +Lemma RList_P6 : (l:Rlist) (ordered_Rlist l)<->((i,j:nat)(le i j)->(lt j (Rlength l))->``(pos_Rl l i)<=(pos_Rl l j)``). Induction l; Split; Intro. Intros; Right; Reflexivity. Unfold ordered_Rlist; Intros; Simpl in H0; Elim (lt_n_O ? H0). @@ -269,8 +268,8 @@ Intros; Induction i; [Induction j; [Right; Reflexivity | Simpl; Apply Rle_trans Unfold ordered_Rlist; Intros; Apply H0; [Apply le_n_Sn | Simpl; Simpl in H1; Apply lt_n_S; Assumption]. Qed. -Lemma RList_P7 : (l:Rlist;x:R) (ordered_Rlist l) -> (In x l) -> ``x<=(pos_Rl l (pred (longueur l)))``. -Intros; Assert H1 := (RList_P6 l); Elim H1; Intros H2 _; Assert H3 := (H2 H); Clear H1 H2; Assert H1 := (RList_P3 l x); Elim H1; Clear H1; Intros; Assert H4 := (H1 H0); Elim H4; Clear H4; Intros; Elim H4; Clear H4; Intros; Rewrite H4; Assert H6 : (longueur l)=(S (pred (longueur l))). +Lemma RList_P7 : (l:Rlist;x:R) (ordered_Rlist l) -> (In x l) -> ``x<=(pos_Rl l (pred (Rlength l)))``. +Intros; Assert H1 := (RList_P6 l); Elim H1; Intros H2 _; Assert H3 := (H2 H); Clear H1 H2; Assert H1 := (RList_P3 l x); Elim H1; Clear H1; Intros; Assert H4 := (H1 H0); Elim H4; Clear H4; Intros; Elim H4; Clear H4; Intros; Rewrite H4; Assert H6 : (Rlength l)=(S (pred (Rlength l))). Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H6 in H5; Elim (lt_n_O ? H5). Apply H3; [Rewrite H6 in H5; Apply lt_n_Sm_le; Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H7 in H5; Elim (lt_n_O ? H5)]. Qed. @@ -289,19 +288,19 @@ Simpl; Intros; Elim (H (insert l2 r) x); Intros; Assert H3 := (H1 H0); Elim H3; Intro; Simpl; Elim (H (insert l2 r) x); Intros _ H1; Apply H1; Elim H0; Intro; [Elim H2; Intro; [Right; Elim (RList_P8 l2 r x); Intros _ H4; Apply H4; Left; Assumption | Left; Assumption] | Right; Elim (RList_P8 l2 r x); Intros _ H3; Apply H3; Right; Assumption]. Qed. -Lemma RList_P10 : (l:Rlist;a:R) (longueur (insert l a))==(S (longueur l)). +Lemma RList_P10 : (l:Rlist;a:R) (Rlength (insert l a))==(S (Rlength l)). Intros; Induction l; [Reflexivity | Simpl; Case (total_order_Rle r a); Intro; [Simpl; Rewrite Hrecl; Reflexivity | Reflexivity]]. Qed. -Lemma RList_P11 : (l1,l2:Rlist) (longueur (cons_ORlist l1 l2))=(plus (longueur l1) (longueur l2)). +Lemma RList_P11 : (l1,l2:Rlist) (Rlength (cons_ORlist l1 l2))=(plus (Rlength l1) (Rlength l2)). Induction l1; [Intro; Reflexivity | Intros; Simpl; Rewrite (H (insert l2 r)); Rewrite RList_P10; Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring]. Qed. -Lemma RList_P12 : (l:Rlist;i:nat;f:R->R) (lt i (longueur l)) -> (pos_Rl (app_Rlist l f) i)==(f (pos_Rl l i)). +Lemma RList_P12 : (l:Rlist;i:nat;f:R->R) (lt i (Rlength l)) -> (pos_Rl (app_Rlist l f) i)==(f (pos_Rl l i)). Induction l; [Intros; Elim (lt_n_O ? H) | Intros; Induction i; [Reflexivity | Simpl; Apply H; Apply lt_S_n; Apply H0]]. Qed. -Lemma RList_P13 : (l:Rlist;i:nat;a:R) (lt i (pred (longueur l))) -> ``(pos_Rl (mid_Rlist l a) (S i)) == ((pos_Rl l i)+(pos_Rl l (S i)))/2``. +Lemma RList_P13 : (l:Rlist;i:nat;a:R) (lt i (pred (Rlength l))) -> ``(pos_Rl (mid_Rlist l a) (S i)) == ((pos_Rl l i)+(pos_Rl l (S i)))/2``. Induction l. Intros; Simpl in H; Elim (lt_n_O ? H). Induction r0. @@ -311,7 +310,7 @@ Reflexivity. Change ``(pos_Rl (mid_Rlist (cons r1 r2) r) (S i)) == ((pos_Rl (cons r1 r2) i)+(pos_Rl (cons r1 r2) (S i)))/2``; Apply H0; Simpl; Apply lt_S_n; Assumption. Qed. -Lemma RList_P14 : (l:Rlist;a:R) (longueur (mid_Rlist l a))=(longueur l). +Lemma RList_P14 : (l:Rlist;a:R) (Rlength (mid_Rlist l a))=(Rlength l). Induction l; Intros; [Reflexivity | Simpl; Rewrite (H r); Reflexivity]. Qed. @@ -321,27 +320,27 @@ Induction l1; [Simpl; Simpl in H1; Right; Symmetry; Assumption | Elim (RList_P9 Induction l1; [Simpl; Simpl in H1; Right; Assumption | Assert H2 : (In (pos_Rl (cons_ORlist (cons r l1) l2) (0)) (cons_ORlist (cons r l1) l2)); [Elim (RList_P3 (cons_ORlist (cons r l1) l2) (pos_Rl (cons_ORlist (cons r l1) l2) (0))); Intros; Apply H3; Exists O; Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_O_Sn] | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) (0))); Intros; Assert H5 := (H3 H2); Elim H5; Intro; [Apply RList_P5; Assumption | Rewrite H1; Apply RList_P5; Assumption]]]. Qed. -Lemma RList_P16 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> (pos_Rl l1 (pred (longueur l1)))==(pos_Rl l2 (pred (longueur l2))) -> (pos_Rl (cons_ORlist l1 l2) (pred (longueur (cons_ORlist l1 l2))))==(pos_Rl l1 (pred (longueur l1))). +Lemma RList_P16 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> (pos_Rl l1 (pred (Rlength l1)))==(pos_Rl l2 (pred (Rlength l2))) -> (pos_Rl (cons_ORlist l1 l2) (pred (Rlength (cons_ORlist l1 l2))))==(pos_Rl l1 (pred (Rlength l1))). Intros; Apply Rle_antisym. Induction l1. Simpl; Simpl in H1; Right; Symmetry; Assumption. -Assert H2 : (In (pos_Rl (cons_ORlist (cons r l1) l2) (pred (longueur (cons_ORlist (cons r l1) l2)))) (cons_ORlist (cons r l1) l2)); [Elim (RList_P3 (cons_ORlist (cons r l1) l2) (pos_Rl (cons_ORlist (cons r l1) l2) (pred (longueur (cons_ORlist (cons r l1) l2))))); Intros; Apply H3; Exists (pred (longueur (cons_ORlist (cons r l1) l2))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn] | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) (pred (longueur (cons_ORlist (cons r l1) l2))))); Intros; Assert H5 := (H3 H2); Elim H5; Intro; [Apply RList_P7; Assumption | Rewrite H1; Apply RList_P7; Assumption]]. +Assert H2 : (In (pos_Rl (cons_ORlist (cons r l1) l2) (pred (Rlength (cons_ORlist (cons r l1) l2)))) (cons_ORlist (cons r l1) l2)); [Elim (RList_P3 (cons_ORlist (cons r l1) l2) (pos_Rl (cons_ORlist (cons r l1) l2) (pred (Rlength (cons_ORlist (cons r l1) l2))))); Intros; Apply H3; Exists (pred (Rlength (cons_ORlist (cons r l1) l2))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn] | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) (pred (Rlength (cons_ORlist (cons r l1) l2))))); Intros; Assert H5 := (H3 H2); Elim H5; Intro; [Apply RList_P7; Assumption | Rewrite H1; Apply RList_P7; Assumption]]. Induction l1. Simpl; Simpl in H1; Right; Assumption. -Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (longueur (cons r l1))))); Intros; Assert H4 : (In (pos_Rl (cons r l1) (pred (longueur (cons r l1)))) (cons r l1))\/(In (pos_Rl (cons r l1) (pred (longueur (cons r l1)))) l2); [Left; Change (In (pos_Rl (cons r l1) (longueur l1)) (cons r l1)); Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (longueur l1))); Intros; Apply H5; Exists (longueur l1); Split; [Reflexivity | Simpl; Apply lt_n_Sn] | Assert H5 := (H3 H4); Apply RList_P7; [Apply RList_P2; Assumption | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (longueur (cons r l1))))); Intros; Apply H7; Left; Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (pred (longueur (cons r l1))))); Intros; Apply H9; Exists (pred (longueur (cons r l1))); Split; [Reflexivity | Simpl; Apply lt_n_Sn]]]. +Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); Intros; Assert H4 : (In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1))\/(In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2); [Left; Change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1)); Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); Intros; Apply H5; Exists (Rlength l1); Split; [Reflexivity | Simpl; Apply lt_n_Sn] | Assert H5 := (H3 H4); Apply RList_P7; [Apply RList_P2; Assumption | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); Intros; Apply H7; Left; Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); Intros; Apply H9; Exists (pred (Rlength (cons r l1))); Split; [Reflexivity | Simpl; Apply lt_n_Sn]]]. Qed. -Lemma RList_P17 : (l1:Rlist;x:R;i:nat) (ordered_Rlist l1) -> (In x l1) -> ``(pos_Rl l1 i)<x`` -> (lt i (pred (longueur l1))) -> ``(pos_Rl l1 (S i))<=x``. +Lemma RList_P17 : (l1:Rlist;x:R;i:nat) (ordered_Rlist l1) -> (In x l1) -> ``(pos_Rl l1 i)<x`` -> (lt i (pred (Rlength l1))) -> ``(pos_Rl l1 (S i))<=x``. Induction l1. Intros; Elim H0. Intros; Induction i. Simpl; Elim H1; Intro; [Simpl in H2; Rewrite H4 in H2; Elim (Rlt_antirefl ? H2) | Apply RList_P5; [Apply RList_P4 with r; Assumption | Assumption]]. Simpl; Simpl in H2; Elim H1; Intro. -Rewrite H4 in H2; Assert H5 : ``r<=(pos_Rl r0 i)``; [Apply Rle_trans with (pos_Rl r0 O); [Apply (H0 O); Simpl; Simpl in H3; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3) | Elim (RList_P6 r0); Intros; Apply H5; [Apply RList_P4 with r; Assumption | Apply le_O_n | Simpl in H3; Apply lt_S_n; Apply lt_trans with (longueur r0); [Apply H3 | Apply lt_n_Sn]]] | Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H5 H2))]. -Apply H; Try Assumption; [Apply RList_P4 with r; Assumption | Simpl in H3; Apply lt_S_n; Replace (S (pred (longueur r0))) with (longueur r0); [Apply H3 | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3)]]. +Rewrite H4 in H2; Assert H5 : ``r<=(pos_Rl r0 i)``; [Apply Rle_trans with (pos_Rl r0 O); [Apply (H0 O); Simpl; Simpl in H3; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3) | Elim (RList_P6 r0); Intros; Apply H5; [Apply RList_P4 with r; Assumption | Apply le_O_n | Simpl in H3; Apply lt_S_n; Apply lt_trans with (Rlength r0); [Apply H3 | Apply lt_n_Sn]]] | Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H5 H2))]. +Apply H; Try Assumption; [Apply RList_P4 with r; Assumption | Simpl in H3; Apply lt_S_n; Replace (S (pred (Rlength r0))) with (Rlength r0); [Apply H3 | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3)]]. Qed. -Lemma RList_P18 : (l:Rlist;f:R->R) (longueur (app_Rlist l f))=(longueur l). +Lemma RList_P18 : (l:Rlist;f:R->R) (Rlength (app_Rlist l f))=(Rlength l). Induction l; Intros; [Reflexivity | Simpl; Rewrite H; Reflexivity]. Qed. @@ -349,7 +348,7 @@ Lemma RList_P19 : (l:Rlist) ~l==nil -> (EXT r:R | (EXT r0:Rlist | l==(cons r r0) Intros; Induction l; [Elim H; Reflexivity | Exists r; Exists l; Reflexivity]. Qed. -Lemma RList_P20 : (l:Rlist) (le (2) (longueur l)) -> (EXT r:R | (EXT r1:R | (EXT l':Rlist | l==(cons r (cons r1 l'))))). +Lemma RList_P20 : (l:Rlist) (le (2) (Rlength l)) -> (EXT r:R | (EXT r1:R | (EXT l':Rlist | l==(cons r (cons r1 l'))))). Intros; Induction l; [Simpl in H; Elim (le_Sn_O ? H) | Induction l; [Simpl in H; Elim (le_Sn_O ? (le_S_n ? ? H)) | Exists r; Exists r0; Exists l; Reflexivity]]. Qed. @@ -361,26 +360,26 @@ Lemma RList_P22 : (l1,l2:Rlist) ~l1==nil -> (pos_Rl (cons_Rlist l1 l2) O)==(pos_ Induction l1; [Intros; Elim H; Reflexivity | Intros; Reflexivity]. Qed. -Lemma RList_P23 : (l1,l2:Rlist) (longueur (cons_Rlist l1 l2))==(plus (longueur l1) (longueur l2)). +Lemma RList_P23 : (l1,l2:Rlist) (Rlength (cons_Rlist l1 l2))==(plus (Rlength l1) (Rlength l2)). Induction l1; [Intro; Reflexivity | Intros; Simpl; Rewrite H; Reflexivity]. Qed. -Lemma RList_P24 : (l1,l2:Rlist) ~l2==nil -> (pos_Rl (cons_Rlist l1 l2) (pred (longueur (cons_Rlist l1 l2)))) == (pos_Rl l2 (pred (longueur l2))). +Lemma RList_P24 : (l1,l2:Rlist) ~l2==nil -> (pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2)))) == (pos_Rl l2 (pred (Rlength l2))). Induction l1. Intros; Reflexivity. Intros; Rewrite <- (H l2 H0); Induction l2. Elim H0; Reflexivity. -Do 2 Rewrite RList_P23; Replace (plus (longueur (cons r r0)) (longueur (cons r1 l2))) with (S (S (plus (longueur r0) (longueur l2)))); [Replace (plus (longueur r0) (longueur (cons r1 l2))) with (S (plus (longueur r0) (longueur l2))); [Reflexivity | Simpl; Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring] | Simpl; Apply INR_eq; Do 3 Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring]. +Do 2 Rewrite RList_P23; Replace (plus (Rlength (cons r r0)) (Rlength (cons r1 l2))) with (S (S (plus (Rlength r0) (Rlength l2)))); [Replace (plus (Rlength r0) (Rlength (cons r1 l2))) with (S (plus (Rlength r0) (Rlength l2))); [Reflexivity | Simpl; Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring] | Simpl; Apply INR_eq; Do 3 Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring]. Qed. -Lemma RList_P25 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> ``(pos_Rl l1 (pred (longueur l1)))<=(pos_Rl l2 O)`` -> (ordered_Rlist (cons_Rlist l1 l2)). +Lemma RList_P25 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> ``(pos_Rl l1 (pred (Rlength l1)))<=(pos_Rl l2 O)`` -> (ordered_Rlist (cons_Rlist l1 l2)). Induction l1. Intros; Simpl; Assumption. Induction r0. Intros; Simpl; Simpl in H2; Unfold ordered_Rlist; Intros; Simpl in H3. Induction i. Simpl; Assumption. -Change ``(pos_Rl l2 i)<=(pos_Rl l2 (S i))``; Apply (H1 i); Apply lt_S_n; Replace (S (pred (longueur l2))) with (longueur l2); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H4 in H3; Elim (lt_n_O ? H3)]. +Change ``(pos_Rl l2 i)<=(pos_Rl l2 (S i))``; Apply (H1 i); Apply lt_S_n; Replace (S (pred (Rlength l2))) with (Rlength l2); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H4 in H3; Elim (lt_n_O ? H3)]. Intros; Clear H; Assert H : (ordered_Rlist (cons_Rlist (cons r1 r2) l2)). Apply H0; Try Assumption. Apply RList_P4 with r; Assumption. @@ -389,7 +388,7 @@ Simpl; Apply (H1 O); Simpl; Apply lt_O_Sn. Change ``(pos_Rl (cons_Rlist (cons r1 r2) l2) i)<=(pos_Rl (cons_Rlist (cons r1 r2) l2) (S i))``; Apply (H i); Simpl; Apply lt_S_n; Assumption. Qed. -Lemma RList_P26 : (l1,l2:Rlist;i:nat) (lt i (longueur l1)) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l1 i). +Lemma RList_P26 : (l1,l2:Rlist;i:nat) (lt i (Rlength l1)) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l1 i). Induction l1. Intros; Elim (lt_n_O ? H). Intros; Induction i. @@ -405,7 +404,7 @@ Lemma RList_P28 : (l:Rlist) (cons_Rlist l nil)==l. Induction l; [Reflexivity | Intros; Simpl; Rewrite H; Reflexivity]. Qed. -Lemma RList_P29 : (l2,l1:Rlist;i:nat) (le (longueur l1) i) -> (lt i (longueur (cons_Rlist l1 l2))) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l2 (minus i (longueur l1))). +Lemma RList_P29 : (l2,l1:Rlist;i:nat) (le (Rlength l1) i) -> (lt i (Rlength (cons_Rlist l1 l2))) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l2 (minus i (Rlength l1))). Induction l2. Intros; Rewrite RList_P28 in H0; Elim (lt_n_n ? (le_lt_trans ? ? ? H H0)). Intros; Replace (cons_Rlist l1 (cons r r0)) with (cons_Rlist (cons_Rlist l1 (cons r nil)) r0). @@ -415,12 +414,12 @@ Clear l2 r0 H i H0 H1 H2; Induction l1. Reflexivity. Simpl; Assumption. Rewrite RList_P23; Rewrite plus_sym; Simpl; Apply lt_n_Sn. -Replace (minus (S m) (longueur l1)) with (S (minus (S m) (S (longueur l1)))). -Rewrite H3; Simpl; Replace (S (longueur l1)) with (longueur (cons_Rlist l1 (cons r nil))). +Replace (minus (S m) (Rlength l1)) with (S (minus (S m) (S (Rlength l1)))). +Rewrite H3; Simpl; Replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))). Apply (H (cons_Rlist l1 (cons r nil)) i). Rewrite RList_P23; Rewrite plus_sym; Simpl; Rewrite <- H3; Apply le_n_S; Assumption. -Repeat Rewrite RList_P23; Simpl; Rewrite RList_P23 in H1; Rewrite plus_sym in H1; Simpl in H1; Rewrite (plus_sym (longueur l1)); Simpl; Rewrite plus_sym; Apply H1. +Repeat Rewrite RList_P23; Simpl; Rewrite RList_P23 in H1; Rewrite plus_sym in H1; Simpl in H1; Rewrite (plus_sym (Rlength l1)); Simpl; Rewrite plus_sym; Apply H1. Rewrite RList_P23; Rewrite plus_sym; Reflexivity. -Change (S (minus m (longueur l1)))=(minus (S m) (longueur l1)); Apply minus_Sn_m; Assumption. +Change (S (minus m (Rlength l1)))=(minus (S m) (Rlength l1)); Apply minus_Sn_m; Assumption. Replace (cons r r0) with (cons_Rlist (cons r nil) r0); [Symmetry; Apply RList_P27 | Reflexivity]. Qed. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 8a4379a83..116cc2e6f 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -255,11 +255,11 @@ Lemma SubEqui_P1 : (a,b:R;del:posreal;h:``a<b``) (pos_Rl (SubEqui del h) O)==a. Intros; Unfold SubEqui; Case (maxN del h); Intros; Reflexivity. Qed. -Lemma SubEqui_P2 : (a,b:R;del:posreal;h:``a<b``) (pos_Rl (SubEqui del h) (pred (longueur (SubEqui del h))))==b. -Intros; Unfold SubEqui; Case (maxN del h); Intros; Clear a0; Cut (x:nat)(a:R)(del:posreal)(pos_Rl (SubEquiN (S x) a b del) (pred (longueur (SubEquiN (S x) a b del)))) == b; [Intro; Apply H | Induction x0; [Intros; Reflexivity | Intros; Change (pos_Rl (SubEquiN (S n) ``a0+del0`` b del0) (pred (longueur (SubEquiN (S n) ``a0+del0`` b del0))))==b; Apply H]]. +Lemma SubEqui_P2 : (a,b:R;del:posreal;h:``a<b``) (pos_Rl (SubEqui del h) (pred (Rlength (SubEqui del h))))==b. +Intros; Unfold SubEqui; Case (maxN del h); Intros; Clear a0; Cut (x:nat)(a:R)(del:posreal)(pos_Rl (SubEquiN (S x) a b del) (pred (Rlength (SubEquiN (S x) a b del)))) == b; [Intro; Apply H | Induction x0; [Intros; Reflexivity | Intros; Change (pos_Rl (SubEquiN (S n) ``a0+del0`` b del0) (pred (Rlength (SubEquiN (S n) ``a0+del0`` b del0))))==b; Apply H]]. Qed. -Lemma SubEqui_P3 : (N:nat;a,b:R;del:posreal) (longueur (SubEquiN N a b del))=(S N). +Lemma SubEqui_P3 : (N:nat;a,b:R;del:posreal) (Rlength (SubEquiN N a b del))=(S N). Induction N; Intros; [Reflexivity | Simpl; Rewrite H; Reflexivity]. Qed. @@ -267,7 +267,7 @@ Lemma SubEqui_P4 : (N:nat;a,b:R;del:posreal;i:nat) (lt i (S N)) -> (pos_Rl (SubE Induction N; [Intros; Inversion H; [Simpl; Ring | Elim (le_Sn_O ? H1)] | Intros; Induction i; [Simpl; Ring | Change (pos_Rl (SubEquiN (S n) ``a+del`` b del) i)==``a+(INR (S i))*del``; Rewrite H; [Rewrite S_INR; Ring | Apply lt_S_n; Apply H0]]]. Qed. -Lemma SubEqui_P5 : (a,b:R;del:posreal;h:``a<b``) (longueur (SubEqui del h))=(S (S (max_N del h))). +Lemma SubEqui_P5 : (a,b:R;del:posreal;h:``a<b``) (Rlength (SubEqui del h))=(S (S (max_N del h))). Intros; Unfold SubEqui; Apply SubEqui_P3. Qed. @@ -278,7 +278,7 @@ Qed. Lemma SubEqui_P7 : (a,b:R;del:posreal;h:``a<b``) (ordered_Rlist (SubEqui del h)). Intros; Unfold ordered_Rlist; Intros; Rewrite SubEqui_P5 in H; Simpl in H; Inversion H. Rewrite (SubEqui_P6 3!del 4!h 5!(max_N del h)). -Replace (S (max_N del h)) with (pred (longueur (SubEqui del h))). +Replace (S (max_N del h)) with (pred (Rlength (SubEqui del h))). Rewrite SubEqui_P2; Unfold max_N; Case (maxN del h); Intros; Left; Elim a0; Intros; Assumption. Rewrite SubEqui_P5; Reflexivity. Apply lt_n_Sn. @@ -288,7 +288,7 @@ Repeat Rewrite SubEqui_P6. Apply Rle_compatibility; Rewrite S_INR; Rewrite Rmult_Rplus_distrl; Pattern 1 ``(INR i)*del``; Rewrite <- Rplus_Or; Apply Rle_compatibility; Rewrite Rmult_1l; Left; Apply (cond_pos del). Qed. -Lemma SubEqui_P8 : (a,b:R;del:posreal;h:``a<b``;i:nat) (lt i (longueur (SubEqui del h))) -> ``a<=(pos_Rl (SubEqui del h) i)<=b``. +Lemma SubEqui_P8 : (a,b:R;del:posreal;h:``a<b``;i:nat) (lt i (Rlength (SubEqui del h))) -> ``a<=(pos_Rl (SubEqui del h) i)<=b``. Intros; Split. Pattern 1 a; Rewrite <- (SubEqui_P1 del h); Apply RList_P5. Apply SubEqui_P7. @@ -296,7 +296,7 @@ Elim (RList_P3 (SubEqui del h) (pos_Rl (SubEqui del h) i)); Intros; Apply H1; Ex Pattern 2 b; Rewrite <- (SubEqui_P2 del h); Apply RList_P7; [Apply SubEqui_P7 | Elim (RList_P3 (SubEqui del h) (pos_Rl (SubEqui del h) i)); Intros; Apply H1; Exists i; Split; [Reflexivity | Assumption]]. Qed. -Lemma SubEqui_P9 : (a,b:R;del:posreal;f:R->R;h:``a<b``) (sigTT ? [g:(StepFun a b)](g b)==(f b)/\(i:nat)(lt i (pred (longueur (SubEqui del h))))->(constant_D_eq g (co_interval (pos_Rl (SubEqui del h) i) (pos_Rl (SubEqui del h) (S i))) (f (pos_Rl (SubEqui del h) i)))). +Lemma SubEqui_P9 : (a,b:R;del:posreal;f:R->R;h:``a<b``) (sigTT ? [g:(StepFun a b)](g b)==(f b)/\(i:nat)(lt i (pred (Rlength (SubEqui del h))))->(constant_D_eq g (co_interval (pos_Rl (SubEqui del h) i) (pos_Rl (SubEqui del h) (S i))) (f (pos_Rl (SubEqui del h) i)))). Intros; Apply StepFun_P38; [Apply SubEqui_P7 | Apply SubEqui_P1 | Apply SubEqui_P2]. Qed. @@ -322,19 +322,19 @@ Elim (Heine_cor2 H0 (mkposreal ? H1)); Intros del H4; Elim (SubEqui_P9 del f H); 2:Apply Rminus_eq_contra; Red; Intro; Clear H6; Rewrite H7 in H; Elim (Rlt_antirefl ? H). 2:DiscrR. 2:Apply Rminus_eq_contra; Red; Intro; Clear H6; Rewrite H7 in H; Elim (Rlt_antirefl ? H). -Intros; Rewrite H2 in H7; Rewrite H3 in H7; Simpl; Unfold fct_cte; Cut (t:R)``a<=t<=b``->t==b\/(EX i:nat | (lt i (pred (longueur (SubEqui del H))))/\(co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i)) t)). +Intros; Rewrite H2 in H7; Rewrite H3 in H7; Simpl; Unfold fct_cte; Cut (t:R)``a<=t<=b``->t==b\/(EX i:nat | (lt i (pred (Rlength (SubEqui del H))))/\(co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i)) t)). Intro; Elim (H8 ? H7); Intro. Rewrite H9; Rewrite H5; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Left; Assumption. Elim H9; Clear H9; Intros I [H9 H10]; Assert H11 := (H6 I H9 t H10); Rewrite H11; Left; Apply H4. Assumption. -Apply SubEqui_P8; Apply lt_trans with (pred (longueur (SubEqui del H))). +Apply SubEqui_P8; Apply lt_trans with (pred (Rlength (SubEqui del H))). Assumption. Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H12 in H9; Elim (lt_n_O ? H9). Unfold co_interval in H10; Elim H10; Clear H10; Intros; Rewrite Rabsolu_right. Rewrite SubEqui_P5 in H9; Simpl in H9; Inversion H9. Apply Rlt_anti_compatibility with (pos_Rl (SubEqui del H) (max_N del H)). Replace ``(pos_Rl (SubEqui del H) (max_N del H))+(t-(pos_Rl (SubEqui del H) (max_N del H)))`` with t; [Idtac | Ring]; Apply Rlt_le_trans with b. -Rewrite H14 in H12; Assert H13 : (S (max_N del H))=(pred (longueur (SubEqui del H))). +Rewrite H14 in H12; Assert H13 : (S (max_N del H))=(pred (Rlength (SubEqui del H))). Rewrite SubEqui_P5; Reflexivity. Rewrite H13 in H12; Rewrite SubEqui_P2 in H12; Apply H12. Rewrite SubEqui_P6. @@ -369,7 +369,7 @@ Rewrite SubEqui_P6. Apply H5. Assumption. Inversion H7. -Replace (S (max_N del H)) with (pred (longueur (SubEqui del H))). +Replace (S (max_N del H)) with (pred (Rlength (SubEqui del H))). Rewrite (SubEqui_P2 del H); Elim H8; Intros. Elim H11; Intro. Assumption. @@ -784,7 +784,7 @@ Replace a with (Rmin a b). Rewrite <- H5; Elim (RList_P6 l); Intros; Apply H10. Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur l)); [Assumption | Apply lt_pred_n_n]. +Apply lt_trans with (pred (Rlength l)); [Assumption | Apply lt_pred_n_n]. Apply neq_O_lt; Intro; Rewrite <- H12 in H6; Discriminate. Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. Assert H11 : ``(pos_Rl l (S i))<=b``. @@ -901,7 +901,7 @@ Apply Rle_lt_trans with (pos_Rl l1 i). Replace b with (Rmin b c). Rewrite <- H5; Elim (RList_P6 l1); Intros; Apply H10; Try Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H12 in H6; Discriminate. +Apply lt_trans with (pred (Rlength l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H12 in H6; Discriminate. Unfold Rmin; Case (total_order_Rle b c); Intro; [Reflexivity | Elim n; Assumption]. Elim H7; Intros; Assumption. Case (total_order_Rle a x); Case (total_order_Rle x b); Intros; [Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H10)) | Reflexivity | Elim n; Apply Rle_trans with b; [Assumption | Left; Assumption] | Elim n0; Apply Rle_trans with b; [Assumption | Left; Assumption]]. @@ -918,7 +918,7 @@ Apply Rle_trans with (pos_Rl l1 i). Replace a with (Rmin a b). Rewrite <- H5; Elim (RList_P6 l1); Intros; Apply H11; Try Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H6; Discriminate. +Apply lt_trans with (pred (Rlength l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H6; Discriminate. Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. Left; Elim H7; Intros; Assumption. Case (total_order_Rle a x); Case (total_order_Rle x b); Intros; Reflexivity Orelse Elim n; Assumption. @@ -936,7 +936,7 @@ Apply Rle_trans with (pos_Rl l1 i). Replace a with (Rmin a b). Rewrite <- H5; Elim (RList_P6 l1); Intros; Apply H11; Try Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H6; Discriminate. +Apply lt_trans with (pred (Rlength l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H6; Discriminate. Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Assumption]. Left; Elim H7; Intros; Assumption. Unfold phi3; Case (total_order_Rle a x); Case (total_order_Rle x b); Intros; Reflexivity Orelse Elim n; Assumption. @@ -946,7 +946,7 @@ Apply Rle_lt_trans with (pos_Rl l1 i). Replace b with (Rmin b c). Rewrite <- H5; Elim (RList_P6 l1); Intros; Apply H10; Try Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H12 in H6; Discriminate. +Apply lt_trans with (pred (Rlength l1)); Try Assumption; Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H12 in H6; Discriminate. Unfold Rmin; Case (total_order_Rle b c); Intro; [Reflexivity | Elim n; Assumption]. Elim H7; Intros; Assumption. Unfold phi3; Case (total_order_Rle a x); Case (total_order_Rle x b); Intros; [Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H10)) | Reflexivity | Elim n; Apply Rle_trans with b; [Assumption | Left; Assumption] | Elim n0; Apply Rle_trans with b; [Assumption | Left; Assumption]]. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index a6c1c7a08..ab0283899 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -69,9 +69,9 @@ Qed. Definition open_interval [a,b:R] : R->Prop := [x:R]``a<x<b``. Definition co_interval [a,b:R] : R->Prop := [x:R]``a<=x<b``. -Definition adapted_couple [f:R->R;a,b:R;l,lf:Rlist] : Prop := (ordered_Rlist l)/\``(pos_Rl l O)==(Rmin a b)``/\``(pos_Rl l (pred (longueur l)))==(Rmax a b)``/\(longueur l)=(S (longueur lf))/\(i:nat)(lt i (pred (longueur l)))->(constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i))) (pos_Rl lf i)). +Definition adapted_couple [f:R->R;a,b:R;l,lf:Rlist] : Prop := (ordered_Rlist l)/\``(pos_Rl l O)==(Rmin a b)``/\``(pos_Rl l (pred (Rlength l)))==(Rmax a b)``/\(Rlength l)=(S (Rlength lf))/\(i:nat)(lt i (pred (Rlength l)))->(constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i))) (pos_Rl lf i)). -Definition adapted_couple_opt [f:R->R;a,b:R;l,lf:Rlist] := (adapted_couple f a b l lf)/\((i:nat)(lt i (pred (longueur lf)))->(``(pos_Rl lf i)<>(pos_Rl lf (S i))``\/``(f (pos_Rl l (S i)))<>(pos_Rl lf i)``))/\((i:nat)(lt i (pred (longueur l)))->``(pos_Rl l i)<>(pos_Rl l (S i))``). +Definition adapted_couple_opt [f:R->R;a,b:R;l,lf:Rlist] := (adapted_couple f a b l lf)/\((i:nat)(lt i (pred (Rlength lf)))->(``(pos_Rl lf i)<>(pos_Rl lf (S i))``\/``(f (pos_Rl l (S i)))<>(pos_Rl lf i)``))/\((i:nat)(lt i (pred (Rlength l)))->``(pos_Rl l i)<>(pos_Rl l (S i))``). Definition is_subdivision [f:R->R;a,b:R;l:Rlist] : Type := (sigTT ? [l0:Rlist](adapted_couple f a b l l0)). @@ -159,7 +159,7 @@ Apply RList_P4 with r1; Assumption. Rewrite H5 in H2; Unfold Rmin; Case (total_order_Rle r2 b); Intro; [Reflexivity | Elim n; Assumption]. Unfold Rmax; Case (total_order_Rle r2 b); Intro; [Rewrite H5 in H2; Rewrite <- H2; Reflexivity | Elim n; Assumption]. Simpl in H4; Simpl; Apply INR_eq; Apply r_Rplus_plus with R1; Do 2 Rewrite (Rplus_sym R1); Do 2 Rewrite <- S_INR; Rewrite H4; Reflexivity. -Intros; Unfold constant_D_eq open_interval; Intros; Unfold constant_D_eq open_interval in H6; Assert H9 : (lt (S i) (pred (longueur (cons r1 (cons r2 l))))). +Intros; Unfold constant_D_eq open_interval; Intros; Unfold constant_D_eq open_interval in H6; Assert H9 : (lt (S i) (pred (Rlength (cons r1 (cons r2 l))))). Simpl; Simpl in H0; Apply lt_n_S; Assumption. Assert H10 := (H6 ? H9); Apply H10; Assumption. Qed. @@ -183,7 +183,7 @@ Apply (H3 O); Simpl; Apply lt_O_Sn. Simpl in H5; Rewrite H2 in H5; Rewrite H5; Replace (Rmin b b) with (Rmax a b); [Rewrite <- H4; Apply RList_P7; [Assumption | Simpl; Right; Left; Reflexivity] | Unfold Rmin Rmax; Case (total_order_Rle b b); Case (total_order_Rle a b); Intros; Try Assumption Orelse Reflexivity]. Qed. -Lemma StepFun_P9 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> ``a<>b`` -> (le (2) (longueur l)). +Lemma StepFun_P9 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> ``a<>b`` -> (le (2) (Rlength l)). Intros; Unfold adapted_couple in H; Decompose [and] H; Clear H; Induction l; [Simpl in H4; Discriminate | Induction l; [Simpl in H3; Simpl in H2; Generalize H3; Generalize H2; Unfold Rmin Rmax; Case (total_order_Rle a b); Intros; Elim H0; Rewrite <- H5; Rewrite <- H7; Reflexivity | Simpl; Do 2 Apply le_n_S; Apply le_O_n]]. Qed. @@ -449,7 +449,7 @@ Clear Hreci; Simpl; Apply (H21 (S i)). Simpl; Apply lt_S_n; Assumption. Unfold open_interval; Apply H2. Elim H3; Clear H3; Intros; Split. -Rewrite H9; Change (i:nat) (lt i (pred (longueur (cons r4 lf2)))) ->``(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 H9; Change (i:nat) (lt i (pred (Rlength (cons r4 lf2)))) ->``(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. Simpl; Red; Intro; Rewrite H13 in H10; Elim (Rlt_antirefl ? H10). Clear Hreci; Apply (H11 (S i)); Simpl; Apply H12. @@ -480,7 +480,7 @@ 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 (longueur lf2) with (S (pred (longueur lf2))). +Simpl; Replace (Rlength lf2) with (S (pred (Rlength lf2))). Apply lt_n_S; Apply H12. Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H12; Elim (lt_n_O ? H12). Intros; Simpl in H12; Rewrite H10; Rewrite H5 in H11; Apply (H11 (S i)); Simpl; Apply lt_n_S; Apply H12. @@ -514,7 +514,7 @@ Lemma StepFun_P19 : (l1:Rlist;f,g:R->R;l:R) (Int_SF (FF l1 [x:R]``(f x)+l*(g x)` Intros; Induction l1; [Simpl; Ring | Induction l1; Simpl; [Ring | Simpl in Hrecl1; Rewrite Hrecl1; Ring]]. Qed. -Lemma StepFun_P20 : (l:Rlist;f:R->R) (lt O (longueur l)) -> (longueur l)=(S (longueur (FF l f))). +Lemma StepFun_P20 : (l:Rlist;f:R->R) (lt O (Rlength l)) -> (Rlength l)=(S (Rlength (FF l f))). Induction l; Intros; [Elim (lt_n_n ? H) | Simpl; Rewrite RList_P18; Rewrite RList_P14; Induction r0; [Reflexivity | Rewrite (H f); [Reflexivity | Simpl; Apply lt_O_Sn]]]. Qed. @@ -555,19 +555,19 @@ Apply RList_P5; [Apply RList_P2; Assumption | Assumption]. Rewrite Hyp_max; Apply Rle_antisym. Induction lf. Simpl; Right; Assumption. -Assert H8 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (longueur (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 (longueur (cons_ORlist (cons r lf) lg))))); Intros _ H10; Apply H10; Exists (pred (longueur (cons_ORlist (cons r lf) lg))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn]. -Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (longueur (cons_ORlist (cons r lf) lg))))); Intros H10 _. +Assert H8 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (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 (Rlength (cons_ORlist (cons r lf) lg))))); Intros _ H10; Apply H10; Exists (pred (Rlength (cons_ORlist (cons r lf) lg))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn]. +Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (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 (longueur (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 lt_n_Sm_le; Assumption | Simpl; Apply lt_n_Sn]. -Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (longueur (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros. -Rewrite H15; Assert H17 : (longueur lg)=(S (pred (longueur lg))). +Elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (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 lt_n_Sm_le; Assumption | Simpl; Apply lt_n_Sn]. +Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros. +Rewrite H15; Assert H17 : (Rlength lg)=(S (pred (Rlength lg))). Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H17 in H16; Elim (lt_n_O ? H16). Rewrite <- H0; Elim (RList_P6 lg); Intros; Apply H18; [Assumption | Rewrite H17 in H16; Apply lt_n_Sm_le; Assumption | Apply lt_pred_n_n; Rewrite H17; Apply lt_O_Sn]. Induction lf. 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 (longueur (cons r lf))); Split; [Symmetry; Assumption | Simpl; Apply lt_n_Sn]. +Elim (RList_P9 (cons r lf) lg b); Intros; Apply H10; Left; Elim (RList_P3 (cons r lf) b); Intros; Apply H12; Exists (pred (Rlength (cons r lf))); Split; [Symmetry; Assumption | Simpl; Apply lt_n_Sn]. Apply RList_P7; [Apply RList_P2; Assumption | Assumption]. Apply StepFun_P20; Rewrite RList_P11; Rewrite H2; Rewrite H7; Simpl; Apply lt_O_Sn. Intros; Unfold constant_D_eq open_interval; Intros; Cut (EXT l:R | (constant_D_eq f (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l)). @@ -590,7 +590,7 @@ Rewrite <- H6; Rewrite <- (RList_P15 lf lg). Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H11. Apply RList_P2; Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur (cons_ORlist lf lg))); [Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H8; Elim (lt_n_O ? H8)]. +Apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); [Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H8; Elim (lt_n_O ? H8)]. Assumption. Assumption. Rewrite H1; Assumption. @@ -602,8 +602,8 @@ Apply RList_P2; Assumption. Apply lt_n_Sm_le; Apply lt_n_S; Assumption. Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H8; Elim (lt_n_O ? H8). Rewrite H0; Assumption. -Pose I := [j:nat]``(pos_Rl lf j)<=(pos_Rl (cons_ORlist lf lg) i)``/\(lt j (longueur lf)); Assert H12 : (Nbound I). -Unfold Nbound; Exists (longueur lf); Intros; Unfold I in H12; Elim H12; Intros; Apply lt_le_weak; Assumption. +Pose I := [j:nat]``(pos_Rl lf j)<=(pos_Rl (cons_ORlist lf lg) i)``/\(lt j (Rlength lf)); Assert H12 : (Nbound I). +Unfold Nbound; Exists (Rlength lf); Intros; Unfold I in H12; Elim H12; Intros; Apply lt_le_weak; Assumption. Assert H13 : (EX n:nat | (I n)). Exists O; Unfold I; Split. Apply Rle_trans with (pos_Rl (cons_ORlist lf lg) O). @@ -612,20 +612,20 @@ Apply RList_P15; Try Assumption; Rewrite H1; Assumption. Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H13. Apply RList_P2; Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur (cons_ORlist lf lg))). +Apply lt_trans with (pred (Rlength (cons_ORlist lf lg))). Assumption. Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H15 in H8; Elim (lt_n_O ? H8). Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H5; Rewrite <- H6 in H11; Rewrite <- H5 in H11; Elim (Rlt_antirefl ? H11). -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 : (lt x0 (pred (longueur lf))). -Elim H14; Clear H14; Intros; Unfold I in H14; Elim H14; Clear H14; Intros; Apply lt_S_n; Replace (S (pred (longueur lf))) with (longueur lf). +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 : (lt x0 (pred (Rlength lf))). +Elim H14; Clear H14; Intros; Unfold I in H14; Elim H14; Clear H14; Intros; Apply lt_S_n; Replace (S (pred (Rlength lf))) with (Rlength lf). Inversion H18. 2:Apply lt_n_S; Assumption. -Cut x0=(pred (longueur lf)). +Cut x0=(pred (Rlength lf)). Intro; Rewrite H19 in H14; Rewrite H5 in H14; Cut ``(pos_Rl (cons_ORlist lf lg) i)<b``. Intro; Elim (Rlt_antirefl ? (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 (longueur (cons_ORlist lf lg)))). +Rewrite <- H5; Apply Rle_trans with (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H21. Apply RList_P2; Assumption. Apply lt_n_Sm_le; Apply lt_n_S; Assumption. @@ -638,8 +638,8 @@ 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)); Try Assumption. -Assert H22 : (lt (S x0) (longueur lf)). -Replace (longueur lf) with (S (pred (longueur lf))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H22 in H21; Elim (lt_n_O ? H21)]. +Assert H22 : (lt (S x0) (Rlength lf)). +Replace (Rlength lf) with (S (pred (Rlength lf))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H22 in H21; Elim (lt_n_O ? H21)]. Elim (total_order_Rle (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); Intro. Assert H23 : (le (S x0) x0). Apply H20; Unfold I; Split; Assumption. @@ -678,17 +678,17 @@ Apply RList_P5; [Apply RList_P2; Assumption | Assumption]. Rewrite Hyp_max; Apply Rle_antisym. Induction lf. Simpl; Right; Assumption. -Assert H8 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (longueur (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 (longueur (cons_ORlist (cons r lf) lg))))); Intros _ H10; Apply H10; Exists (pred (longueur (cons_ORlist (cons r lf) lg))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn]. -Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (longueur (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 (longueur (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 lt_n_Sm_le; Assumption | Simpl; Apply lt_n_Sn]. -Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (longueur (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Assert H17 : (longueur lg)=(S (pred (longueur lg))). +Assert H8 : (In (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (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 (Rlength (cons_ORlist (cons r lf) lg))))); Intros _ H10; Apply H10; Exists (pred (Rlength (cons_ORlist (cons r lf) lg))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn]. +Elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (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 (Rlength (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 lt_n_Sm_le; Assumption | Simpl; Apply lt_n_Sn]. +Elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) (pred (Rlength (cons_ORlist (cons r lf) lg))))); Intros H13 _; Assert H14 := (H13 H12); Elim H14; Intros; Elim H15; Clear H15; Intros; Rewrite H15; Assert H17 : (Rlength lg)=(S (pred (Rlength lg))). Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H17 in H16; Elim (lt_n_O ? H16). Rewrite <- H0; Elim (RList_P6 lg); Intros; Apply H18; [Assumption | Rewrite H17 in H16; Apply lt_n_Sm_le; Assumption | Apply lt_pred_n_n; Rewrite H17; Apply lt_O_Sn]. Induction lf. 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 (longueur (cons r lf))); Split; [Symmetry; Assumption | Simpl; Apply lt_n_Sn]. +Elim (RList_P9 (cons r lf) lg b); Intros; Apply H10; Left; Elim (RList_P3 (cons r lf) b); Intros; Apply H12; Exists (pred (Rlength (cons r lf))); Split; [Symmetry; Assumption | Simpl; Apply lt_n_Sn]. Apply RList_P7; [Apply RList_P2; Assumption | Assumption]. Apply StepFun_P20; Rewrite RList_P11; Rewrite H7; Rewrite H2; Simpl; Apply lt_O_Sn. Unfold constant_D_eq open_interval; Intros; Cut (EXT l:R | (constant_D_eq g (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l)). @@ -711,7 +711,7 @@ Rewrite <- H6; Rewrite <- (RList_P15 lf lg); Try Assumption. Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H11. Apply RList_P2; Assumption. Apply le_O_n. -Apply lt_trans with (pred (longueur (cons_ORlist lf lg))); [Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H8; Elim (lt_n_O ? H8)]. +Apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); [Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H8; Elim (lt_n_O ? H8)]. Rewrite H1; Assumption. Apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). Elim H10; Intros; Apply Rlt_trans with x; Assumption. @@ -721,24 +721,24 @@ Apply RList_P2; Assumption. Apply lt_n_Sm_le; Apply lt_n_S; Assumption. Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H8; Elim (lt_n_O ? H8). Rewrite H0; Assumption. -Pose I := [j:nat]``(pos_Rl lg j)<=(pos_Rl (cons_ORlist lf lg) i)``/\(lt j (longueur lg)); Assert H12 : (Nbound I). -Unfold Nbound; Exists (longueur lg); Intros; Unfold I in H12; Elim H12; Intros; Apply lt_le_weak; Assumption. +Pose I := [j:nat]``(pos_Rl lg j)<=(pos_Rl (cons_ORlist lf lg) i)``/\(lt j (Rlength lg)); Assert H12 : (Nbound I). +Unfold Nbound; Exists (Rlength lg); Intros; Unfold I in H12; Elim H12; Intros; Apply lt_le_weak; Assumption. Assert H13 : (EX n:nat | (I n)). Exists O; Unfold I; Split. Apply Rle_trans with (pos_Rl (cons_ORlist lf lg) O). Right; Symmetry; Rewrite H1; Rewrite <- H6; Apply RList_P15; Try Assumption; Rewrite H1; Assumption. -Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H13; [Apply RList_P2; Assumption | Apply le_O_n | Apply lt_trans with (pred (longueur (cons_ORlist lf lg))); [Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H15 in H8; Elim (lt_n_O ? H8)]]. +Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H13; [Apply RList_P2; Assumption | Apply le_O_n | Apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); [Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H15 in H8; Elim (lt_n_O ? H8)]]. Apply neq_O_lt; Red; Intro; Rewrite <- H13 in H0; Rewrite <- H1 in H11; Rewrite <- H0 in H11; Elim (Rlt_antirefl ? H11). -Assert H14 := (Nzorn H13 H12); Elim H14; Clear H14; Intros x0 H14; Exists (pos_Rl lg0 x0); Unfold constant_D_eq open_interval; Intros; Assert H16 := (H4 x0); Assert H17 : (lt x0 (pred (longueur lg))). -Elim H14; Clear H14; Intros; Unfold I in H14; Elim H14; Clear H14; Intros; Apply lt_S_n; Replace (S (pred (longueur lg))) with (longueur lg). +Assert H14 := (Nzorn H13 H12); Elim H14; Clear H14; Intros x0 H14; Exists (pos_Rl lg0 x0); Unfold constant_D_eq open_interval; Intros; Assert H16 := (H4 x0); Assert H17 : (lt x0 (pred (Rlength lg))). +Elim H14; Clear H14; Intros; Unfold I in H14; Elim H14; Clear H14; Intros; Apply lt_S_n; Replace (S (pred (Rlength lg))) with (Rlength lg). Inversion H18. 2:Apply lt_n_S; Assumption. -Cut x0=(pred (longueur lg)). +Cut x0=(pred (Rlength lg)). Intro; Rewrite H19 in H14; Rewrite H0 in H14; Cut ``(pos_Rl (cons_ORlist lf lg) i)<b``. Intro; Elim (Rlt_antirefl ? (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 <- H0; Apply Rle_trans with (pos_Rl (cons_ORlist lf lg) (pred (longueur (cons_ORlist lf lg)))). +Rewrite <- H0; Apply Rle_trans with (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). Elim (RList_P6 (cons_ORlist lf lg)); Intros; Apply H21. Apply RList_P2; Assumption. Apply lt_n_Sm_le; Apply lt_n_S; Assumption. @@ -752,8 +752,8 @@ 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)); Try Assumption. -Assert H22 : (lt (S x0) (longueur lg)). -Replace (longueur lg) with (S (pred (longueur lg))). +Assert H22 : (lt (S x0) (Rlength lg)). +Replace (Rlength lg) with (S (pred (Rlength lg))). Apply lt_n_S; Assumption. Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H22 in H21; Elim (lt_n_O ? H21). Elim (total_order_Rle (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); Intro. @@ -826,7 +826,7 @@ Apply StepFun_P17 with [x:R](Rabsolu (f x)) a b; [Apply StepFun_P31; Apply StepF Elim n; Assumption. Qed. -Lemma StepFun_P35 : (l:Rlist;a,b:R;f,g:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (longueur l)))==b -> ((x:R)``a<x<b``->``(f x)<=(g x)``) -> ``(Int_SF (FF l f) l)<=(Int_SF (FF l g) l)``. +Lemma StepFun_P35 : (l:Rlist;a,b:R;f,g:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (Rlength l)))==b -> ((x:R)``a<x<b``->``(f x)<=(g x)``) -> ``(Int_SF (FF l f) l)<=(Int_SF (FF l g) l)``. Induction l; Intros. Right; Reflexivity. Simpl; Induction r0. @@ -853,7 +853,7 @@ Apply Rlt_monotony_contra with ``2``. Sup0. Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. Rewrite Rmult_1l; Rewrite double; Assert H5 : ``r0<=b``. -Replace b with (pos_Rl (cons r (cons r0 r1)) (pred (longueur (cons r (cons r0 r1))))). +Replace b with (pos_Rl (cons r (cons r0 r1)) (pred (Rlength (cons r (cons r0 r1))))). Replace r0 with (pos_Rl (cons r (cons r0 r1)) (S O)). Elim (RList_P6 (cons r (cons r0 r1))); Intros; Apply H5. Assumption. @@ -898,7 +898,7 @@ EApply StepFun_P25; Apply StepFun_P29. EApply StepFun_P23; Apply StepFun_P29. Qed. -Lemma StepFun_P38 : (l:Rlist;a,b:R;f:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (longueur l)))==b -> (sigTT ? [g:(StepFun a b)](g b)==(f b)/\(i:nat)(lt i (pred (longueur l)))->(constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) (f (pos_Rl l i)))). +Lemma StepFun_P38 : (l:Rlist;a,b:R;f:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (Rlength l)))==b -> (sigTT ? [g:(StepFun a b)](g b)==(f b)/\(i:nat)(lt i (pred (Rlength l)))->(constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) (f (pos_Rl l i)))). Induction l. Intros; Simpl in H0; Simpl in H1; Exists (mkStepFun (StepFun_P4 a b (f b))); Split. Reflexivity. @@ -911,7 +911,7 @@ Intros; Clear X; Assert H2 : (ordered_Rlist (cons r1 r2)). Apply RList_P4 with r; Assumption. Assert H3 : (pos_Rl (cons r1 r2) O)==r1. Reflexivity. -Assert H4 : (pos_Rl (cons r1 r2) (pred (longueur (cons r1 r2))))==b. +Assert H4 : (pos_Rl (cons r1 r2) (pred (Rlength (cons r1 r2))))==b. Rewrite <- H1; Reflexivity. Elim (X0 r1 b f H2 H3 H4); Intros g [H5 H6]. Pose g' := [x:R]Cases (total_order_Rle r1 x) of @@ -926,7 +926,7 @@ Simpl; Rewrite H12; Replace (Rmin r1 b) with r1. Simpl in H0; Rewrite <- H0; Apply (H O); Simpl; Apply lt_O_Sn. Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n; Assumption]. Apply (H10 i); Apply lt_S_n. -Replace (S (pred (longueur lg))) with (longueur lg). +Replace (S (pred (Rlength lg))) with (Rlength lg). Apply H9. Apply S_pred with O; Apply neq_O_lt; Intro; Rewrite <- H14 in H9; Elim (lt_n_O ? H9). Simpl; Assert H14 : ``a<=b``. @@ -946,9 +946,9 @@ Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n; Assumpti Rewrite H16 in H12; Rewrite H12 in H14; Elim H14; Clear H14; Intros _ H14; Unfold g'; Case (total_order_Rle r1 x); Intro. Elim (Rlt_antirefl ? (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 : (lt i (pred (longueur lg))). +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 : (lt i (pred (Rlength lg))). Apply lt_S_n. -Replace (S (pred (longueur lg))) with (longueur lg). +Replace (S (pred (Rlength lg))) with (Rlength lg). Assumption. Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H14 in H9; Elim (lt_n_O ? 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 (total_order_Rle r1 x); Intro. @@ -959,7 +959,7 @@ Apply RList_P5. Assumption. Elim (RList_P3 lg (pos_Rl lg i)); Intros; Apply H21; Exists i; Split. Reflexivity. -Apply lt_trans with (pred (longueur lg)); Try Assumption. +Apply lt_trans with (pred (Rlength lg)); Try Assumption. Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H22 in H17; Elim (lt_n_O ? H17). Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n0; Assumption]. Exists (mkStepFun H8); Split. @@ -970,11 +970,11 @@ Intros; Simpl in H9; Induction i. Unfold constant_D_eq co_interval; Simpl; Intros; Simpl in H0; Rewrite H0; Elim H10; Clear H10; Intros; Unfold g'; Case (total_order_Rle r1 x); Intro. Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r3 H11)). Reflexivity. -Clear Hreci; Change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 r2) i) (pos_Rl (cons r1 r2) (S i))) (f (pos_Rl (cons r1 r2) i))); Assert H10 := (H6 i); Assert H11 : (lt i (pred (longueur (cons r1 r2)))). +Clear Hreci; Change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 r2) i) (pos_Rl (cons r1 r2) (S i))) (f (pos_Rl (cons r1 r2) i))); Assert H10 := (H6 i); Assert H11 : (lt i (pred (Rlength (cons r1 r2)))). Simpl; Apply lt_S_n; 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 (total_order_Rle r1 x); Intro. Reflexivity. -Elim n; Elim H13; Clear H13; Intros; Apply Rle_trans with (pos_Rl (cons r1 r2) i); Try Assumption; Change ``(pos_Rl (cons r1 r2) O)<=(pos_Rl (cons r1 r2) i)``; Elim (RList_P6 (cons r1 r2)); Intros; Apply H15; [Assumption | Apply le_O_n | Simpl; Apply lt_trans with (longueur r2); [Apply lt_S_n; Assumption | Apply lt_n_Sn]]. +Elim n; Elim H13; Clear H13; Intros; Apply Rle_trans with (pos_Rl (cons r1 r2) i); Try Assumption; Change ``(pos_Rl (cons r1 r2) O)<=(pos_Rl (cons r1 r2) i)``; Elim (RList_P6 (cons r1 r2)); Intros; Apply H15; [Assumption | Apply le_O_n | Simpl; Apply lt_trans with (Rlength r2); [Apply lt_S_n; Assumption | Apply lt_n_Sn]]. Qed. Lemma StepFun_P39 : (a,b:R;f:(StepFun a b)) (RiemannInt_SF f)==(Ropp (RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))))). @@ -997,19 +997,19 @@ Rewrite H9; Unfold Rmin Rmax; Case (total_order_Rle b c); Case (total_order_Rle Red; Intro; Rewrite H1 in H11; Discriminate. Apply StepFun_P20. Rewrite RList_P23; Apply neq_O_lt; Red; Intro. -Assert H2 : (plus (longueur l1) (longueur l2))=O. +Assert H2 : (plus (Rlength l1) (Rlength l2))=O. Symmetry; Apply H1. Elim (plus_is_O ? ? H2); Intros; Rewrite H12 in H6; Discriminate. -Unfold constant_D_eq open_interval; Intros; Elim (le_or_lt (S (S i)) (longueur l1)); Intro. +Unfold constant_D_eq open_interval; Intros; Elim (le_or_lt (S (S i)) (Rlength l1)); Intro. Assert H14 : (pos_Rl (cons_Rlist l1 l2) i) == (pos_Rl l1 i). -Apply RList_P26; Apply lt_S_n; Apply le_lt_n_Sm; Apply le_S_n; Apply le_trans with (longueur l1); [Assumption | Apply le_n_Sn]. +Apply RList_P26; Apply lt_S_n; Apply le_lt_n_Sm; Apply le_S_n; Apply le_trans with (Rlength l1); [Assumption | Apply le_n_Sn]. Assert H15 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l1 (S i)). Apply RList_P26; Apply lt_S_n; Apply le_lt_n_Sm; Assumption. -Rewrite H14 in H2; Rewrite H15 in H2; Assert H16 : (le (2) (longueur l1)). +Rewrite H14 in H2; Rewrite H15 in H2; Assert H16 : (le (2) (Rlength l1)). Apply le_trans with (S (S i)); [Repeat Apply le_n_S; Apply le_O_n | Assumption]. Elim (RList_P20 ? H16); Intros r1 [r2 [r3 H17]]; Rewrite H17; Change (f x)==(pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i); Rewrite RList_P12. Induction i. -Simpl; Assert H18 := (H8 O); Unfold constant_D_eq open_interval in H18; Assert H19 : (lt O (pred (longueur l1))). +Simpl; Assert H18 := (H8 O); Unfold constant_D_eq open_interval in H18; Assert H19 : (lt O (pred (Rlength l1))). Rewrite H17; Simpl; Apply lt_O_Sn. Assert H20 := (H18 H19); Repeat Rewrite H20. Reflexivity. @@ -1023,7 +1023,7 @@ Rewrite H17; Simpl; Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; R Elim H2; Intros; Rewrite H17 in H23; Rewrite H17 in H24; Simpl in H24; Simpl in H23; Rewrite H22 in H23; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H23 H24)). Assumption. Clear Hreci; Rewrite RList_P13. -Rewrite H17 in H14; Rewrite H17 in H15; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) i)== (pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; Rewrite H14; Change (pos_Rl (cons_Rlist (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 : (lt (S i) (pred (longueur l1))). +Rewrite H17 in H14; Rewrite H17 in H15; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) i)== (pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; Rewrite H14; Change (pos_Rl (cons_Rlist (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 : (lt (S i) (pred (Rlength l1))). Apply lt_pred; Apply lt_S_n; Apply le_lt_n_Sm; Assumption. Assert H20 := (H18 H19); Repeat Rewrite H20. Reflexivity. @@ -1047,22 +1047,22 @@ Simpl in H15; Discriminate. Clear Hrecl1; Simpl in H1; Simpl; Apply lt_n_S; Assumption. Assert H17 : (pos_Rl (cons_Rlist l1 l2) i)==b. Rewrite RList_P26. -Replace i with (pred (longueur l1)); [Rewrite H4; Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Left; Assumption] | Rewrite H15; Reflexivity]. +Replace i with (pred (Rlength l1)); [Rewrite H4; Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n; Left; Assumption] | Rewrite H15; Reflexivity]. Rewrite H15; Apply lt_n_Sn. Rewrite H16 in H2; Rewrite H17 in H2; Elim H2; Intros; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H14 H18)). -Assert H16 : (pos_Rl (cons_Rlist l1 l2) i) == (pos_Rl l2 (minus i (longueur l1))). +Assert H16 : (pos_Rl (cons_Rlist l1 l2) i) == (pos_Rl l2 (minus i (Rlength l1))). Apply RList_P29. Apply le_S_n; Assumption. -Apply lt_le_trans with (pred (longueur (cons_Rlist l1 l2))); [Assumption | Apply le_pred_n]. -Assert H17 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l2 (S (minus i (longueur l1)))). -Replace (S (minus i (longueur l1))) with (minus (S i) (longueur l1)). +Apply lt_le_trans with (pred (Rlength (cons_Rlist l1 l2))); [Assumption | Apply le_pred_n]. +Assert H17 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l2 (S (minus i (Rlength l1)))). +Replace (S (minus i (Rlength l1))) with (minus (S i) (Rlength l1)). Apply RList_P29. Apply le_S_n; Apply le_trans with (S i); [Assumption | Apply le_n_Sn]. Induction l1. Simpl in H6; Discriminate. Clear Hrecl1; Simpl in H1; Simpl; Apply lt_n_S; Assumption. Symmetry; Apply minus_Sn_m; Apply le_S_n; Assumption. -Assert H18 : (le (2) (longueur l1)). +Assert H18 : (le (2) (Rlength l1)). 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. Discriminate. Clear Hrecl1; Induction l1. @@ -1074,29 +1074,29 @@ Elim (RList_P20 ? H18); Intros r1 [r2 [r3 H19]]; Rewrite H19; Change (f x)==(pos Induction i. Assert H20 := (le_S_n ? ? H15); Assert H21 := (le_trans ? ? ? H18 H20); Elim (le_Sn_O ? H21). Clear Hreci; Rewrite RList_P13. -Rewrite H19 in H16; Rewrite H19 in H17; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) i)== (pos_Rl l2 (minus (S i) (longueur (cons r1 (cons r2 r3))))) in H16; Rewrite H16; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i))== (pos_Rl l2 (S (minus (S i) (longueur (cons r1 (cons r2 r3)))))) in H17; Rewrite H17; Assert H20 := (H13 (minus (S i) (longueur l1))); Unfold constant_D_eq open_interval in H20; Assert H21 : (lt (minus (S i) (longueur l1)) (pred (longueur l2))). +Rewrite H19 in H16; Rewrite H19 in H17; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) i)== (pos_Rl l2 (minus (S i) (Rlength (cons r1 (cons r2 r3))))) in H16; Rewrite H16; Change (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i))== (pos_Rl l2 (S (minus (S i) (Rlength (cons r1 (cons r2 r3)))))) in H17; Rewrite H17; Assert H20 := (H13 (minus (S i) (Rlength l1))); Unfold constant_D_eq open_interval in H20; Assert H21 : (lt (minus (S i) (Rlength l1)) (pred (Rlength l2))). Apply lt_pred; Rewrite minus_Sn_m. -Apply simpl_lt_plus_l with (longueur l1); Rewrite <- le_plus_minus. +Apply simpl_lt_plus_l with (Rlength l1); Rewrite <- le_plus_minus. Rewrite H19 in H1; Simpl in H1; Rewrite H19; Simpl; Rewrite RList_P23 in H1; Apply lt_n_S; Assumption. Apply le_trans with (S i); [Apply le_S_n; Assumption | Apply le_n_Sn]. Apply le_S_n; Assumption. Assert H22 := (H20 H21); Repeat Rewrite H22. Reflexivity. -Rewrite <- H19; Assert H23 : ``(pos_Rl l2 (minus (S i) (longueur l1)))<=(pos_Rl l2 (S (minus (S i) (longueur l1))))``. +Rewrite <- H19; Assert H23 : ``(pos_Rl l2 (minus (S i) (Rlength l1)))<=(pos_Rl l2 (S (minus (S i) (Rlength l1))))``. Apply H7; Apply lt_pred. Rewrite minus_Sn_m. -Apply simpl_lt_plus_l with (longueur l1); Rewrite <- le_plus_minus. +Apply simpl_lt_plus_l with (Rlength l1); Rewrite <- le_plus_minus. Rewrite H19 in H1; Simpl in H1; Rewrite H19; Simpl; Rewrite RList_P23 in H1; Apply lt_n_S; Assumption. Apply le_trans with (S i); [Apply le_S_n; Assumption | Apply le_n_Sn]. Apply le_S_n; Assumption. Elim H23; Intro. Split. Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. -Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite (Rplus_sym (pos_Rl l2 (minus (S i) (longueur l1)))); Rewrite double; Apply Rlt_compatibility; Assumption | DiscrR]]. +Apply Rlt_monotony_contra with ``2``; [Sup0 | Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1l; Rewrite (Rplus_sym (pos_Rl l2 (minus (S i) (Rlength l1)))); Rewrite double; Apply Rlt_compatibility; 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_antirefl ? (Rlt_trans ? ? ? H25 H26)). -Assert H23 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l2 (minus (S i) (longueur l1))). +Assert H23 : (pos_Rl (cons_Rlist l1 l2) (S i))==(pos_Rl l2 (minus (S i) (Rlength l1))). Rewrite H19; Simpl; Simpl in H16; Apply H16. -Assert H24 : (pos_Rl (cons_Rlist l1 l2) (S (S i)))==(pos_Rl l2 (S (minus (S i) (longueur l1)))). +Assert H24 : (pos_Rl (cons_Rlist l1 l2) (S (S i)))==(pos_Rl l2 (S (minus (S i) (Rlength l1)))). Rewrite H19; Simpl; Simpl in H17; Apply H17. Rewrite <- H23; Rewrite <- H24; Assumption. Simpl; Rewrite H19 in H1; Simpl in H1; Apply lt_S_n; Assumption. @@ -1115,7 +1115,7 @@ Split with l2; Split with lf2; Rewrite <- b0 in H2; Assumption. Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)). Qed. -Lemma StepFun_P42 : (l1,l2:Rlist;f:R->R) (pos_Rl l1 (pred (longueur l1)))==(pos_Rl l2 O) -> ``(Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)) == (Int_SF (FF l1 f) l1) + (Int_SF (FF l2 f) l2)``. +Lemma StepFun_P42 : (l1,l2:Rlist;f:R->R) (pos_Rl l1 (pred (Rlength l1)))==(pos_Rl l2 O) -> ``(Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)) == (Int_SF (FF l1 f) l1) + (Int_SF (FF l2 f) l2)``. Induction l1; [Intros; Simpl; Ring | Induction r0; [Intros; Simpl in H0; Simpl; Induction l2; [Simpl; Ring | Simpl; Simpl in H0; Rewrite H0; Ring] | Intros; Simpl; Rewrite Rplus_assoc; Apply Rplus_plus_r; Apply (H0 l2 f); Rewrite <- H1; Reflexivity]]. Qed. @@ -1291,7 +1291,7 @@ Rewrite H6; Unfold ordered_Rlist; Intros; Simpl in H8; Inversion H8; [Simpl; Ass Simpl; Unfold Rmin; Case (total_order_Rle a c); Intro; [Assumption | Elim n; Assumption]. Simpl; Unfold Rmax; Case (total_order_Rle a c); Intro; [Reflexivity | Elim n; Assumption]. Unfold constant_D_eq open_interval; Intros; Simpl in H8; Inversion H8. -Simpl; Assert H10 := (H7 O); Assert H12 : (lt (0) (pred (longueur (cons r (cons r1 r2))))). +Simpl; Assert H10 := (H7 O); Assert H12 : (lt (0) (pred (Rlength (cons r (cons r1 r2))))). Simpl; Apply lt_O_Sn. Apply (H10 H12); Unfold open_interval; Simpl; Rewrite H11 in H9; Simpl in H9; Elim H9; Clear H9; Intros; Split; Try Assumption. Apply Rlt_le_trans with c; Assumption. @@ -1318,7 +1318,7 @@ Rewrite <- H11; Reflexivity. Unfold Rmax; Case (total_order_Rle r1 c); Case (total_order_Rle a c); Intros; [Reflexivity | Elim n; Elim H0; Intros; Assumption | Elim n; Left; Assumption | Elim n0; Left; Assumption]. Simpl; Simpl in H13; Rewrite H13; Reflexivity. Intros; Simpl in H; Unfold constant_D_eq open_interval; Intros; Induction i. -Simpl; Assert H17 := (H10 O); Assert H18 : (lt (0) (pred (longueur (cons r (cons r1 r2))))). +Simpl; Assert H17 := (H10 O); Assert H18 : (lt (0) (pred (Rlength (cons r (cons r1 r2))))). Simpl; Apply lt_O_Sn. Apply (H17 H18); Unfold open_interval; Simpl; Simpl in H4; Elim H4; Clear H4; Intros; Split; Try Assumption; Replace r1 with r4. Assumption. |