diff options
| author | Pierre-Marie Pédrot | 2020-02-08 13:14:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-08 13:14:20 +0100 |
| commit | 80010afc70eee3df65b6f8a16a202fb9da11fb80 (patch) | |
| tree | f7251eb90109afb1e12f799bb87ea06791ebf302 | |
| parent | 79e9700d0533c3f36c9fbf0011f816981b8a3a3d (diff) | |
| parent | 0fe99a0d6a4d643cf311200c870aeaff042d7069 (diff) | |
Merge PR #11404: replace RList by list R in all files where it is used in this directory
Ack-by: SkySkimmer
Reviewed-by: herbelin
| -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. |