diff options
| author | Yves Bertot | 2020-01-16 13:28:28 +0100 |
|---|---|---|
| committer | Yves Bertot | 2020-02-06 17:53:31 +0100 |
| commit | 0fe99a0d6a4d643cf311200c870aeaff042d7069 (patch) | |
| tree | 4140ca1e18e3918385c263ca31db2dae8fff1ef3 | |
| parent | c6e89e2b13d7fa99aaaaf02fc3430ae6c5f00beb (diff) | |
replace RList by list R
add an overlay for coquelicot
remove functions from RList: In, Rlength, cons_Rlist, app_RList
because they are essentially the same as In, length, app, and map from List
(beware that the order of arguments changes for map, and the In function
contains reversed equalities).
adds deprecation warnings for Rlist and Rlength
adds deprecated notations for RList.cons and RList.nil
| -rw-r--r-- | doc/changelog/10-standard-library/11404-removeRList.rst | 15 | ||||
| -rw-r--r-- | theories/Reals/RList.v | 496 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt.v | 38 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 342 | ||||
| -rw-r--r-- | theories/Reals/Rtopology.v | 20 |
5 files changed, 451 insertions, 460 deletions
diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst new file mode 100644 index 0000000000..88e22d128c --- /dev/null +++ b/doc/changelog/10-standard-library/11404-removeRList.rst @@ -0,0 +1,15 @@ +- **Removed:** + Type `RList` has been removed. All uses have been replaced by `list R`. + Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` + have also been removed as they are essentially the same as `In`, `length`, + `app`, and `map` from `List`, modulo the following changes: + + - `RList.In x (RList.cons a l)` used to be convertible to + `(x = a) \\/ RList.In x l`, + but `List.In x (a :: l)` is convertible to + `(a = x) \\/ List.In l`. + The equality is reversed. + - `app_Rlist` and `List.map` take arguments in different order. + + (`#11404 <https://github.com/coq/coq/pull/11404>`_, + by Yves Bertot). diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 128543d8ab..18cc3aa034 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -8,98 +8,90 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import List. Require Import Rbase. Require Import Rfunctions. Local Open Scope R_scope. -Inductive Rlist : Type := -| nil : Rlist -| cons : R -> Rlist -> Rlist. -Fixpoint In (x:R) (l:Rlist) : Prop := - match l with - | nil => False - | cons a l' => x = a \/ In x l' - end. +#[deprecated(since="8.12",note="use (list R) instead")] +Notation Rlist := (list R). -Fixpoint Rlength (l:Rlist) : nat := - match l with - | nil => 0%nat - | cons a l' => S (Rlength l') - end. +#[deprecated(since="8.12",note="use List.length instead")] +Notation Rlength := List.length. -Fixpoint MaxRlist (l:Rlist) : R := +Fixpoint MaxRlist (l:list R) : R := match l with | nil => 0 - | cons a l1 => + | a :: l1 => match l1 with | nil => a - | cons a' l2 => Rmax a (MaxRlist l1) + | a' :: l2 => Rmax a (MaxRlist l1) end end. -Fixpoint MinRlist (l:Rlist) : R := +Fixpoint MinRlist (l:list R) : R := match l with | nil => 1 - | cons a l1 => + | a :: l1 => match l1 with | nil => a - | cons a' l2 => Rmin a (MinRlist l1) + | a' :: l2 => Rmin a (MinRlist l1) end end. -Lemma MaxRlist_P1 : forall (l:Rlist) (x:R), In x l -> x <= MaxRlist l. +Lemma MaxRlist_P1 : forall (l:list R) (x:R), In x l -> x <= MaxRlist l. Proof. intros; induction l as [| r l Hrecl]. simpl in H; elim H. induction l as [| r0 l Hrecl0]. simpl in H; elim H; intro. - simpl; right; assumption. + simpl; right; symmetry; assumption. elim H0. - replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))). + replace (MaxRlist (r :: r0 :: l)) with (Rmax r (MaxRlist (r0 :: l))). simpl in H; decompose [or] H. rewrite H0; apply RmaxLess1. - unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro. + unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. apply Hrecl; simpl; tauto. - apply Rle_trans with (MaxRlist (cons r0 l)); + apply Rle_trans with (MaxRlist (r0 :: l)); [ apply Hrecl; simpl; tauto | left; auto with real ]. - unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro. + unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. apply Hrecl; simpl; tauto. - apply Rle_trans with (MaxRlist (cons r0 l)); + apply Rle_trans with (MaxRlist (r0 :: l)); [ apply Hrecl; simpl; tauto | left; auto with real ]. reflexivity. Qed. -Fixpoint AbsList (l:Rlist) (x:R) : Rlist := +Fixpoint AbsList (l:list R) (x:R) : list R := match l with | nil => nil - | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x) + | a :: l' => (Rabs (a - x) / 2) :: (AbsList l' x) end. -Lemma MinRlist_P1 : forall (l:Rlist) (x:R), In x l -> MinRlist l <= x. +Lemma MinRlist_P1 : forall (l:list R) (x:R), In x l -> MinRlist l <= x. Proof. intros; induction l as [| r l Hrecl]. simpl in H; elim H. induction l as [| r0 l Hrecl0]. simpl in H; elim H; intro. - simpl; right; symmetry ; assumption. + simpl; right; assumption. elim H0. - replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). + replace (MinRlist (r :: r0 :: l)) with (Rmin r (MinRlist (r0 :: l))). simpl in H; decompose [or] H. rewrite H0; apply Rmin_l. - unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro. - apply Rle_trans with (MinRlist (cons r0 l)). + unfold Rmin; case (Rle_dec r (MinRlist (r0 :: l))); intro. + apply Rle_trans with (MinRlist (r0 :: l)). assumption. apply Hrecl; simpl; tauto. apply Hrecl; simpl; tauto. - apply Rle_trans with (MinRlist (cons r0 l)). + apply Rle_trans with (MinRlist (r0 :: l)). apply Rmin_r. apply Hrecl; simpl; tauto. reflexivity. Qed. Lemma AbsList_P1 : - forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x). + forall (l:list R) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x). Proof. intros; induction l as [| r l Hrecl]. elim H. @@ -109,21 +101,21 @@ Proof. Qed. Lemma MinRlist_P2 : - forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l. + forall l:list R, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l. Proof. intros; induction l as [| r l Hrecl]. apply Rlt_0_1. induction l as [| r0 l Hrecl0]. simpl; apply H; simpl; tauto. - replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). - unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro. + replace (MinRlist (r :: r0 :: l)) with (Rmin r (MinRlist (r0 :: l))). + unfold Rmin; case (Rle_dec r (MinRlist (r0 :: l))); intro. apply H; simpl; tauto. apply Hrecl; intros; apply H; simpl; simpl in H0; tauto. reflexivity. Qed. Lemma AbsList_P2 : - forall (l:Rlist) (x y:R), + forall (l:list R) (x y:R), In y (AbsList l x) -> exists z : R, In z l /\ y = Rabs (z - x) / 2. Proof. intros; induction l as [| r l Hrecl]. @@ -131,47 +123,48 @@ Proof. elim H; intro. exists r; split. simpl; tauto. + symmetry. assumption. assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros; exists x0; simpl; simpl in H2; tauto. Qed. Lemma MaxRlist_P2 : - forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l. + forall l:list R, (exists y : R, In y l) -> In (MaxRlist l) l. Proof. intros; induction l as [| r l Hrecl]. simpl in H; elim H; trivial. induction l as [| r0 l Hrecl0]. simpl; left; reflexivity. - change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))); - unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); + change (In (Rmax r (MaxRlist (r0 :: l))) (r :: r0 :: l)); + unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. right; apply Hrecl; exists r0; left; reflexivity. left; reflexivity. Qed. -Fixpoint pos_Rl (l:Rlist) (i:nat) : R := +Fixpoint pos_Rl (l:list R) (i:nat) : R := match l with | nil => 0 - | cons a l' => match i with + | a :: l' => match i with | O => a | S i' => pos_Rl l' i' end end. Lemma pos_Rl_P1 : - forall (l:Rlist) (a:R), - (0 < Rlength l)%nat -> - pos_Rl (cons a l) (Rlength l) = pos_Rl l (pred (Rlength l)). + forall (l:list R) (a:R), + (0 < length l)%nat -> + pos_Rl (a :: l) (length l) = pos_Rl l (pred (length l)). Proof. intros; induction l as [| r l Hrecl]; [ elim (lt_n_O _ H) - | simpl; case (Rlength l); [ reflexivity | intro; reflexivity ] ]. + | simpl; case (length l); [ reflexivity | intro; reflexivity ] ]. Qed. Lemma pos_Rl_P2 : - forall (l:Rlist) (x:R), - In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i). + forall (l:list R) (x:R), + In x l <-> (exists i : nat, (i < length l)%nat /\ x = pos_Rl l i). Proof. intros; induction l as [| r l Hrecl]. split; intro; @@ -179,12 +172,12 @@ Proof. split; intro. elim H; intro. exists 0%nat; split; - [ simpl; apply lt_O_Sn | simpl; apply H0 ]. + [ simpl; apply lt_O_Sn | simpl; symmetry; apply H0 ]. elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros; exists (S x0); split; [ simpl; apply lt_n_S; assumption | simpl; assumption ]. elim H; intros; elim H0; intros; destruct (zerop x0) as [->|]. - simpl in H2; left; assumption. + simpl in H2; left; symmetry; assumption. right; elim Hrecl; intros H4 H5; apply H5; assert (H6 : S (pred x0) = x0). symmetry ; apply S_pred with 0%nat; assumption. exists (pred x0); split; @@ -193,21 +186,21 @@ Proof. Qed. Lemma Rlist_P1 : - forall (l:Rlist) (P:R -> R -> Prop), + forall (l:list R) (P:R -> R -> Prop), (forall x:R, In x l -> exists y : R, P x y) -> - exists l' : Rlist, - Rlength l = Rlength l' /\ - (forall i:nat, (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i)). + exists l' : list R, + length l = length l' /\ + (forall i:nat, (i < length l)%nat -> P (pos_Rl l i) (pos_Rl l' i)). Proof. intros; induction l as [| r l Hrecl]. exists nil; intros; split; [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ]. - assert (H0 : In r (cons r l)). + assert (H0 : In r (r :: l)). simpl; left; reflexivity. assert (H1 := H _ H0); assert (H2 : forall x:R, In x l -> exists y : R, P x y). intros; apply H; simpl; right; assumption. - assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0); + assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (x :: x0); intros; elim H5; clear H5; intros; split. simpl; rewrite H5; reflexivity. intros; destruct (zerop i) as [->|]. @@ -218,57 +211,45 @@ Proof. assumption. Qed. -Definition ordered_Rlist (l:Rlist) : Prop := - forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <= pos_Rl l (S i). +Definition ordered_Rlist (l:list R) : Prop := + forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <= pos_Rl l (S i). -Fixpoint insert (l:Rlist) (x:R) : Rlist := +Fixpoint insert (l:list R) (x:R) : list R := match l with - | nil => cons x nil - | cons a l' => + | nil => x :: nil + | a :: l' => match Rle_dec a x with - | left _ => cons a (insert l' x) - | right _ => cons x l + | left _ => a :: (insert l' x) + | right _ => x :: l end end. -Fixpoint cons_Rlist (l k:Rlist) : Rlist := - match l with - | nil => k - | cons a l' => cons a (cons_Rlist l' k) - end. - -Fixpoint cons_ORlist (k l:Rlist) : Rlist := +Fixpoint cons_ORlist (k l:list R) : list R := match k with | nil => l - | cons a k' => cons_ORlist k' (insert l a) + | a :: k' => cons_ORlist k' (insert l a) end. -Fixpoint app_Rlist (l:Rlist) (f:R -> R) : Rlist := +Fixpoint mid_Rlist (l:list R) (x:R) : list R := match l with | nil => nil - | cons a l' => cons (f a) (app_Rlist l' f) + | a :: l' => ((x + a) / 2) :: (mid_Rlist l' a) end. -Fixpoint mid_Rlist (l:Rlist) (x:R) : Rlist := +Definition Rtail (l:list R) : list R := match l with | nil => nil - | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a) + | a :: l' => l' end. -Definition Rtail (l:Rlist) : Rlist := +Definition FF (l:list R) (f:R -> R) : list R := match l with | nil => nil - | cons a l' => l' - end. - -Definition FF (l:Rlist) (f:R -> R) : Rlist := - match l with - | nil => nil - | cons a l' => app_Rlist (mid_Rlist l' a) f + | a :: l' => map f (mid_Rlist l' a) end. Lemma RList_P0 : - forall (l:Rlist) (a:R), + forall (l:list R) (a:R), pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0. Proof. intros; induction l as [| r l Hrecl]; @@ -278,7 +259,7 @@ Proof. Qed. Lemma RList_P1 : - forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a). + forall (l:list R) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a). Proof. intros; induction l as [| r l Hrecl]. simpl; unfold ordered_Rlist; intros; simpl in H0; @@ -286,8 +267,8 @@ Proof. simpl; case (Rle_dec r a); intro. assert (H1 : ordered_Rlist l). unfold ordered_Rlist; unfold ordered_Rlist in H; intros; - assert (H1 : (S i < pred (Rlength (cons r l)))%nat); - [ simpl; replace (Rlength l) with (S (pred (Rlength l))); + assert (H1 : (S i < pred (length (r :: l)))%nat); + [ simpl; replace (length l) with (S (pred (length l))); [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ] @@ -300,18 +281,18 @@ Proof. [ simpl; assumption | rewrite H4; apply (H 0%nat); simpl; apply lt_O_Sn ]. simpl; apply H2; simpl in H0; apply lt_S_n; - replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a)); + replace (S (pred (length (insert l a)))) with (length (insert l a)); [ assumption | apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H3 in H0; elim (lt_n_O _ H0) ]. unfold ordered_Rlist; intros; induction i as [| i Hreci]; [ simpl; auto with real - | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)); apply H; + | change (pos_Rl (r :: l) i <= pos_Rl (r :: l) (S i)); apply H; simpl in H0; simpl; apply (lt_S_n _ _ H0) ]. Qed. Lemma RList_P2 : - forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2). + forall l1 l2:list R, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2). Proof. simple induction l1; [ intros; simpl; apply H @@ -319,36 +300,36 @@ Proof. Qed. Lemma RList_P3 : - forall (l:Rlist) (x:R), - In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat). + forall (l:list R) (x:R), + In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < length l)%nat). Proof. intros; split; intro; [ induction l as [| r l Hrecl] | induction l as [| r l Hrecl] ]. elim H. elim H; intro; - [ exists 0%nat; split; [ apply H0 | simpl; apply lt_O_Sn ] + [ exists 0%nat; split; [ symmetry; 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 ] ]. elim H; intros; elim H0; intros; elim (lt_n_O _ H2). simpl; elim H; intros; elim H0; clear H0; intros; induction x0 as [| x0 Hrecx0]; - [ left; apply H0 + [ left; symmetry; apply H0 | right; apply Hrecl; exists x0; split; [ apply H0 | simpl in H1; apply lt_S_n; assumption ] ]. Qed. Lemma RList_P4 : - forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1. + forall (l1:list R) (a:R), ordered_Rlist (a :: l1) -> ordered_Rlist l1. Proof. intros; unfold ordered_Rlist; intros; apply (H (S i)); simpl; - replace (Rlength l1) with (S (pred (Rlength l1))); + replace (length l1) with (S (pred (length l1))); [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ]. Qed. Lemma RList_P5 : - forall (l:Rlist) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x. + forall (l:list R) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x. Proof. intros; induction l as [| r l Hrecl]; [ elim H0 @@ -361,14 +342,14 @@ Proof. Qed. Lemma RList_P6 : - forall l:Rlist, + forall l:list R, ordered_Rlist l <-> (forall i j:nat, - (i <= j)%nat -> (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j). + (i <= j)%nat -> (j < length l)%nat -> pos_Rl l i <= pos_Rl l j). Proof. - simple induction l; split; intro. + induction l as [ | r r0 H]; split; intro. intros; right; reflexivity. - unfold ordered_Rlist; intros; simpl in H0; elim (lt_n_O _ H0). + unfold ordered_Rlist;intros; simpl in H0; elim (lt_n_O _ H0). intros; induction i as [| i Hreci]; [ induction j as [| j Hrecj]; [ right; reflexivity @@ -391,14 +372,14 @@ Proof. Qed. Lemma RList_P7 : - forall (l:Rlist) (x:R), - ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)). + forall (l:list R) (x:R), + ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (length l)). Proof. 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))). + assert (H6 : length l = S (pred (length l))). apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H6 in H5; elim (lt_n_O _ H5). apply H3; @@ -408,52 +389,55 @@ Proof. Qed. Lemma RList_P8 : - forall (l:Rlist) (a x:R), In x (insert l a) <-> x = a \/ In x l. -Proof. - simple induction l. - intros; split; intro; simpl in H; apply H. - intros; split; intro; - [ simpl in H0; generalize H0; case (Rle_dec r a); intros; - [ simpl in H1; elim H1; intro; - [ right; left; assumption - | elim (H a x); intros; elim (H3 H2); intro; - [ left; assumption | right; right; assumption ] ] - | simpl in H1; decompose [or] H1; - [ left; assumption - | right; left; assumption - | right; right; assumption ] ] - | simpl; case (Rle_dec r a); intro; - [ simpl in H0; decompose [or] H0; - [ right; elim (H a x); intros; apply H3; left - | left - | right; elim (H a x); intros; apply H3; right ] - | simpl in H0; decompose [or] H0; [ left | right; left | right; right ] ]; - assumption ]. + forall (l:list R) (a x:R), In x (insert l a) <-> x = a \/ In x l. +Proof. + induction l as [ | r r0 H]. + intros; split; intro; destruct H as [ax | []]; left; symmetry; exact ax. + intros; split; intro. + simpl in H0; generalize H0; case (Rle_dec r a); intros. + simpl in H1; elim H1; intro. + right; left; assumption. + elim (H a x); intros; elim (H3 H2); intro. + left; assumption. + right; right; assumption. + simpl in H1; decompose [or] H1. + left; symmetry; assumption. + right; left; assumption. + right; right; assumption. + simpl; case (Rle_dec r a); intro. + simpl in H0; decompose [or] H0. + right; elim (H a x); intros; apply H3; left. assumption. + left. assumption. + right; elim (H a x); intros; apply H3; right; assumption. + simpl in H0; decompose [or] H0; [ left | right; left | right; right]; + trivial; symmetry; assumption. Qed. Lemma RList_P9 : - forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2. + forall (l1 l2:list R) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2. Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; split; intro; [ simpl in H; right; assumption | simpl; elim H; intro; [ elim H0 | assumption ] ]. intros; split. simpl; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0); - elim H3; intro; - [ left; right; assumption - | elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro; - [ left; left; assumption | right; assumption ] ]. + elim H3; intro. + left; right; assumption. + elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro. + left; left; symmetry; assumption. + right; assumption. 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 ]. + elim H0; intro. + elim H2; intro. + right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left. + symmetry; assumption. + left; assumption. + right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption. Qed. Lemma RList_P10 : - forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l). + forall (l:list R) (a:R), length (insert l a) = S (length l). Proof. intros; induction l as [| r l Hrecl]; [ reflexivity @@ -462,10 +446,10 @@ Proof. Qed. Lemma RList_P11 : - forall l1 l2:Rlist, - Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat. + forall l1 l2:list R, + length (cons_ORlist l1 l2) = (length l1 + length l2)%nat. Proof. - simple induction l1; + induction l1 as [ | r r0 H]; [ intro; reflexivity | intros; simpl; rewrite (H (insert l2 r)); rewrite RList_P10; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; @@ -473,8 +457,8 @@ Proof. Qed. Lemma RList_P12 : - forall (l:Rlist) (i:nat) (f:R -> R), - (i < Rlength l)%nat -> pos_Rl (app_Rlist l f) i = f (pos_Rl l i). + forall (l:list R) (i:nat) (f:R -> R), + (i < length l)%nat -> pos_Rl (map f l) i = f (pos_Rl l i). Proof. simple induction l; [ intros; elim (lt_n_O _ H) @@ -483,30 +467,30 @@ Proof. Qed. Lemma RList_P13 : - forall (l:Rlist) (i:nat) (a:R), - (i < pred (Rlength l))%nat -> + forall (l:list R) (i:nat) (a:R), + (i < pred (length l))%nat -> pos_Rl (mid_Rlist l a) (S i) = (pos_Rl l i + pos_Rl l (S i)) / 2. Proof. - simple induction l. + induction l as [ | r r0 H]. intros; simpl in H; elim (lt_n_O _ H). - simple induction r0. + induction r0 as [ | r1 r2 H0]. intros; simpl in H0; elim (lt_n_O _ H0). intros; simpl in H1; induction i as [| i Hreci]. 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. + (pos_Rl (mid_Rlist (r1 :: r2) r) (S i) = + (pos_Rl (r1 :: r2) i + pos_Rl (r1 :: r2) (S i)) / 2). + apply H; simpl; apply lt_S_n; assumption. Qed. -Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l. +Lemma RList_P14 : forall (l:list R) (a:R), length (mid_Rlist l a) = length l. Proof. - simple induction l; intros; + induction l as [ | r r0 H]; intros; [ reflexivity | simpl; rewrite (H r); reflexivity ]. Qed. Lemma RList_P15 : - forall l1 l2:Rlist, + forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> pos_Rl l1 0 = pos_Rl l2 0 -> pos_Rl (cons_ORlist l1 l2) 0 = pos_Rl l1 0. @@ -514,10 +498,10 @@ Proof. intros; apply Rle_antisym. induction l1 as [| r l1 Hrecl1]; [ simpl; simpl in H1; right; symmetry ; assumption - | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros; + | elim (RList_P9 (r :: l1) l2 (pos_Rl (r :: l1) 0)); intros; assert (H4 : - In (pos_Rl (cons r l1) 0) (cons r l1) \/ In (pos_Rl (cons r l1) 0) l2); + In (pos_Rl (r :: l1) 0) (r :: l1) \/ In (pos_Rl (r :: l1) 0) l2); [ left; left; reflexivity | assert (H5 := H3 H4); apply RList_P5; [ apply RList_P2; assumption | assumption ] ] ]. @@ -525,25 +509,25 @@ Proof. [ simpl; simpl in H1; right; assumption | assert (H2 : - In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2)); + In (pos_Rl (cons_ORlist (r :: l1) l2) 0) (cons_ORlist (r :: l1) l2)); [ elim - (RList_P3 (cons_ORlist (cons r l1) l2) - (pos_Rl (cons_ORlist (cons r l1) l2) 0)); + (RList_P3 (cons_ORlist (r :: l1) l2) + (pos_Rl (cons_ORlist (r :: l1) l2) 0)); intros; apply H3; exists 0%nat; 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)); + | elim (RList_P9 (r :: l1) l2 (pos_Rl (cons_ORlist (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 : - forall l1 l2:Rlist, + forall l1 l2:list R, 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)). + pos_Rl l1 (pred (length l1)) = pos_Rl l2 (pred (length l2)) -> + pos_Rl (cons_ORlist l1 l2) (pred (length (cons_ORlist l1 l2))) = + pos_Rl l1 (pred (length l1)). Proof. intros; apply Rle_antisym. induction l1 as [| r l1 Hrecl1]. @@ -551,99 +535,99 @@ Proof. 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)); + (pos_Rl (cons_ORlist (r :: l1) l2) + (pred (length (cons_ORlist (r :: l1) l2)))) + (cons_ORlist (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))); + (RList_P3 (cons_ORlist (r :: l1) l2) + (pos_Rl (cons_ORlist (r :: l1) l2) + (pred (length (cons_ORlist (r :: l1) l2))))); + intros; apply H3; exists (pred (length (cons_ORlist (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))))); + (RList_P9 (r :: l1) l2 + (pos_Rl (cons_ORlist (r :: l1) l2) + (pred (length (cons_ORlist (r :: l1) l2))))); intros; assert (H5 := H3 H2); elim H5; intro; [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ]. induction l1 as [| r l1 Hrecl1]. simpl; simpl in H1; right; assumption. elim - (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); + (RList_P9 (r :: l1) l2 (pos_Rl (r :: l1) (pred (length (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; + In (pos_Rl (r :: l1) (pred (length (r :: l1)))) (r :: l1) \/ + In (pos_Rl (r :: l1) (pred (length (r :: l1)))) l2); + [ left; change (In (pos_Rl (r :: l1) (length l1)) (r :: l1)); + elim (RList_P3 (r :: l1) (pos_Rl (r :: l1) (length l1))); + intros; apply H5; exists (length 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))))); + (RList_P9 (r :: l1) l2 + (pos_Rl (r :: l1) (pred (length (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))); + (RList_P3 (r :: l1) + (pos_Rl (r :: l1) (pred (length (r :: l1))))); + intros; apply H9; exists (pred (length (r :: l1))); split; [ reflexivity | simpl; apply lt_n_Sn ] ] ]. Qed. Lemma RList_P17 : - forall (l1:Rlist) (x:R) (i:nat), + forall (l1:list R) (x:R) (i:nat), ordered_Rlist l1 -> In x l1 -> - pos_Rl l1 i < x -> (i < pred (Rlength l1))%nat -> pos_Rl l1 (S i) <= x. + pos_Rl l1 i < x -> (i < pred (length l1))%nat -> pos_Rl l1 (S i) <= x. Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; elim H0. intros; induction i as [| i Hreci]. simpl; elim H1; intro; [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ 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); + rewrite <- H4 in H2; assert (H5 : r <= pos_Rl r0 i); [ apply Rle_trans with (pos_Rl r0 0); [ apply (H0 0%nat); 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); + | simpl in H3; apply lt_S_n; apply lt_trans with (length r0); [ apply H3 | apply lt_n_Sn ] ] ] | elim (Rlt_irrefl _ (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); + replace (S (pred (length r0))) with (length r0); [ apply H3 | apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ]. Qed. Lemma RList_P18 : - forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l. + forall (l:list R) (f:R -> R), length (map f l) = length l. Proof. simple induction l; intros; [ reflexivity | simpl; rewrite H; reflexivity ]. Qed. Lemma RList_P19 : - forall l:Rlist, - l <> nil -> exists r : R, (exists r0 : Rlist, l = cons r r0). + forall l:list R, + l <> nil -> exists r : R, (exists r0 : list R, l = r :: r0). Proof. intros; induction l as [| r l Hrecl]; [ elim H; reflexivity | exists r; exists l; reflexivity ]. Qed. Lemma RList_P20 : - forall l:Rlist, - (2 <= Rlength l)%nat -> + forall l:list R, + (2 <= length l)%nat -> exists r : R, - (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). + (exists r1 : R, (exists l' : list R, l = r :: r1 :: l')). Proof. intros; induction l as [| r l Hrecl]; [ simpl in H; elim (le_Sn_O _ H) @@ -652,40 +636,32 @@ Proof. | exists r; exists r0; exists l; reflexivity ] ]. Qed. -Lemma RList_P21 : forall l l':Rlist, l = l' -> Rtail l = Rtail l'. +Lemma RList_P21 : forall l l':list R, l = l' -> Rtail l = Rtail l'. Proof. intros; rewrite H; reflexivity. Qed. Lemma RList_P22 : - forall l1 l2:Rlist, l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0. + forall l1 l2:list R, l1 <> nil -> pos_Rl (app l1 l2) 0 = pos_Rl l1 0. Proof. simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ]. Qed. -Lemma RList_P23 : - forall l1 l2:Rlist, - Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat. -Proof. - simple induction l1; - [ intro; reflexivity | intros; simpl; rewrite H; reflexivity ]. -Qed. - Lemma RList_P24 : - forall l1 l2:Rlist, + forall l1 l2:list R, l2 <> nil -> - pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2))) = - pos_Rl l2 (pred (Rlength l2)). + pos_Rl (app l1 l2) (pred (length (app l1 l2))) = + pos_Rl l2 (pred (length l2)). Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; reflexivity. intros; rewrite <- (H l2 H0); induction l2 as [| r1 l2 Hrecl2]. elim H0; reflexivity. - do 2 rewrite RList_P23; - replace (Rlength (cons r r0) + Rlength (cons r1 l2))%nat with - (S (S (Rlength r0 + Rlength l2))); - [ replace (Rlength r0 + Rlength (cons r1 l2))%nat with - (S (Rlength r0 + Rlength l2)); + do 2 rewrite app_length; + replace (length (r :: r0) + length (r1 :: l2))%nat with + (S (S (length r0 + length l2))); + [ replace (length r0 + length (r1 :: l2))%nat with + (S (length r0 + length l2)); [ reflexivity | simpl; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring ] @@ -694,39 +670,39 @@ Proof. Qed. Lemma RList_P25 : - forall l1 l2:Rlist, + forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> - pos_Rl l1 (pred (Rlength l1)) <= pos_Rl l2 0 -> - ordered_Rlist (cons_Rlist l1 l2). + pos_Rl l1 (pred (length l1)) <= pos_Rl l2 0 -> + ordered_Rlist (app l1 l2). Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; simpl; assumption. - simple induction r0. + induction r0 as [ | r1 r2 H0]. intros; simpl; simpl in H2; unfold ordered_Rlist; intros; simpl in H3. induction i as [| i Hreci]. simpl; assumption. 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); + replace (S (pred (length l2))) with (length l2); [ assumption | apply S_pred with 0%nat; 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. + intros; assert (H4 : ordered_Rlist (app (r1 :: r2) l2)). + apply H; try assumption. apply RList_P4 with r; assumption. - unfold ordered_Rlist; intros; simpl in H4; + unfold ordered_Rlist; intros i H5; simpl in H5. induction i as [| i Hreci]. simpl; apply (H1 0%nat); 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. + (pos_Rl (app (r1 :: r2) l2) i <= + pos_Rl (app (r1 :: r2) l2) (S i)); + apply (H4 i); simpl; apply lt_S_n; assumption. Qed. Lemma RList_P26 : - forall (l1 l2:Rlist) (i:nat), - (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i. + forall (l1 l2:list R) (i:nat), + (i < length l1)%nat -> pos_Rl (app l1 l2) i = pos_Rl l1 i. Proof. simple induction l1. intros; elim (lt_n_O _ H). @@ -735,49 +711,41 @@ Proof. apply (H l2 i); simpl in H0; apply lt_S_n; assumption. Qed. -Lemma RList_P27 : - forall l1 l2 l3:Rlist, - cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3. -Proof. - simple induction l1; intros; - [ reflexivity | simpl; rewrite (H l2 l3); reflexivity ]. -Qed. - -Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l. -Proof. - simple induction l; - [ reflexivity | intros; simpl; rewrite H; reflexivity ]. -Qed. - Lemma RList_P29 : - forall (l2 l1:Rlist) (i:nat), - (Rlength l1 <= i)%nat -> - (i < Rlength (cons_Rlist l1 l2))%nat -> - pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1). + forall (l2 l1:list R) (i:nat), + (length l1 <= i)%nat -> + (i < length (app l1 l2))%nat -> + pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1). Proof. - simple induction l2. - intros; rewrite RList_P28 in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)). + induction l2 as [ | r r0 H]. + intros; rewrite app_nil_r in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)). intros; - replace (cons_Rlist l1 (cons r r0)) with - (cons_Rlist (cons_Rlist l1 (cons r nil)) r0). + replace (app l1 (r :: r0)) with + (app (app l1 (r :: nil)) r0). inversion H0. rewrite <- minus_n_n; simpl; rewrite RList_P26. - clear l2 r0 H i H0 H1 H2; induction l1 as [| r0 l1 Hrecl1]. + clear r0 H i H0 H1 H2; induction l1 as [| r0 l1 Hrecl1]. reflexivity. simpl; assumption. - rewrite RList_P23; rewrite plus_comm; simpl; apply lt_n_Sn. - replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))). + rewrite app_length; rewrite plus_comm; simpl; apply lt_n_Sn. + replace (S m - length l1)%nat with (S (S m - S (length 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_comm; simpl; rewrite <- H3; + replace (S (length l1)) with (length (app l1 (r :: nil))). + apply (H (app l1 (r :: nil)) i). + rewrite app_length; rewrite plus_comm; simpl; rewrite <- H3; apply le_n_S; assumption. - repeat rewrite RList_P23; simpl; rewrite RList_P23 in H1; - rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1)); + repeat rewrite app_length; simpl; rewrite app_length in H1; + rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (length l1)); simpl; rewrite plus_comm; apply H1. - rewrite RList_P23; rewrite plus_comm; reflexivity. - change (S (m - Rlength l1) = (S m - Rlength l1)%nat); + rewrite app_length; rewrite plus_comm; reflexivity. + change (S (m - length l1) = (S m - length l1)%nat); apply minus_Sn_m; assumption. - replace (cons r r0) with (cons_Rlist (cons r nil) r0); - [ symmetry ; apply RList_P27 | reflexivity ]. + replace (r :: r0) with (app (r :: nil) r0); + [ symmetry ; apply app_assoc | reflexivity ]. Qed. + +#[deprecated(since="8.12",note="use List.cons instead")] +Notation cons := List.cons. + +#[deprecated(since="8.12",note="use List.nil instead")] +Notation nil := List.nil. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 0337b12cad..23094c6b93 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -464,7 +464,7 @@ Proof. elim (Rlt_irrefl _ H7) ] ]. Qed. -Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist := +Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : list R := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) @@ -473,7 +473,7 @@ Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist := Definition max_N (a b:R) (del:posreal) (h:a < b) : nat := let (N,_) := maxN del h in N. -Definition SubEqui (a b:R) (del:posreal) (h:a < b) : Rlist := +Definition SubEqui (a b:R) (del:posreal) (h:a < b) : list R := SubEquiN (S (max_N del h)) a b del. Lemma Heine_cor1 : @@ -566,25 +566,25 @@ Qed. Lemma SubEqui_P2 : forall (a b:R) (del:posreal) (h:a < b), - pos_Rl (SubEqui del h) (pred (Rlength (SubEqui del h))) = b. + pos_Rl (SubEqui del h) (pred (length (SubEqui del h))) = b. Proof. intros; unfold SubEqui; destruct (maxN del h)as (x,_). cut (forall (x:nat) (a:R) (del:posreal), pos_Rl (SubEquiN (S x) a b del) - (pred (Rlength (SubEquiN (S x) a b del))) = b); + (pred (length (SubEquiN (S x) a b del))) = b); [ intro; apply H | simple 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) + (pred (length (SubEquiN (S n) (a0 + del0) b del0))) = b) ; apply H ] ]. Qed. Lemma SubEqui_P3 : - forall (N:nat) (a b:R) (del:posreal), Rlength (SubEquiN N a b del) = S N. + forall (N:nat) (a b:R) (del:posreal), length (SubEquiN N a b del) = S N. Proof. simple induction N; intros; [ reflexivity | simpl; rewrite H; reflexivity ]. @@ -605,7 +605,7 @@ Qed. Lemma SubEqui_P5 : forall (a b:R) (del:posreal) (h:a < b), - Rlength (SubEqui del h) = S (S (max_N del h)). + length (SubEqui del h) = S (S (max_N del h)). Proof. intros; unfold SubEqui; apply SubEqui_P3. Qed. @@ -623,7 +623,7 @@ Proof. intros; unfold ordered_Rlist; intros; rewrite SubEqui_P5 in H; simpl in H; inversion H. rewrite (SubEqui_P6 del h (i:=(max_N del h))). - replace (S (max_N del h)) with (pred (Rlength (SubEqui del h))). + replace (S (max_N del h)) with (pred (length (SubEqui del h))). rewrite SubEqui_P2; unfold max_N; case (maxN del h) as (?&?&?); left; assumption. rewrite SubEqui_P5; reflexivity. @@ -639,7 +639,7 @@ Qed. Lemma SubEqui_P8 : forall (a b:R) (del:posreal) (h:a < b) (i:nat), - (i < Rlength (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b. + (i < length (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b. Proof. intros; split. pattern a at 1; rewrite <- (SubEqui_P1 del h); apply RList_P5. @@ -657,7 +657,7 @@ Lemma SubEqui_P9 : { g:StepFun a b | g b = f b /\ (forall i:nat, - (i < pred (Rlength (SubEqui del h)))%nat -> + (i < pred (length (SubEqui del h)))%nat -> constant_D_eq g (co_interval (pos_Rl (SubEqui del h) i) (pos_Rl (SubEqui del h) (S i))) @@ -713,7 +713,7 @@ Proof. a <= t <= b -> t = b \/ (exists i : nat, - (i < pred (Rlength (SubEqui del H)))%nat /\ + (i < pred (length (SubEqui del H)))%nat /\ co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i)) t)). intro; elim (H8 _ H7); intro. @@ -722,7 +722,7 @@ Proof. 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 (Rlength (SubEqui del H))). + apply SubEqui_P8; apply lt_trans with (pred (length (SubEqui del H))). assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H9; elim (lt_n_O _ H9). @@ -734,7 +734,7 @@ Proof. (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 (Rlength (SubEqui del H))). + assert (H13 : S (max_N del H) = pred (length (SubEqui del H))). rewrite SubEqui_P5; reflexivity. rewrite H13 in H12; rewrite SubEqui_P2 in H12; apply H12. rewrite SubEqui_P6. @@ -785,7 +785,7 @@ Proof. apply H5. assumption. inversion H7. - replace (S (max_N del H)) with (pred (Rlength (SubEqui del H))). + replace (S (max_N del H)) with (pred (length (SubEqui del H))). rewrite (SubEqui_P2 del H); elim H8; intros. elim H11; intro. assumption. @@ -1753,7 +1753,7 @@ Proof. rewrite <- H5; elim (RList_P6 l); intros; apply H10. assumption. apply le_O_n. - apply lt_trans with (pred (Rlength l)); [ assumption | apply lt_pred_n_n ]. + apply lt_trans with (pred (length l)); [ assumption | apply lt_pred_n_n ]. apply neq_O_lt; intro; rewrite <- H12 in H6; discriminate. unfold Rmin; decide (Rle_dec a b) with H; reflexivity. assert (H11 : pos_Rl l (S i) <= b). @@ -1960,7 +1960,7 @@ Proof. 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 (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. unfold Rmin; decide (Rle_dec b c) with Hyp2; @@ -1991,7 +1991,7 @@ Proof. 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 (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H6; discriminate. unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. @@ -2018,7 +2018,7 @@ Proof. 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 (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H6; discriminate. unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. @@ -2037,7 +2037,7 @@ Proof. 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 (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index c8ec4782d9..65221c67d2 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -12,6 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis_reg. Require Import Classical_Prop. +Require Import List. Require Import RList. Local Open Scope R_scope. @@ -114,41 +115,41 @@ Qed. Definition open_interval (a b x:R) : Prop := a < x < b. Definition co_interval (a b x:R) : Prop := a <= x < b. -Definition adapted_couple (f:R -> R) (a b:R) (l lf:Rlist) : Prop := +Definition adapted_couple (f:R -> R) (a b:R) (l lf:list R) : Prop := ordered_Rlist l /\ pos_Rl l 0 = Rmin a b /\ - pos_Rl l (pred (Rlength l)) = Rmax a b /\ - Rlength l = S (Rlength lf) /\ + pos_Rl l (pred (length l)) = Rmax a b /\ + length l = S (length lf) /\ (forall i:nat, - (i < pred (Rlength l))%nat -> + (i < pred (length l))%nat -> 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) := +Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:list R) := adapted_couple f a b l lf /\ (forall i:nat, - (i < pred (Rlength lf))%nat -> + (i < pred (length lf))%nat -> pos_Rl lf i <> pos_Rl lf (S i) \/ f (pos_Rl l (S i)) <> pos_Rl lf i) /\ - (forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)). + (forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <> pos_Rl l (S i)). -Definition is_subdivision (f:R -> R) (a b:R) (l:Rlist) : Type := - { l0:Rlist & adapted_couple f a b l l0 }. +Definition is_subdivision (f:R -> R) (a b:R) (l:list R) : Type := + { l0:list R & adapted_couple f a b l l0 }. Definition IsStepFun (f:R -> R) (a b:R) : Type := - { l:Rlist & is_subdivision f a b l }. + { l:list R & is_subdivision f a b l }. (** ** Class of step functions *) Record StepFun (a b:R) : Type := mkStepFun {fe :> R -> R; pre : IsStepFun fe a b}. -Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). +Definition subdivision (a b:R) (f:StepFun a b) : list R := projT1 (pre f). -Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := +Definition subdivision_val (a b:R) (f:StepFun a b) : list R := match projT2 (pre f) with | existT _ a b => a end. -Fixpoint Int_SF (l k:Rlist) : R := +Fixpoint Int_SF (l k:list R) : R := match l with | nil => 0 | cons a l' => @@ -179,7 +180,7 @@ Proof. Qed. Lemma StepFun_P2 : - forall (a b:R) (f:R -> R) (l lf:Rlist), + forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> adapted_couple f b a l lf. Proof. unfold adapted_couple; intros; decompose [and] H; clear H; @@ -219,7 +220,7 @@ Proof. Qed. Lemma StepFun_P5 : - forall (a b:R) (f:R -> R) (l:Rlist), + forall (a b:R) (f:R -> R) (l:list R), is_subdivision f a b l -> is_subdivision f b a l. Proof. destruct 1 as (x,(H0,(H1,(H2,(H3,H4))))); exists x; @@ -236,7 +237,7 @@ Proof. Qed. Lemma StepFun_P7 : - forall (a b r1 r2 r3:R) (f:R -> R) (l lf:Rlist), + forall (a b r1 r2 r3:R) (f:R -> R) (l lf:list R), a <= b -> adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) -> adapted_couple f r2 b (cons r2 l) lf. @@ -257,31 +258,36 @@ Proof. rewrite H4; reflexivity. intros; unfold constant_D_eq, open_interval; intros; unfold constant_D_eq, open_interval in H6; - assert (H9 : (S i < pred (Rlength (cons r1 (cons r2 l))))%nat). + assert (H9 : (S i < pred (length (cons r1 (cons r2 l))))%nat). simpl; simpl in H0; apply lt_n_S; assumption. assert (H10 := H6 _ H9); apply H10; assumption. Qed. Lemma StepFun_P8 : - forall (f:R -> R) (l1 lf1:Rlist) (a b:R), + forall (f:R -> R) (l1 lf1:list R) (a b:R), adapted_couple f a b l1 lf1 -> a = b -> Int_SF lf1 l1 = 0. Proof. simple induction l1. intros; induction lf1 as [| r lf1 Hreclf1]; reflexivity. - simple induction r0. + intros r r0. + induction r0 as [ | r1 r2 H0]. intros; induction lf1 as [| r1 lf1 Hreclf1]. reflexivity. unfold adapted_couple in H0; decompose [and] H0; clear H0; simpl in H5; discriminate. - intros; induction lf1 as [| r3 lf1 Hreclf1]. + intros H. + induction lf1 as [| r3 lf1 Hreclf1]; intros a b H1 H2. reflexivity. simpl; cut (r = r1). - intro; rewrite H3; rewrite (H0 lf1 r b). + intros H3. + rewrite H3; rewrite (H lf1 r b). ring. rewrite H3; apply StepFun_P7 with a r r3; [ right; assumption | assumption ]. - clear H H0 Hreclf1 r0; unfold adapted_couple in H1; decompose [and] H1; + clear H H0 Hreclf1; unfold adapted_couple in H1. + decompose [and] H1. intros; simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; [ assumption | reflexivity ]. + unfold adapted_couple in H1; decompose [and] H1; intros; apply Rle_antisym. apply (H3 0%nat); simpl; apply lt_O_Sn. simpl in H5; rewrite H2 in H5; rewrite H5; replace (Rmin b b) with (Rmax a b); @@ -292,8 +298,8 @@ Proof. Qed. Lemma StepFun_P9 : - forall (a b:R) (f:R -> R) (l lf:Rlist), - adapted_couple f a b l lf -> a <> b -> (2 <= Rlength l)%nat. + forall (a b:R) (f:R -> R) (l lf:list R), + adapted_couple f a b l lf -> a <> b -> (2 <= length l)%nat. Proof. intros; unfold adapted_couple in H; decompose [and] H; clear H; induction l as [| r l Hrecl]; @@ -307,13 +313,13 @@ Proof. Qed. Lemma StepFun_P10 : - forall (f:R -> R) (l lf:Rlist) (a b:R), + forall (f:R -> R) (l lf:list R) (a b:R), a <= b -> adapted_couple f a b l lf -> - exists l' : Rlist, - (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). + exists l' : list R, + (exists lf' : list R, adapted_couple_opt f a b l' lf'). Proof. - simple induction l. + 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. @@ -503,7 +509,7 @@ Proof. Qed. Lemma StepFun_P11 : - forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist) + forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R) (f:R -> R), a < b -> adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> @@ -627,7 +633,7 @@ Proof. Qed. Lemma StepFun_P12 : - forall (a b:R) (f:R -> R) (l lf:Rlist), + forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple_opt f a b l lf -> adapted_couple_opt f b a l lf. Proof. unfold adapted_couple_opt; unfold adapted_couple; intros; @@ -643,7 +649,7 @@ Proof. Qed. Lemma StepFun_P13 : - forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist) + forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R) (f:R -> R), a <> b -> adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> @@ -657,15 +663,15 @@ Proof. Qed. Lemma StepFun_P14 : - forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R), + 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. - simple induction l1. + 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. - simple induction r0. + 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. @@ -798,7 +804,7 @@ Proof. rewrite H9; change (forall i:nat, - (i < pred (Rlength (cons r4 lf2)))%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. @@ -840,7 +846,7 @@ Proof. rewrite <- H10; unfold open_interval; apply H2. elim H3; clear H3; intros; split. rewrite H5 in H3; intros; apply (H3 (S i)). - simpl; replace (Rlength lf2) with (S (pred (Rlength lf2))). + simpl; replace (length lf2) with (S (pred (length lf2))). apply lt_n_S; apply H12. symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H13 in H12; elim (lt_n_O _ H12). @@ -863,7 +869,7 @@ Proof. Qed. Lemma StepFun_P15 : - forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R), + forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. @@ -876,10 +882,10 @@ Proof. Qed. Lemma StepFun_P16 : - forall (f:R -> R) (l lf:Rlist) (a b:R), + forall (f:R -> R) (l lf:list R) (a b:R), adapted_couple f a b l lf -> - exists l' : Rlist, - (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). + exists l' : list R, + (exists lf' : list R, adapted_couple_opt f a b l' lf'). Proof. intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply (StepFun_P10 Hle H) @@ -891,7 +897,7 @@ Proof. Qed. Lemma StepFun_P17 : - forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R), + forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), adapted_couple f a b l1 lf1 -> adapted_couple f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. @@ -922,7 +928,7 @@ Proof. Qed. Lemma StepFun_P19 : - forall (l1:Rlist) (f g:R -> R) (l:R), + forall (l1:list R) (f g:R -> R) (l:R), Int_SF (FF l1 (fun x:R => f x + l * g x)) l1 = Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1. Proof. @@ -933,8 +939,8 @@ Proof. Qed. Lemma StepFun_P20 : - forall (l:Rlist) (f:R -> R), - (0 < Rlength l)%nat -> Rlength l = S (Rlength (FF l f)). + forall (l:list R) (f:R -> R), + (0 < length l)%nat -> length l = S (length (FF l f)). Proof. intros l f H; induction l; [ elim (lt_irrefl _ H) @@ -942,7 +948,7 @@ Proof. Qed. Lemma StepFun_P21 : - forall (a b:R) (f:R -> R) (l:Rlist), + forall (a b:R) (f:R -> R) (l:list R), is_subdivision f a b l -> adapted_couple f a b l (FF l f). Proof. intros * (x & H & H1 & H0 & H2 & H4). @@ -979,7 +985,7 @@ Proof. Qed. Lemma StepFun_P22 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + 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). @@ -1032,25 +1038,25 @@ Proof. (H8 : In (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (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 (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; - exists (pred (Rlength (cons_ORlist (cons r lf) lg))); + exists (pred (length (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))))); + (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 (Rlength (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; @@ -1060,10 +1066,10 @@ Proof. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (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 : Rlength lg = S (pred (Rlength lg))). + rewrite H15; assert (H17 : length lg = S (pred (length lg))). apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18; @@ -1075,7 +1081,7 @@ Proof. 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 (Rlength (cons r lf))); split; + exists (pred (length (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; @@ -1089,7 +1095,7 @@ Proof. intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : - exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). + exists r : R, (exists r0 : list R, cons_ORlist lf lg = cons r r0)). apply RList_P19; red; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF; rewrite RList_P12. @@ -1128,7 +1134,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply le_O_n. - apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); + apply lt_trans with (pred (length (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) ]. @@ -1147,9 +1153,9 @@ Proof. set (I := fun j:nat => - pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat); + pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < length lf)%nat); assert (H12 : Nbound I). - unfold Nbound; exists (Rlength lf); intros; unfold I in H12; elim H12; + unfold Nbound; exists (length lf); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). exists 0%nat; unfold I; split. @@ -1159,7 +1165,7 @@ Proof. 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))). + apply lt_trans with (pred (length (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). @@ -1167,12 +1173,12 @@ Proof. rewrite <- H6 in H11; rewrite <- H5 in H11; elim (Rlt_irrefl _ 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 : (x0 < pred (Rlength lf))%nat). + 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 lt_S_n; replace (S (pred (Rlength lf))) with (Rlength lf). + apply lt_S_n; replace (S (pred (length lf))) with (length lf). inversion H18. 2: apply lt_n_S; assumption. - cut (x0 = pred (Rlength lf)). + cut (x0 = pred (length lf)). intro; 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)). @@ -1180,7 +1186,7 @@ Proof. elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H5; apply Rle_trans with - (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). + (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 lt_n_Sm_le; apply lt_n_S; assumption. @@ -1197,8 +1203,8 @@ Proof. 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 : (S x0 < Rlength lf)%nat). - replace (Rlength lf) with (S (pred (Rlength lf))); + assert (H22 : (S x0 < length lf)%nat). + replace (length lf) with (S (pred (length lf))); [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ]. @@ -1216,7 +1222,7 @@ Proof. Qed. Lemma StepFun_P23 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + forall (a b:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg). Proof. @@ -1229,7 +1235,7 @@ Proof. Qed. Lemma StepFun_P24 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + 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 g a b (cons_ORlist lf lg). @@ -1282,24 +1288,24 @@ Proof. (H8 : In (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (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 (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; - exists (pred (Rlength (cons_ORlist (cons r lf) lg))); + exists (pred (length (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))))); + (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 (Rlength (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; @@ -1309,10 +1315,10 @@ Proof. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (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 : Rlength lg = S (pred (Rlength lg))). + assert (H17 : length lg = S (pred (length lg))). apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18; @@ -1324,7 +1330,7 @@ Proof. 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 (Rlength (cons r lf))); split; + exists (pred (length (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; @@ -1338,7 +1344,7 @@ Proof. intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : - exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). + exists r : R, (exists r0 : list R, cons_ORlist lf lg = cons r r0)). apply RList_P19; red; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF; rewrite RList_P12. @@ -1377,7 +1383,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply le_O_n. - apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); + apply lt_trans with (pred (length (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) ]. @@ -1394,9 +1400,9 @@ Proof. set (I := fun j:nat => - pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat); + pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < length lg)%nat); assert (H12 : Nbound I). - unfold Nbound; exists (Rlength lg); intros; unfold I in H12; elim H12; + unfold Nbound; exists (length lg); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). exists 0%nat; unfold I; split. @@ -1406,7 +1412,7 @@ Proof. 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))); + | apply lt_trans with (pred (length (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) ] ]. @@ -1414,12 +1420,12 @@ Proof. rewrite <- H1 in H11; rewrite <- H0 in H11; elim (Rlt_irrefl _ 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 : (x0 < pred (Rlength lg))%nat). + intros; assert (H16 := H4 x0); assert (H17 : (x0 < pred (length lg))%nat). 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). + apply lt_S_n; replace (S (pred (length lg))) with (length lg). inversion H18. 2: apply lt_n_S; assumption. - cut (x0 = pred (Rlength lg)). + cut (x0 = pred (length lg)). intro; rewrite H19 in H14; rewrite H0 in H14; cut (pos_Rl (cons_ORlist lf lg) i < b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)). @@ -1427,7 +1433,7 @@ Proof. elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H0; apply Rle_trans with - (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). + (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 lt_n_Sm_le; apply lt_n_S; assumption. @@ -1445,8 +1451,8 @@ Proof. 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 : (S x0 < Rlength lg)%nat). - replace (Rlength lg) with (S (pred (Rlength lg))). + assert (H22 : (S x0 < length lg)%nat). + replace (length lg) with (S (pred (length lg))). apply lt_n_S; assumption. symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21). @@ -1463,7 +1469,7 @@ Proof. Qed. Lemma StepFun_P25 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + forall (a b:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg). Proof. @@ -1476,7 +1482,7 @@ Proof. Qed. Lemma StepFun_P26 : - forall (a b l:R) (f g:R -> R) (l1:Rlist), + forall (a b l:R) (f g:R -> R) (l1:list R), is_subdivision f a b l1 -> is_subdivision g a b l1 -> is_subdivision (fun x:R => f x + l * g x) a b l1. @@ -1494,7 +1500,7 @@ Proof. change (pos_Rl x0 i + l * pos_Rl x i = pos_Rl - (app_Rlist (mid_Rlist (cons r r0) r) (fun x2:R => f x2 + l * g x2)) + (map (fun x2:R => f x2 + l * g x2) (mid_Rlist (cons r r0) r)) (S i)); rewrite RList_P12. rewrite RList_P13. rewrite <- H12; rewrite (H9 _ H8); try rewrite (H4 _ H8); @@ -1521,7 +1527,7 @@ Proof. Qed. Lemma StepFun_P27 : - forall (a b l:R) (f g:R -> R) (lf lg:Rlist), + forall (a b l:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision (fun x:R => f x + l * g x) a b (cons_ORlist lf lg). @@ -1586,9 +1592,9 @@ Proof. Qed. Lemma StepFun_P31 : - forall (a b:R) (f:R -> R) (l lf:Rlist), + forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> - adapted_couple (fun x:R => Rabs (f x)) a b l (app_Rlist lf Rabs). + adapted_couple (fun x:R => Rabs (f x)) a b l (map Rabs lf). Proof. unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. @@ -1604,15 +1610,15 @@ Lemma StepFun_P32 : Proof. intros a b f; unfold IsStepFun; apply existT with (subdivision f); unfold is_subdivision; - apply existT with (app_Rlist (subdivision_val f) Rabs); + apply existT with (map Rabs (subdivision_val f)); apply StepFun_P31; apply StepFun_P1. Qed. Lemma StepFun_P33 : - forall l2 l1:Rlist, - ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (app_Rlist l2 Rabs) l1. + forall l2 l1:list R, + ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (map Rabs l2) l1. Proof. - simple induction l2; intros. + induction l2 as [ | r r0 H]; intros. simpl; rewrite Rabs_R0; right; reflexivity. simpl; induction l1 as [| r1 l1 Hrecl1]. rewrite Rabs_R0; right; reflexivity. @@ -1635,7 +1641,7 @@ Proof. replace (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f))) (subdivision (mkStepFun (StepFun_P32 f)))) with - (Int_SF (app_Rlist (subdivision_val f) Rabs) (subdivision f)). + (Int_SF (map Rabs (subdivision_val f)) (subdivision f)). apply StepFun_P33; assert (H0 := StepFun_P29 f); unfold is_subdivision in H0; elim H0; intros; unfold adapted_couple in p; decompose [and] p; assumption. @@ -1645,14 +1651,14 @@ Proof. Qed. Lemma StepFun_P35 : - forall (l:Rlist) (a b:R) (f g:R -> R), + forall (l:list R) (a b:R) (f g:R -> R), ordered_Rlist l -> pos_Rl l 0 = a -> - pos_Rl l (pred (Rlength l)) = b -> + pos_Rl l (pred (length l)) = b -> (forall x:R, a < x < b -> f x <= g x) -> Int_SF (FF l f) l <= Int_SF (FF l g) l. Proof. - simple induction l; intros. + induction l as [ | r r0 H]; intros. right; reflexivity. simpl; induction r0 as [| r0 r1 Hrecr0]. right; reflexivity. @@ -1682,7 +1688,7 @@ Proof. rewrite <- Rinv_r_sym. rewrite Rmult_1_l; rewrite double; assert (H5 : r0 <= b). replace b with - (pos_Rl (cons r (cons r0 r1)) (pred (Rlength (cons r (cons r0 r1))))). + (pos_Rl (cons r (cons r0 r1)) (pred (length (cons r (cons r0 r1))))). replace r0 with (pos_Rl (cons r (cons r0 r1)) 1). elim (RList_P6 (cons r (cons r0 r1))); intros; apply H5. assumption. @@ -1712,7 +1718,7 @@ Proof. Qed. Lemma StepFun_P36 : - forall (a b:R) (f g:StepFun a b) (l:Rlist), + forall (a b:R) (f g:StepFun a b) (l:list R), a <= b -> is_subdivision f a b l -> is_subdivision g a b l -> @@ -1748,18 +1754,18 @@ Proof. Qed. Lemma StepFun_P38 : - forall (l:Rlist) (a b:R) (f:R -> R), + forall (l:list R) (a b:R) (f:R -> R), ordered_Rlist l -> pos_Rl l 0 = a -> - pos_Rl l (pred (Rlength l)) = b -> + pos_Rl l (pred (length l)) = b -> { g:StepFun a b | g b = f b /\ (forall i:nat, - (i < pred (Rlength l))%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. - intros l a b f; generalize a; clear a; induction l. + 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. @@ -1772,7 +1778,7 @@ Proof. apply RList_P4 with r; assumption. assert (H3 : pos_Rl (cons r1 l) 0 = r1). reflexivity. - assert (H4 : pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))) = b). + 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 @@ -1796,7 +1802,7 @@ Proof. simpl in H0; rewrite <- H0; apply (H 0%nat); simpl; apply lt_O_Sn. unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. apply (H10 i); apply lt_S_n. - replace (S (pred (Rlength lg))) with (Rlength lg). + replace (S (pred (length lg))) with (length lg). apply H9. apply S_pred with 0%nat; apply neq_O_lt; intro; rewrite <- H14 in H9; elim (lt_n_O _ H9). @@ -1825,9 +1831,9 @@ Proof. 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 (Rlength lg))%nat). + assert (H17 : (i < pred (length lg))%nat). apply lt_S_n. - replace (S (pred (Rlength lg))) with (Rlength lg). + replace (S (pred (length lg))) with (length lg). assumption. apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H14 in H9; elim (lt_n_O _ H9). @@ -1843,7 +1849,7 @@ Proof. assumption. elim (RList_P3 lg (pos_Rl lg i)); intros; apply H21; exists i; split. reflexivity. - apply lt_trans with (pred (Rlength lg)); try assumption. + apply lt_trans with (pred (length 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; decide (Rle_dec r1 b) with H7; reflexivity. @@ -1860,7 +1866,7 @@ Proof. (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 (Rlength (cons r1 l)))%nat). + assert (H11 : (i < pred (length (cons r1 l)))%nat). 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; @@ -1873,7 +1879,7 @@ Proof. elim (RList_P6 (cons r1 l)); intros; apply H15; [ assumption | apply le_O_n - | simpl; apply lt_trans with (Rlength l); + | simpl; apply lt_trans with (length l); [ apply lt_S_n; assumption | apply lt_n_Sn ] ]. Qed. @@ -1912,12 +1918,12 @@ Proof. Qed. Lemma StepFun_P40 : - forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:Rlist), + forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:list R), a < b -> b < c -> adapted_couple f a b l1 lf1 -> adapted_couple f b c l2 lf2 -> - adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f). + adapted_couple f a c (app l1 l2) (FF (app l1 l2) f). Proof. intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; unfold adapted_couple in H1, H2; unfold adapted_couple; decompose [and] H1; @@ -1941,28 +1947,28 @@ Proof. | left; assumption ]. red; intro; rewrite H1 in H11; discriminate. apply StepFun_P20. - rewrite RList_P23; apply neq_O_lt; red; intro. - assert (H2 : (Rlength l1 + Rlength l2)%nat = 0%nat). + rewrite app_length; apply neq_O_lt; red; intro. + assert (H2 : (length l1 + length l2)%nat = 0%nat). 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)) (Rlength l1)); intro. - assert (H14 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i). + elim (le_or_lt (S (S i)) (length l1)); intro. + assert (H14 : pos_Rl (app 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 (Rlength l1); [ assumption | apply le_n_Sn ]. - assert (H15 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l1 (S i)). + apply le_trans with (length l1); [ assumption | apply le_n_Sn ]. + assert (H15 : pos_Rl (app 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 : (2 <= Rlength l1)%nat). + rewrite H14 in H2; rewrite H15 in H2; assert (H16 : (2 <= length l1)%nat). 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) + (f x = pos_Rl (map f (mid_Rlist (app (cons r2 r3) l2) r1)) i) ; rewrite RList_P12. induction i as [| i Hreci]. simpl; assert (H18 := H8 0%nat); unfold constant_D_eq, open_interval in H18; - assert (H19 : (0 < pred (Rlength l1))%nat). + assert (H19 : (0 < pred (length l1))%nat). rewrite H17; simpl; apply lt_O_Sn. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. @@ -1991,14 +1997,14 @@ Proof. 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 (app (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 (app (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 : (S i < pred (Rlength l1))%nat). + assert (H19 : (S i < pred (length l1))%nat). apply lt_pred; apply lt_S_n; apply le_lt_n_Sm; assumption. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. @@ -2025,7 +2031,7 @@ Proof. simpl; rewrite H17 in H1; simpl in H1; apply lt_S_n; assumption. rewrite RList_P14; rewrite H17 in H1; simpl in H1; apply H1. inversion H12. - assert (H16 : pos_Rl (cons_Rlist l1 l2) (S i) = b). + assert (H16 : pos_Rl (app l1 l2) (S i) = b). rewrite RList_P29. rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin; case (Rle_dec b c) as [|[]]; [ reflexivity | left; assumption ]. @@ -2033,30 +2039,30 @@ Proof. induction l1 as [| r l1 Hrecl1]. 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). + assert (H17 : pos_Rl (app l1 l2) i = b). rewrite RList_P26. - replace i with (pred (Rlength l1)); + replace i with (pred (length l1)); [ rewrite H4; unfold Rmax; case (Rle_dec a b) as [|[]]; [ reflexivity | left; assumption ] | rewrite H15; reflexivity ]. rewrite H15; apply lt_n_Sn. rewrite H16 in H2; rewrite H17 in H2; elim H2; intros; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H14 H18)). - assert (H16 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1)). + assert (H16 : pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1)). apply RList_P29. apply le_S_n; assumption. - apply lt_le_trans with (pred (Rlength (cons_Rlist l1 l2))); + apply lt_le_trans with (pred (length (app l1 l2))); [ assumption | apply le_pred_n ]. assert - (H17 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S (i - Rlength l1))). - replace (S (i - Rlength l1)) with (S i - Rlength l1)%nat. + (H17 : pos_Rl (app l1 l2) (S i) = pos_Rl l2 (S (i - length l1))). + replace (S (i - length l1)) with (S i - length l1)%nat. apply RList_P29. apply le_S_n; apply le_trans with (S i); [ assumption | apply le_n_Sn ]. induction l1 as [| r l1 Hrecl1]. 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 : (2 <= Rlength l1)%nat). + assert (H18 : (2 <= length l1)%nat). 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 as [| r l1 Hrecl1]. discriminate. @@ -2068,7 +2074,7 @@ Proof. clear Hrecl1; simpl; repeat apply le_n_S; apply le_O_n. elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19; change - (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i) + (f x = pos_Rl (map f (mid_Rlist (app (cons r2 r3) l2) r1)) i) ; rewrite RList_P12. induction i as [| i Hreci]. assert (H20 := le_S_n _ _ H15); assert (H21 := le_trans _ _ _ H18 H20); @@ -2076,31 +2082,31 @@ Proof. 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 (S i - Rlength (cons r1 (cons r2 r3)))) + (pos_Rl (app (cons r2 r3) l2) i = + pos_Rl l2 (S i - length (cons r1 (cons r2 r3)))) in H16; rewrite H16; change - (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) = - pos_Rl l2 (S (S i - Rlength (cons r1 (cons r2 r3))))) - in H17; rewrite H17; assert (H20 := H13 (S i - Rlength l1)%nat); + (pos_Rl (app (cons r2 r3) l2) (S i) = + pos_Rl l2 (S (S i - length (cons r1 (cons r2 r3))))) + in H17; rewrite H17; assert (H20 := H13 (S i - length l1)%nat); unfold constant_D_eq, open_interval in H20; - assert (H21 : (S i - Rlength l1 < pred (Rlength l2))%nat). + assert (H21 : (S i - length l1 < pred (length l2))%nat). apply lt_pred; rewrite minus_Sn_m. - apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. + apply plus_lt_reg_l with (length 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. + rewrite app_length 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 (S i - Rlength l1) <= pos_Rl l2 (S (S i - Rlength l1))). + (H23 : pos_Rl l2 (S i - length l1) <= pos_Rl l2 (S (S i - length l1))). apply H7; apply lt_pred. rewrite minus_Sn_m. - apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. + apply plus_lt_reg_l with (length 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. + rewrite app_length 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. @@ -2115,7 +2121,7 @@ Proof. [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; - [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - Rlength l1))); + [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - length l1))); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite <- H19 in H16; rewrite <- H19 in H17; elim H2; intros; @@ -2123,11 +2129,11 @@ Proof. 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_irrefl _ (Rlt_trans _ _ _ H25 H26)). - assert (H23 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S i - Rlength l1)). + assert (H23 : pos_Rl (app l1 l2) (S i) = pos_Rl l2 (S i - length l1)). rewrite H19; simpl; simpl in H16; apply H16. assert (H24 : - pos_Rl (cons_Rlist l1 l2) (S (S i)) = pos_Rl l2 (S (S i - Rlength l1))). + pos_Rl (app l1 l2) (S (S i)) = pos_Rl l2 (S (S i - length 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. @@ -2141,7 +2147,7 @@ Proof. intros f a b c H H0 (l1,(lf1,H1)) (l2,(lf2,H2)); destruct (total_order_T a b) as [[Hltab|Hab]|Hgtab]. destruct (total_order_T b c) as [[Hltbc|Hbc]|Hgtbc]. - exists (cons_Rlist l1 l2); exists (FF (cons_Rlist l1 l2) f); + exists (app l1 l2); exists (FF (app l1 l2) f); apply StepFun_P40 with b lf1 lf2; assumption. exists l1; exists lf1; rewrite Hbc in H1; assumption. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgtbc)). @@ -2150,9 +2156,9 @@ Proof. Qed. Lemma StepFun_P42 : - forall (l1 l2:Rlist) (f:R -> R), - pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 0 -> - Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2) = + forall (l1 l2:list R) (f:R -> R), + pos_Rl l1 (pred (length l1)) = pos_Rl l2 0 -> + Int_SF (FF (app l1 l2) f) (app l1 l2) = Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2. Proof. intros l1 l2 f; induction l1 as [| r l1 IHl1]; intros H; @@ -2193,7 +2199,7 @@ Proof. elim Hle; intro. elim Hle'; intro. replace (Int_SF lf3 l3) with - (Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)). + (Int_SF (FF (app l1 l2) f) (app l1 l2)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). symmetry ; apply StepFun_P42. @@ -2225,7 +2231,7 @@ Proof. elim Hle''; intro. rewrite Rplus_comm; replace (Int_SF lf1 l1) with - (Int_SF (FF (cons_Rlist l3 l2) f) (cons_Rlist l3 l2)). + (Int_SF (FF (app l3 l2) f) (app l3 l2)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). apply StepFun_P42. @@ -2249,7 +2255,7 @@ Proof. ring. elim Hle; intro. replace (Int_SF lf2 l2) with - (Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist l3 l1)). + (Int_SF (FF (app l3 l1) f) (app l3 l1)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). symmetry ; apply StepFun_P42. @@ -2277,7 +2283,7 @@ Proof. ring. rewrite Rplus_comm; elim Hle''; intro. replace (Int_SF lf2 l2) with - (Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist l1 l3)). + (Int_SF (FF (app l1 l3) f) (app l1 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). symmetry ; apply StepFun_P42. @@ -2304,7 +2310,7 @@ Proof. ring. elim Hle'; intro. replace (Int_SF lf1 l1) with - (Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist l2 l3)). + (Int_SF (FF (app l2 l3) f) (app l2 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). symmetry ; apply StepFun_P42. @@ -2334,7 +2340,7 @@ Proof. replace (Int_SF lf3 l3) with (Int_SF lf2 l2 + Int_SF lf1 l1). ring. replace (Int_SF lf3 l3) with - (Int_SF (FF (cons_Rlist l2 l1) f) (cons_Rlist l2 l1)). + (Int_SF (FF (app l2 l1) f) (app l2 l1)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). symmetry ; apply StepFun_P42. @@ -2395,17 +2401,17 @@ Proof. elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X; elim X; clear X; intros l1 [lf1 H2]; cut - (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R), + (forall (l1 lf1:list R) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> - { l:Rlist & { l0:Rlist & adapted_couple f a c l l0 } }). + { l:list R & { l0:list R & adapted_couple f a c l l0 } }). intro X; unfold IsStepFun; unfold is_subdivision; eapply X. apply H2. split; assumption. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; discriminate. - simple induction r0. + intros r r0; elim r0. intros X lf1 a b c f H H0; assert (H1 : a = b). unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3; simpl in H2; assert (H7 : a <= b). @@ -2438,7 +2444,7 @@ Proof. unfold constant_D_eq, open_interval; intros; simpl in H8; inversion H8. simpl; assert (H10 := H7 0%nat); - assert (H12 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). + assert (H12 : (0 < pred (length (cons r (cons r1 r2))))%nat). simpl; apply lt_O_Sn. apply (H10 H12); unfold open_interval; simpl; rewrite H11 in H9; simpl in H9; elim H9; clear H9; @@ -2479,7 +2485,7 @@ Proof. intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. simpl; assert (H17 := H10 0%nat); - assert (H18 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). + assert (H18 : (0 < pred (length (cons r (cons r1 r2))))%nat). simpl; apply lt_O_Sn. apply (H17 H18); unfold open_interval; simpl; simpl in H4; elim H4; clear H4; intros; split; try assumption; @@ -2507,16 +2513,16 @@ Proof. elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X; elim X; clear X; intros l1 [lf1 H2]; cut - (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R), + (forall (l1 lf1:list R) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> - { l:Rlist & { l0:Rlist & adapted_couple f c b l l0 } }). + { l:list R & { l0:list R & adapted_couple f c b l l0 } }). intro X; unfold IsStepFun; unfold is_subdivision; eapply X; [ apply H2 | split; assumption ]. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; discriminate. - simple induction r0. + intros r r0; elim r0. intros X lf1 a b c f H H0; assert (H1 : a = b). unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3; simpl in H2; assert (H7 : a <= b). diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index d21042884e..fa5442e86f 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -12,6 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. Require Import RList. +Require Import List. Require Import Classical_Prop. Require Import Classical_Pred_Type. Local Open Scope R_scope. @@ -388,7 +389,7 @@ Record family : Type := mkfamily Definition family_open_set (f:family) : Prop := forall x:R, open_set (f x). Definition domain_finite (D:R -> Prop) : Prop := - exists l : Rlist, (forall x:R, D x <-> In x l). + exists l : list R, (forall x:R, D x <-> In x l). Definition family_finite (f:family) : Prop := domain_finite (ind f). @@ -669,7 +670,7 @@ Proof. intro H14; simpl in H14; unfold intersection_domain in H14; specialize H13 with x0; destruct H13 as (H13,H15); destruct (Req_dec x0 y0) as [H16|H16]. - simpl; left; apply H16. + simpl; left. symmetry; apply H16. simpl; right; apply H13. simpl; unfold intersection_domain; unfold Db in H14; decompose [and or] H14. @@ -678,8 +679,8 @@ Proof. intro H14; simpl in H14; destruct H14 as [H15|H15]; simpl; unfold intersection_domain. split. - apply (cond_fam f0); rewrite H15; exists b; apply H6. - unfold Db; right; assumption. + apply (cond_fam f0); rewrite <- H15; exists b; apply H6. + unfold Db; right; symmetry; assumption. simpl; unfold intersection_domain; elim (H13 x0). intros _ H16; assert (H17 := H16 H15); simpl in H17; unfold intersection_domain in H17; split. @@ -750,15 +751,15 @@ Proof. intro H14; simpl in H14; unfold intersection_domain in H14; specialize (H13 x0); destruct H13 as (H13,H15); destruct (Req_dec x0 y0) as [Heq|Hneq]. - simpl; left; apply Heq. + simpl; left; symmetry; apply Heq. simpl; right; apply H13; simpl; unfold intersection_domain; unfold Db in H14; decompose [and or] H14. split; assumption. elim Hneq; assumption. intros [H15|H15]. split. - apply (cond_fam f0); rewrite H15; exists m; apply H6. - unfold Db; right; assumption. + apply (cond_fam f0); rewrite <- H15; exists m; apply H6. + unfold Db; right; symmetry; assumption. elim (H13 x0); intros _ H16. assert (H17 := H16 H15). simpl in H17. @@ -810,9 +811,10 @@ Proof. unfold family_finite; unfold domain_finite; exists (cons y0 nil); intro; split. simpl; unfold intersection_domain; intros (H3,H4). - unfold D' in H4; left; apply H4. + unfold D' in H4; left; symmetry; apply H4. simpl; unfold intersection_domain; intros [H4|[]]. - split; [ rewrite H4; apply (cond_fam f0); exists a; apply H2 | apply H4 ]. + split; [ rewrite <- H4; apply (cond_fam f0); exists a; apply H2 | + symmetry; apply H4 ]. split; [ right; reflexivity | apply Hle ]. apply compact_eqDom with (fun c:R => False). apply compact_EMP. |