diff options
Diffstat (limited to 'theories/Reals/RList.v')
| -rw-r--r-- | theories/Reals/RList.v | 744 |
1 files changed, 744 insertions, 0 deletions
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v new file mode 100644 index 00000000..3b58c02f --- /dev/null +++ b/theories/Reals/RList.v @@ -0,0 +1,744 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: RList.v,v 1.10.2.1 2004/07/16 19:31:11 herbelin Exp $ i*) + +Require Import Rbase. +Require Import Rfunctions. +Open Local Scope R_scope. + +Inductive Rlist : Type := + | nil : Rlist + | cons : R -> Rlist -> Rlist. + +Fixpoint In (x:R) (l:Rlist) {struct l} : Prop := + match l with + | nil => False + | cons a l' => x = a \/ In x l' + end. + +Fixpoint Rlength (l:Rlist) : nat := + match l with + | nil => 0%nat + | cons a l' => S (Rlength l') + end. + +Fixpoint MaxRlist (l:Rlist) : R := + match l with + | nil => 0 + | cons a l1 => + match l1 with + | nil => a + | cons a' l2 => Rmax a (MaxRlist l1) + end + end. + +Fixpoint MinRlist (l:Rlist) : R := + match l with + | nil => 1 + | cons a l1 => + match l1 with + | nil => a + | cons a' l2 => Rmin a (MinRlist l1) + end + end. + +Lemma MaxRlist_P1 : forall (l:Rlist) (x:R), In x l -> x <= MaxRlist l. +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 in |- *; right; assumption. +elim H0. +replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))). +simpl in H; decompose [or] H. +rewrite H0; apply RmaxLess1. +unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro. +apply Hrecl; simpl in |- *; tauto. +apply Rle_trans with (MaxRlist (cons r0 l)); + [ apply Hrecl; simpl in |- *; tauto | left; auto with real ]. +unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro. +apply Hrecl; simpl in |- *; tauto. +apply Rle_trans with (MaxRlist (cons r0 l)); + [ apply Hrecl; simpl in |- *; tauto | left; auto with real ]. +reflexivity. +Qed. + +Fixpoint AbsList (l:Rlist) (x:R) {struct l} : Rlist := + match l with + | nil => nil + | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x) + end. + +Lemma MinRlist_P1 : forall (l:Rlist) (x:R), In x l -> MinRlist l <= x. +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 in |- *; right; symmetry in |- *; assumption. +elim H0. +replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). +simpl in H; decompose [or] H. +rewrite H0; apply Rmin_l. +unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro. +apply Rle_trans with (MinRlist (cons r0 l)). +assumption. +apply Hrecl; simpl in |- *; tauto. +apply Hrecl; simpl in |- *; tauto. +apply Rle_trans with (MinRlist (cons r0 l)). +apply Rmin_r. +apply Hrecl; simpl in |- *; tauto. +reflexivity. +Qed. + +Lemma AbsList_P1 : + forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x). +intros; induction l as [| r l Hrecl]. +elim H. +simpl in |- *; simpl in H; elim H; intro. +left; rewrite H0; reflexivity. +right; apply Hrecl; assumption. +Qed. + +Lemma MinRlist_P2 : + forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l. +intros; induction l as [| r l Hrecl]. +apply Rlt_0_1. +induction l as [| r0 l Hrecl0]. +simpl in |- *; apply H; simpl in |- *; tauto. +replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). +unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro. +apply H; simpl in |- *; tauto. +apply Hrecl; intros; apply H; simpl in |- *; simpl in H0; tauto. +reflexivity. +Qed. + +Lemma AbsList_P2 : + forall (l:Rlist) (x y:R), + In y (AbsList l x) -> exists z : R, In z l /\ y = Rabs (z - x) / 2. +intros; induction l as [| r l Hrecl]. +elim H. +elim H; intro. +exists r; split. +simpl in |- *; tauto. +assumption. +assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros; + exists x0; simpl in |- *; simpl in H2; tauto. +Qed. + +Lemma MaxRlist_P2 : + forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l. +intros; induction l as [| r l Hrecl]. +simpl in H; elim H; trivial. +induction l as [| r0 l Hrecl0]. +simpl in |- *; left; reflexivity. +change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))) in |- *; + unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); + intro. +right; apply Hrecl; exists r0; left; reflexivity. +left; reflexivity. +Qed. + +Fixpoint pos_Rl (l:Rlist) (i:nat) {struct l} : R := + match l with + | nil => 0 + | cons 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)). +intros; induction l as [| r l Hrecl]; + [ elim (lt_n_O _ H) + | simpl in |- *; case (Rlength 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). +intros; induction l as [| r l Hrecl]. +split; intro; + [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ]. +split; intro. +elim H; intro. +exists 0%nat; split; + [ simpl in |- *; apply lt_O_Sn | simpl in |- *; apply H0 ]. +elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros; + exists (S x0); split; + [ simpl in |- *; apply lt_n_S; assumption | simpl in |- *; assumption ]. +elim H; intros; elim H0; intros; elim (zerop x0); intro. +rewrite a in H2; simpl in H2; left; assumption. +right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0). +symmetry in |- *; apply S_pred with 0%nat; assumption. +exists (pred x0); split; + [ simpl in H1; apply lt_S_n; rewrite H5; assumption + | rewrite <- H5 in H2; simpl in H2; assumption ]. +Qed. + +Lemma Rlist_P1 : + forall (l:Rlist) (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)). +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)). +simpl in |- *; left; reflexivity. +assert (H1 := H _ H0); + assert (H2 : forall x:R, In x l -> exists y : R, P x y). +intros; apply H; simpl in |- *; right; assumption. +assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0); + intros; elim H5; clear H5; intros; split. +simpl in |- *; rewrite H5; reflexivity. +intros; elim (zerop i); intro. +rewrite a; simpl in |- *; assumption. +assert (H8 : i = S (pred i)). +apply S_pred with 0%nat; assumption. +rewrite H8; simpl in |- *; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8; + 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). + +Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist := + match l with + | nil => cons x nil + | cons a l' => + match Rle_dec a x with + | left _ => cons a (insert l' x) + | right _ => cons x l + end + end. + +Fixpoint cons_Rlist (l k:Rlist) {struct l} : Rlist := + match l with + | nil => k + | cons a l' => cons a (cons_Rlist l' k) + end. + +Fixpoint cons_ORlist (k l:Rlist) {struct k} : Rlist := + match k with + | nil => l + | cons a k' => cons_ORlist k' (insert l a) + end. + +Fixpoint app_Rlist (l:Rlist) (f:R -> R) {struct l} : Rlist := + match l with + | nil => nil + | cons a l' => cons (f a) (app_Rlist l' f) + end. + +Fixpoint mid_Rlist (l:Rlist) (x:R) {struct l} : Rlist := + match l with + | nil => nil + | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a) + end. + +Definition Rtail (l:Rlist) : Rlist := + 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 + end. + +Lemma RList_P0 : + forall (l:Rlist) (a:R), + pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0. +intros; induction l as [| r l Hrecl]; + [ left; reflexivity + | simpl in |- *; case (Rle_dec r a); intro; + [ right; reflexivity | left; reflexivity ] ]. +Qed. + +Lemma RList_P1 : + forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a). +intros; induction l as [| r l Hrecl]. +simpl in |- *; unfold ordered_Rlist in |- *; intros; simpl in H0; + elim (lt_n_O _ H0). +simpl in |- *; case (Rle_dec r a); intro. +assert (H1 : ordered_Rlist l). +unfold ordered_Rlist in |- *; unfold ordered_Rlist in H; intros; + assert (H1 : (S i < pred (Rlength (cons r l)))%nat); + [ simpl in |- *; replace (Rlength l) with (S (pred (Rlength l))); + [ apply lt_n_S; assumption + | symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *; + intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ] + | apply (H _ H1) ]. +assert (H2 := Hrecl H1); unfold ordered_Rlist in |- *; intros; + induction i as [| i Hreci]. +simpl in |- *; assert (H3 := RList_P0 l a); elim H3; intro. +rewrite H4; assumption. +induction l as [| r1 l Hrecl0]; + [ simpl in |- *; assumption + | rewrite H4; apply (H 0%nat); simpl in |- *; apply lt_O_Sn ]. +simpl in |- *; apply H2; simpl in H0; apply lt_S_n; + replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a)); + [ assumption + | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + rewrite <- H3 in H0; elim (lt_n_O _ H0) ]. +unfold ordered_Rlist in |- *; intros; induction i as [| i Hreci]; + [ simpl in |- *; auto with real + | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)) in |- *; apply H; + simpl in H0; simpl in |- *; apply (lt_S_n _ _ H0) ]. +Qed. + +Lemma RList_P2 : + forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2). +simple induction l1; + [ intros; simpl in |- *; apply H + | intros; simpl in |- *; apply H; apply RList_P1; assumption ]. +Qed. + +Lemma RList_P3 : + forall (l:Rlist) (x:R), + In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat). +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 in |- *; apply lt_O_Sn ] + | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split; + [ apply H1 | simpl in |- *; apply lt_n_S; assumption ] ]. +elim H; intros; elim H0; intros; elim (lt_n_O _ H2). +simpl in |- *; elim H; intros; elim H0; clear H0; intros; + induction x0 as [| x0 Hrecx0]; + [ left; 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. +intros; unfold ordered_Rlist in |- *; intros; apply (H (S i)); simpl in |- *; + replace (Rlength l1) with (S (pred (Rlength l1))); + [ apply lt_n_S; assumption + | symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *; + 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. +intros; induction l as [| r l Hrecl]; + [ elim H0 + | simpl in |- *; elim H0; intro; + [ rewrite H1; right; reflexivity + | apply Rle_trans with (pos_Rl l 0); + [ apply (H 0%nat); simpl in |- *; induction l as [| r0 l Hrecl0]; + [ elim H1 | simpl in |- *; apply lt_O_Sn ] + | apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ]. +Qed. + +Lemma RList_P6 : + forall l:Rlist, + ordered_Rlist l <-> + (forall i j:nat, + (i <= j)%nat -> (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j). +simple induction l; split; intro. +intros; right; reflexivity. +unfold ordered_Rlist in |- *; intros; simpl in H0; elim (lt_n_O _ H0). +intros; induction i as [| i Hreci]; + [ induction j as [| j Hrecj]; + [ right; reflexivity + | simpl in |- *; apply Rle_trans with (pos_Rl r0 0); + [ apply (H0 0%nat); simpl in |- *; simpl in H2; apply neq_O_lt; + red in |- *; intro; rewrite <- H3 in H2; + assert (H4 := lt_S_n _ _ H2); elim (lt_n_O _ H4) + | elim H; intros; apply H3; + [ apply RList_P4 with r; assumption + | apply le_O_n + | simpl in H2; apply lt_S_n; assumption ] ] ] + | induction j as [| j Hrecj]; + [ elim (le_Sn_O _ H1) + | simpl in |- *; elim H; intros; apply H3; + [ apply RList_P4 with r; assumption + | apply le_S_n; assumption + | simpl in H2; apply lt_S_n; assumption ] ] ]. +unfold ordered_Rlist in |- *; intros; apply H0; + [ apply le_n_Sn | simpl in |- *; simpl in H1; apply lt_n_S; assumption ]. +Qed. + +Lemma RList_P7 : + forall (l:Rlist) (x:R), + ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)). +intros; assert (H1 := RList_P6 l); elim H1; intros H2 _; assert (H3 := H2 H); + clear H1 H2; assert (H1 := RList_P3 l x); elim H1; + clear H1; intros; assert (H4 := H1 H0); elim H4; clear H4; + intros; elim H4; clear H4; intros; rewrite H4; + assert (H6 : Rlength l = S (pred (Rlength l))). +apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + rewrite <- H6 in H5; elim (lt_n_O _ H5). +apply H3; + [ rewrite H6 in H5; apply lt_n_Sm_le; assumption + | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H7 in H5; + elim (lt_n_O _ H5) ]. +Qed. + +Lemma RList_P8 : + forall (l:Rlist) (a x:R), In x (insert l a) <-> x = a \/ In x l. +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 in |- *; 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 ]. +Qed. + +Lemma RList_P9 : + forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2. +simple induction l1. +intros; split; intro; + [ simpl in H; right; assumption + | simpl in |- *; elim H; intro; [ elim H0 | assumption ] ]. +intros; split. +simpl in |- *; 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 ] ]. +intro; simpl in |- *; elim (H (insert l2 r) x); intros _ H1; apply H1; + elim H0; intro; + [ elim H2; intro; + [ right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left; assumption + | left; assumption ] + | right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption ]. +Qed. + +Lemma RList_P10 : + forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l). +intros; induction l as [| r l Hrecl]; + [ reflexivity + | simpl in |- *; case (Rle_dec r a); intro; + [ simpl in |- *; rewrite Hrecl; reflexivity | reflexivity ] ]. +Qed. + +Lemma RList_P11 : + forall l1 l2:Rlist, + Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat. +simple induction l1; + [ intro; reflexivity + | intros; simpl in |- *; rewrite (H (insert l2 r)); rewrite RList_P10; + apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; + rewrite S_INR; ring ]. +Qed. + +Lemma RList_P12 : + forall (l:Rlist) (i:nat) (f:R -> R), + (i < Rlength l)%nat -> pos_Rl (app_Rlist l f) i = f (pos_Rl l i). +simple induction l; + [ intros; elim (lt_n_O _ H) + | intros; induction i as [| i Hreci]; + [ reflexivity | simpl in |- *; apply H; apply lt_S_n; apply H0 ] ]. +Qed. + +Lemma RList_P13 : + forall (l:Rlist) (i:nat) (a:R), + (i < pred (Rlength l))%nat -> + pos_Rl (mid_Rlist l a) (S i) = (pos_Rl l i + pos_Rl l (S i)) / 2. +simple induction l. +intros; simpl in H; elim (lt_n_O _ H). +simple induction r0. +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) + in |- *; apply H0; simpl in |- *; apply lt_S_n; assumption. +Qed. + +Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l. +simple induction l; intros; + [ reflexivity | simpl in |- *; rewrite (H r); reflexivity ]. +Qed. + +Lemma RList_P15 : + forall l1 l2:Rlist, + 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. +intros; apply Rle_antisym. +induction l1 as [| r l1 Hrecl1]; + [ simpl in |- *; simpl in H1; right; symmetry in |- *; assumption + | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros; + assert + (H4 : + In (pos_Rl (cons r l1) 0) (cons r l1) \/ In (pos_Rl (cons r l1) 0) l2); + [ left; left; reflexivity + | assert (H5 := H3 H4); apply RList_P5; + [ apply RList_P2; assumption | assumption ] ] ]. +induction l1 as [| r l1 Hrecl1]; + [ simpl in |- *; simpl in H1; right; assumption + | assert + (H2 : + In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2)); + [ elim + (RList_P3 (cons_ORlist (cons r l1) l2) + (pos_Rl (cons_ORlist (cons r l1) l2) 0)); + intros; apply H3; exists 0%nat; split; + [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ] + | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) 0)); + intros; assert (H5 := H3 H2); elim H5; intro; + [ apply RList_P5; assumption + | rewrite H1; apply RList_P5; assumption ] ] ]. +Qed. + +Lemma RList_P16 : + forall l1 l2:Rlist, + ordered_Rlist l1 -> + ordered_Rlist l2 -> + pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 (pred (Rlength l2)) -> + pos_Rl (cons_ORlist l1 l2) (pred (Rlength (cons_ORlist l1 l2))) = + pos_Rl l1 (pred (Rlength l1)). +intros; apply Rle_antisym. +induction l1 as [| r l1 Hrecl1]. +simpl in |- *; simpl in H1; right; symmetry in |- *; assumption. +assert + (H2 : + In + (pos_Rl (cons_ORlist (cons r l1) l2) + (pred (Rlength (cons_ORlist (cons r l1) l2)))) + (cons_ORlist (cons r l1) l2)); + [ elim + (RList_P3 (cons_ORlist (cons r l1) l2) + (pos_Rl (cons_ORlist (cons r l1) l2) + (pred (Rlength (cons_ORlist (cons r l1) l2))))); + intros; apply H3; exists (pred (Rlength (cons_ORlist (cons r l1) l2))); + split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ] + | elim + (RList_P9 (cons r l1) l2 + (pos_Rl (cons_ORlist (cons r l1) l2) + (pred (Rlength (cons_ORlist (cons r l1) l2))))); + intros; assert (H5 := H3 H2); elim H5; intro; + [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ]. +induction l1 as [| r l1 Hrecl1]. +simpl in |- *; simpl in H1; right; assumption. +elim + (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); + intros; + assert + (H4 : + In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1) \/ + In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2); + [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1)) in |- *; + elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); + intros; apply H5; exists (Rlength l1); split; + [ reflexivity | simpl in |- *; apply lt_n_Sn ] + | assert (H5 := H3 H4); apply RList_P7; + [ apply RList_P2; assumption + | elim + (RList_P9 (cons r l1) l2 + (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); + intros; apply H7; left; + elim + (RList_P3 (cons r l1) + (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); + intros; apply H9; exists (pred (Rlength (cons r l1))); + split; [ reflexivity | simpl in |- *; apply lt_n_Sn ] ] ]. +Qed. + +Lemma RList_P17 : + forall (l1:Rlist) (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. +simple induction l1. +intros; elim H0. +intros; induction i as [| i Hreci]. +simpl in |- *; 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 in |- *; simpl in H2; elim H1; intro. +rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i); + [ apply Rle_trans with (pos_Rl r0 0); + [ apply (H0 0%nat); simpl in |- *; simpl in H3; apply neq_O_lt; + red in |- *; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3) + | elim (RList_P6 r0); intros; apply H5; + [ apply RList_P4 with r; assumption + | apply le_O_n + | simpl in H3; apply lt_S_n; apply lt_trans with (Rlength r0); + [ apply H3 | apply lt_n_Sn ] ] ] + | elim (Rlt_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); + [ apply H3 + | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; 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. +simple induction l; intros; + [ reflexivity | simpl in |- *; rewrite H; reflexivity ]. +Qed. + +Lemma RList_P19 : + forall l:Rlist, + l <> nil -> exists r : R, (exists r0 : Rlist, l = cons r r0). +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 -> + exists r : R, + (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). +intros; induction l as [| r l Hrecl]; + [ simpl in H; elim (le_Sn_O _ H) + | induction l as [| r0 l Hrecl0]; + [ simpl in H; elim (le_Sn_O _ (le_S_n _ _ H)) + | exists r; exists r0; exists l; reflexivity ] ]. +Qed. + +Lemma RList_P21 : forall l l':Rlist, l = l' -> Rtail l = Rtail l'. +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. +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. +simple induction l1; + [ intro; reflexivity | intros; simpl in |- *; rewrite H; reflexivity ]. +Qed. + +Lemma RList_P24 : + forall l1 l2:Rlist, + l2 <> nil -> + pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2))) = + pos_Rl l2 (pred (Rlength l2)). +simple induction l1. +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)); + [ reflexivity + | simpl in |- *; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; + rewrite S_INR; ring ] + | simpl in |- *; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR; + rewrite S_INR; ring ]. +Qed. + +Lemma RList_P25 : + forall l1 l2:Rlist, + ordered_Rlist l1 -> + ordered_Rlist l2 -> + pos_Rl l1 (pred (Rlength l1)) <= pos_Rl l2 0 -> + ordered_Rlist (cons_Rlist l1 l2). +simple induction l1. +intros; simpl in |- *; assumption. +simple induction r0. +intros; simpl in |- *; simpl in H2; unfold ordered_Rlist in |- *; intros; + simpl in H3. +induction i as [| i Hreci]. +simpl in |- *; assumption. +change (pos_Rl l2 i <= pos_Rl l2 (S i)) in |- *; apply (H1 i); apply lt_S_n; + replace (S (pred (Rlength l2))) with (Rlength l2); + [ assumption + | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + rewrite <- H4 in H3; elim (lt_n_O _ H3) ]. +intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)). +apply H0; try assumption. +apply RList_P4 with r; assumption. +unfold ordered_Rlist in |- *; intros; simpl in H4; + induction i as [| i Hreci]. +simpl in |- *; apply (H1 0%nat); simpl in |- *; apply lt_O_Sn. +change + (pos_Rl (cons_Rlist (cons r1 r2) l2) i <= + pos_Rl (cons_Rlist (cons r1 r2) l2) (S i)) in |- *; + apply (H i); simpl in |- *; 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. +simple induction l1. +intros; elim (lt_n_O _ H). +intros; induction i as [| i Hreci]. +apply RList_P22; discriminate. +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. +simple induction l1; intros; + [ reflexivity | simpl in |- *; rewrite (H l2 l3); reflexivity ]. +Qed. + +Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l. +simple induction l; + [ reflexivity | intros; simpl in |- *; 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). +simple induction l2. +intros; rewrite RList_P28 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). +inversion H0. +rewrite <- minus_n_n; simpl in |- *; rewrite RList_P26. +clear l2 r0 H i H0 H1 H2; induction l1 as [| r0 l1 Hrecl1]. +reflexivity. +simpl in |- *; assumption. +rewrite RList_P23; rewrite plus_comm; simpl in |- *; apply lt_n_Sn. +replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))). +rewrite H3; simpl in |- *; + 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 in |- *; rewrite <- H3; + apply le_n_S; assumption. +repeat rewrite RList_P23; simpl in |- *; rewrite RList_P23 in H1; + rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1)); + simpl in |- *; rewrite plus_comm; apply H1. +rewrite RList_P23; rewrite plus_comm; reflexivity. +change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *; + apply minus_Sn_m; assumption. +replace (cons r r0) with (cons_Rlist (cons r nil) r0); + [ symmetry in |- *; apply RList_P27 | reflexivity ]. +Qed. |