diff options
Diffstat (limited to 'theories7/Reals/RList.v')
| -rw-r--r-- | theories7/Reals/RList.v | 427 |
1 files changed, 427 insertions, 0 deletions
diff --git a/theories7/Reals/RList.v b/theories7/Reals/RList.v new file mode 100644 index 00000000..b89296fb --- /dev/null +++ b/theories7/Reals/RList.v @@ -0,0 +1,427 @@ +(************************************************************************) +(* 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.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) + +Require Rbase. +Require Rfunctions. +V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. +Open Local Scope R_scope. + +Inductive Rlist : Type := +| nil : Rlist +| cons : R -> Rlist -> Rlist. + +Fixpoint In [x:R;l:Rlist] : Prop := +Cases l of +| nil => False +| (cons a l') => ``x==a``\/(In x l') end. + +Fixpoint Rlength [l:Rlist] : nat := +Cases l of +| nil => O +| (cons a l') => (S (Rlength l')) end. + +Fixpoint MaxRlist [l:Rlist] : R := + Cases l of + | nil => R0 + | (cons a l1) => + Cases l1 of + | nil => a + | (cons a' l2) => (Rmax a (MaxRlist l1)) + end +end. + +Fixpoint MinRlist [l:Rlist] : R := +Cases l of + | nil => R1 + | (cons a l1) => + Cases l1 of + | nil => a + | (cons a' l2) => (Rmin a (MinRlist l1)) + end +end. + +Lemma MaxRlist_P1 : (l:Rlist;x:R) (In x l)->``x<=(MaxRlist l)``. +Intros; Induction l. +Simpl in H; Elim H. +Induction l. +Simpl in H; Elim H; Intro. +Simpl; 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; Case (total_order_Rle r (MaxRlist (cons r0 l))); Intro. +Apply Hrecl; Simpl; Tauto. +Apply Rle_trans with (MaxRlist (cons r0 l)); [Apply Hrecl; Simpl; Tauto | Left; Auto with real]. +Unfold Rmax; Case (total_order_Rle r (MaxRlist (cons r0 l))); Intro. +Apply Hrecl; Simpl; Tauto. +Apply Rle_trans with (MaxRlist (cons r0 l)); [Apply Hrecl; Simpl; Tauto | Left; Auto with real]. +Reflexivity. +Qed. + +Fixpoint AbsList [l:Rlist] : R->Rlist := +[x:R] Cases l of +| nil => nil +| (cons a l') => (cons ``(Rabsolu (a-x))/2`` (AbsList l' x)) +end. + +Lemma MinRlist_P1 : (l:Rlist;x:R) (In x l)->``(MinRlist l)<=x``. +Intros; Induction l. +Simpl in H; Elim H. +Induction l. +Simpl in H; Elim H; Intro. +Simpl; Right; Symmetry; 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; Case (total_order_Rle r (MinRlist (cons r0 l))); Intro. +Apply Rle_trans with (MinRlist (cons r0 l)). +Assumption. +Apply Hrecl; Simpl; Tauto. +Apply Hrecl; Simpl; Tauto. +Apply Rle_trans with (MinRlist (cons r0 l)). +Apply Rmin_r. +Apply Hrecl; Simpl; Tauto. +Reflexivity. +Qed. + +Lemma AbsList_P1 : (l:Rlist;x,y:R) (In y l) -> (In ``(Rabsolu (y-x))/2`` (AbsList l x)). +Intros; Induction l. +Elim H. +Simpl; Simpl in H; Elim H; Intro. +Left; Rewrite H0; Reflexivity. +Right; Apply Hrecl; Assumption. +Qed. + +Lemma MinRlist_P2 : (l:Rlist) ((y:R)(In y l)->``0<y``)->``0<(MinRlist l)``. +Intros; Induction l. +Apply Rlt_R0_R1. +Induction l. +Simpl; Apply H; Simpl; Tauto. +Replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). +Unfold Rmin; Case (total_order_Rle r (MinRlist (cons r0 l))); Intro. +Apply H; Simpl; Tauto. +Apply Hrecl; Intros; Apply H; Simpl; Simpl in H0; Tauto. +Reflexivity. +Qed. + +Lemma AbsList_P2 : (l:Rlist;x,y:R) (In y (AbsList l x)) -> (EXT z : R | (In z l)/\``y==(Rabsolu (z-x))/2``). +Intros; Induction l. +Elim H. +Elim H; Intro. +Exists r; Split. +Simpl; Tauto. +Assumption. +Assert H1 := (Hrecl H0); Elim H1; Intros; Elim H2; Clear H2; Intros; Exists x0; Simpl; Simpl in H2; Tauto. +Qed. + +Lemma MaxRlist_P2 : (l:Rlist) (EXT y:R | (In y l)) -> (In (MaxRlist l) l). +Intros; Induction l. +Simpl in H; Elim H; Trivial. +Induction l. +Simpl; Left; Reflexivity. +Change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))); Unfold Rmax; Case (total_order_Rle r (MaxRlist (cons r0 l))); Intro. +Right; Apply Hrecl; Exists r0; Left; Reflexivity. +Left; Reflexivity. +Qed. + +Fixpoint pos_Rl [l:Rlist] : nat->R := +[i:nat] Cases l of +| nil => R0 +| (cons a l') => + Cases i of + | O => a + | (S i') => (pos_Rl l' i') + end +end. + +Lemma pos_Rl_P1 : (l:Rlist;a:R) (lt O (Rlength l)) -> (pos_Rl (cons a l) (Rlength l))==(pos_Rl l (pred (Rlength l))). +Intros; Induction l; [Elim (lt_n_O ? H) | Simpl; Case (Rlength l); [Reflexivity | Intro; Reflexivity]]. +Qed. + +Lemma pos_Rl_P2 : (l:Rlist;x:R) (In x l)<->(EX i:nat | (lt i (Rlength l))/\x==(pos_Rl l i)). +Intros; Induction l. +Split; Intro; [Elim H | Elim H; Intros; Elim H0; Intros; Elim (lt_n_O ? H1)]. +Split; Intro. +Elim H; Intro. +Exists O; Split; [Simpl; Apply lt_O_Sn | Simpl; 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; 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; Apply S_pred with O; Assumption. +Exists (pred x0); Split; [Simpl in H1; Apply lt_S_n; Rewrite H5; Assumption | Rewrite <- H5 in H2; Simpl in H2; Assumption]. +Qed. + +Lemma Rlist_P1 : (l:Rlist;P:R->R->Prop) ((x:R)(In x l)->(EXT y:R | (P x y))) -> (EXT l':Rlist | (Rlength l)=(Rlength l')/\(i:nat) (lt i (Rlength l))->(P (pos_Rl l i) (pos_Rl l' i))). +Intros; Induction l. +Exists nil; Intros; Split; [Reflexivity | Intros; Simpl in H0; Elim (lt_n_O ? H0)]. +Assert H0 : (In r (cons r l)). +Simpl; Left; Reflexivity. +Assert H1 := (H ? H0); Assert H2 : (x:R)(In x l)->(EXT 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); Intros; Elim H5; Clear H5; Intros; Split. +Simpl; Rewrite H5; Reflexivity. +Intros; Elim (zerop i); Intro. +Rewrite a; Simpl; Assumption. +Assert H8 : i=(S (pred i)). +Apply S_pred with O; Assumption. +Rewrite H8; Simpl; Apply H6; Simpl in H7; Apply lt_S_n; Rewrite <- H8; Assumption. +Qed. + +Definition ordered_Rlist [l:Rlist] : Prop := (i:nat) (lt i (pred (Rlength l))) -> (Rle (pos_Rl l i) (pos_Rl l (S i))). + +Fixpoint insert [l:Rlist] : R->Rlist := +[x:R] Cases l of +| nil => (cons x nil) +| (cons a l') => + Cases (total_order_Rle a x) of + | (leftT _) => (cons a (insert l' x)) + | (rightT _) => (cons x l) + end +end. + +Fixpoint cons_Rlist [l:Rlist] : Rlist->Rlist := +[k:Rlist] Cases l of +| nil => k +| (cons a l') => (cons a (cons_Rlist l' k)) end. + +Fixpoint cons_ORlist [k:Rlist] : Rlist->Rlist := +[l:Rlist] Cases k of +| nil => l +| (cons a k') => (cons_ORlist k' (insert l a)) +end. + +Fixpoint app_Rlist [l:Rlist] : (R->R)->Rlist := +[f:R->R] Cases l of +| nil => nil +| (cons a l') => (cons (f a) (app_Rlist l' f)) +end. + +Fixpoint mid_Rlist [l:Rlist] : R->Rlist := +[x:R] Cases l of +| nil => nil +| (cons a l') => (cons ``(x+a)/2`` (mid_Rlist l' a)) +end. + +Definition Rtail [l:Rlist] : Rlist := +Cases l of +| nil => nil +| (cons a l') => l' +end. + +Definition FF [l:Rlist;f:R->R] : Rlist := +Cases l of +| nil => nil +| (cons a l') => (app_Rlist (mid_Rlist l' a) f) +end. + +Lemma RList_P0 : (l:Rlist;a:R) ``(pos_Rl (insert l a) O) == a`` \/ ``(pos_Rl (insert l a) O) == (pos_Rl l O)``. +Intros; Induction l; [Left; Reflexivity | Simpl; Case (total_order_Rle r a); Intro; [Right; Reflexivity | Left; Reflexivity]]. +Qed. + +Lemma RList_P1 : (l:Rlist;a:R) (ordered_Rlist l) -> (ordered_Rlist (insert l a)). +Intros; Induction l. +Simpl; Unfold ordered_Rlist; Intros; Simpl in H0; Elim (lt_n_O ? H0). +Simpl; Case (total_order_Rle r a); Intro. +Assert H1 : (ordered_Rlist l). +Unfold ordered_Rlist; Unfold ordered_Rlist in H; Intros; Assert H1 : (lt (S i) (pred (Rlength (cons r l)))); [Simpl; Replace (Rlength l) with (S (pred (Rlength l))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Simpl in H0; Elim (lt_n_O ? H0)] | Apply (H ? H1)]. +Assert H2 := (Hrecl H1); Unfold ordered_Rlist; Intros; Induction i. +Simpl; Assert H3 := (RList_P0 l a); Elim H3; Intro. +Rewrite H4; Assumption. +Induction l; [Simpl; Assumption | Rewrite H4; Apply (H O); Simpl; Apply lt_O_Sn]. +Simpl; Apply H2; Simpl in H0; Apply lt_S_n; Replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a)); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H3 in H0; Elim (lt_n_O ? H0)]. +Unfold ordered_Rlist; Intros; Induction i; [Simpl; Auto with real | Change ``(pos_Rl (cons r l) i)<=(pos_Rl (cons r l) (S i))``; Apply H; Simpl in H0; Simpl; Apply (lt_S_n ? ? H0)]. +Qed. + +Lemma RList_P2 : (l1,l2:Rlist) (ordered_Rlist l2) ->(ordered_Rlist (cons_ORlist l1 l2)). +Induction l1; [Intros; Simpl; Apply H | Intros; Simpl; Apply H; Apply RList_P1; Assumption]. +Qed. + +Lemma RList_P3 : (l:Rlist;x:R) (In x l) <-> (EX i:nat | x==(pos_Rl l i)/\(lt i (Rlength l))). +Intros; Split; Intro; Induction l. +Elim H. +Elim H; Intro; [Exists O; Split; [Apply H0 | Simpl; Apply lt_O_Sn] | Elim (Hrecl H0); Intros; Elim H1; Clear H1; Intros; Exists (S x0); Split; [Apply H1 | Simpl; Apply lt_n_S; Assumption]]. +Elim H; Intros; Elim H0; Intros; Elim (lt_n_O ? H2). +Simpl; Elim H; Intros; Elim H0; Clear H0; Intros; Induction x0; [Left; Apply H0 | Right; Apply Hrecl; Exists x0; Split; [Apply H0 | Simpl in H1; Apply lt_S_n; Assumption]]. +Qed. + +Lemma RList_P4 : (l1:Rlist;a:R) (ordered_Rlist (cons a l1)) -> (ordered_Rlist l1). +Intros; Unfold ordered_Rlist; Intros; Apply (H (S i)); Simpl; Replace (Rlength l1) with (S (pred (Rlength l1))); [Apply lt_n_S; Assumption | Symmetry; Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H1 in H0; Elim (lt_n_O ? H0)]. +Qed. + +Lemma RList_P5 : (l:Rlist;x:R) (ordered_Rlist l) -> (In x l) -> ``(pos_Rl l O)<=x``. +Intros; Induction l; [Elim H0 | Simpl; Elim H0; Intro; [Rewrite H1; Right; Reflexivity | Apply Rle_trans with (pos_Rl l O); [Apply (H O); Simpl; Induction l; [Elim H1 | Simpl; Apply lt_O_Sn] | Apply Hrecl; [EApply RList_P4; Apply H | Assumption]]]]. +Qed. + +Lemma RList_P6 : (l:Rlist) (ordered_Rlist l)<->((i,j:nat)(le i j)->(lt j (Rlength l))->``(pos_Rl l i)<=(pos_Rl l j)``). +Induction l; Split; Intro. +Intros; Right; Reflexivity. +Unfold ordered_Rlist; Intros; Simpl in H0; Elim (lt_n_O ? H0). +Intros; Induction i; [Induction j; [Right; Reflexivity | Simpl; Apply Rle_trans with (pos_Rl r0 O); [Apply (H0 O); Simpl; Simpl in H2; Apply neq_O_lt; Red; 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; [Elim (le_Sn_O ? H1) | Simpl; 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; Intros; Apply H0; [Apply le_n_Sn | Simpl; Simpl in H1; Apply lt_n_S; Assumption]. +Qed. + +Lemma RList_P7 : (l:Rlist;x:R) (ordered_Rlist l) -> (In x l) -> ``x<=(pos_Rl l (pred (Rlength l)))``. +Intros; Assert H1 := (RList_P6 l); Elim H1; Intros H2 _; Assert H3 := (H2 H); Clear H1 H2; Assert H1 := (RList_P3 l x); Elim H1; Clear H1; Intros; Assert H4 := (H1 H0); Elim H4; Clear H4; Intros; Elim H4; Clear H4; Intros; Rewrite H4; Assert H6 : (Rlength l)=(S (pred (Rlength l))). +Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H6 in H5; Elim (lt_n_O ? H5). +Apply H3; [Rewrite H6 in H5; Apply lt_n_Sm_le; Assumption | Apply lt_pred_n_n; Apply neq_O_lt; Red; Intro; Rewrite <- H7 in H5; Elim (lt_n_O ? H5)]. +Qed. + +Lemma RList_P8 : (l:Rlist;a,x:R) (In x (insert l a)) <-> x==a\/(In x l). +Induction l. +Intros; Split; Intro; Simpl in H; Apply H. +Intros; Split; Intro; [Simpl in H0; Generalize H0; Case (total_order_Rle 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 (total_order_Rle 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 : (l1,l2:Rlist;x:R) (In x (cons_ORlist l1 l2)) <-> (In x l1)\/(In x l2). +Induction l1. +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]]. +Intro; Simpl; Elim (H (insert l2 r) x); Intros _ H1; Apply H1; Elim H0; Intro; [Elim H2; Intro; [Right; Elim (RList_P8 l2 r x); Intros _ H4; Apply H4; Left; Assumption | Left; Assumption] | Right; Elim (RList_P8 l2 r x); Intros _ H3; Apply H3; Right; Assumption]. +Qed. + +Lemma RList_P10 : (l:Rlist;a:R) (Rlength (insert l a))==(S (Rlength l)). +Intros; Induction l; [Reflexivity | Simpl; Case (total_order_Rle r a); Intro; [Simpl; Rewrite Hrecl; Reflexivity | Reflexivity]]. +Qed. + +Lemma RList_P11 : (l1,l2:Rlist) (Rlength (cons_ORlist l1 l2))=(plus (Rlength l1) (Rlength l2)). +Induction l1; [Intro; Reflexivity | Intros; Simpl; Rewrite (H (insert l2 r)); Rewrite RList_P10; Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring]. +Qed. + +Lemma RList_P12 : (l:Rlist;i:nat;f:R->R) (lt i (Rlength l)) -> (pos_Rl (app_Rlist l f) i)==(f (pos_Rl l i)). +Induction l; [Intros; Elim (lt_n_O ? H) | Intros; Induction i; [Reflexivity | Simpl; Apply H; Apply lt_S_n; Apply H0]]. +Qed. + +Lemma RList_P13 : (l:Rlist;i:nat;a:R) (lt i (pred (Rlength l))) -> ``(pos_Rl (mid_Rlist l a) (S i)) == ((pos_Rl l i)+(pos_Rl l (S i)))/2``. +Induction l. +Intros; Simpl in H; Elim (lt_n_O ? H). +Induction r0. +Intros; Simpl in H0; Elim (lt_n_O ? H0). +Intros; Simpl in H1; Induction i. +Reflexivity. +Change ``(pos_Rl (mid_Rlist (cons r1 r2) r) (S i)) == ((pos_Rl (cons r1 r2) i)+(pos_Rl (cons r1 r2) (S i)))/2``; Apply H0; Simpl; Apply lt_S_n; Assumption. +Qed. + +Lemma RList_P14 : (l:Rlist;a:R) (Rlength (mid_Rlist l a))=(Rlength l). +Induction l; Intros; [Reflexivity | Simpl; Rewrite (H r); Reflexivity]. +Qed. + +Lemma RList_P15 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> (pos_Rl l1 O)==(pos_Rl l2 O) -> (pos_Rl (cons_ORlist l1 l2) O)==(pos_Rl l1 O). +Intros; Apply Rle_antisym. +Induction l1; [Simpl; Simpl in H1; Right; Symmetry; 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; [Simpl; Simpl in H1; Right; Assumption | Assert H2 : (In (pos_Rl (cons_ORlist (cons r l1) l2) (0)) (cons_ORlist (cons r l1) l2)); [Elim (RList_P3 (cons_ORlist (cons r l1) l2) (pos_Rl (cons_ORlist (cons r l1) l2) (0))); Intros; Apply H3; Exists O; Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_O_Sn] | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) (0))); Intros; Assert H5 := (H3 H2); Elim H5; Intro; [Apply RList_P5; Assumption | Rewrite H1; Apply RList_P5; Assumption]]]. +Qed. + +Lemma RList_P16 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> (pos_Rl l1 (pred (Rlength l1)))==(pos_Rl l2 (pred (Rlength l2))) -> (pos_Rl (cons_ORlist l1 l2) (pred (Rlength (cons_ORlist l1 l2))))==(pos_Rl l1 (pred (Rlength l1))). +Intros; Apply Rle_antisym. +Induction l1. +Simpl; Simpl in H1; Right; Symmetry; Assumption. +Assert H2 : (In (pos_Rl (cons_ORlist (cons r l1) l2) (pred (Rlength (cons_ORlist (cons r l1) l2)))) (cons_ORlist (cons r l1) l2)); [Elim (RList_P3 (cons_ORlist (cons r l1) l2) (pos_Rl (cons_ORlist (cons r l1) l2) (pred (Rlength (cons_ORlist (cons r l1) l2))))); Intros; Apply H3; Exists (pred (Rlength (cons_ORlist (cons r l1) l2))); Split; [Reflexivity | Rewrite RList_P11; Simpl; Apply lt_n_Sn] | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) (pred (Rlength (cons_ORlist (cons r l1) l2))))); Intros; Assert H5 := (H3 H2); Elim H5; Intro; [Apply RList_P7; Assumption | Rewrite H1; Apply RList_P7; Assumption]]. +Induction l1. +Simpl; Simpl in H1; Right; Assumption. +Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); Intros; Assert H4 : (In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1))\/(In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2); [Left; Change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1)); Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); Intros; Apply H5; Exists (Rlength l1); Split; [Reflexivity | Simpl; Apply lt_n_Sn] | Assert H5 := (H3 H4); Apply RList_P7; [Apply RList_P2; Assumption | Elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); Intros; Apply H7; Left; Elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); Intros; Apply H9; Exists (pred (Rlength (cons r l1))); Split; [Reflexivity | Simpl; Apply lt_n_Sn]]]. +Qed. + +Lemma RList_P17 : (l1:Rlist;x:R;i:nat) (ordered_Rlist l1) -> (In x l1) -> ``(pos_Rl l1 i)<x`` -> (lt i (pred (Rlength l1))) -> ``(pos_Rl l1 (S i))<=x``. +Induction l1. +Intros; Elim H0. +Intros; Induction i. +Simpl; Elim H1; Intro; [Simpl in H2; Rewrite H4 in H2; Elim (Rlt_antirefl ? H2) | Apply RList_P5; [Apply RList_P4 with r; Assumption | Assumption]]. +Simpl; Simpl in H2; Elim H1; Intro. +Rewrite H4 in H2; Assert H5 : ``r<=(pos_Rl r0 i)``; [Apply Rle_trans with (pos_Rl r0 O); [Apply (H0 O); Simpl; Simpl in H3; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3) | Elim (RList_P6 r0); Intros; Apply H5; [Apply RList_P4 with r; Assumption | Apply le_O_n | Simpl in H3; Apply lt_S_n; Apply lt_trans with (Rlength r0); [Apply H3 | Apply lt_n_Sn]]] | Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H5 H2))]. +Apply H; Try Assumption; [Apply RList_P4 with r; Assumption | Simpl in H3; Apply lt_S_n; Replace (S (pred (Rlength r0))) with (Rlength r0); [Apply H3 | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H5 in H3; Elim (lt_n_O ? H3)]]. +Qed. + +Lemma RList_P18 : (l:Rlist;f:R->R) (Rlength (app_Rlist l f))=(Rlength l). +Induction l; Intros; [Reflexivity | Simpl; Rewrite H; Reflexivity]. +Qed. + +Lemma RList_P19 : (l:Rlist) ~l==nil -> (EXT r:R | (EXT r0:Rlist | l==(cons r r0))). +Intros; Induction l; [Elim H; Reflexivity | Exists r; Exists l; Reflexivity]. +Qed. + +Lemma RList_P20 : (l:Rlist) (le (2) (Rlength l)) -> (EXT r:R | (EXT r1:R | (EXT l':Rlist | l==(cons r (cons r1 l'))))). +Intros; Induction l; [Simpl in H; Elim (le_Sn_O ? H) | Induction l; [Simpl in H; Elim (le_Sn_O ? (le_S_n ? ? H)) | Exists r; Exists r0; Exists l; Reflexivity]]. +Qed. + +Lemma RList_P21 : (l,l':Rlist) l==l' -> (Rtail l)==(Rtail l'). +Intros; Rewrite H; Reflexivity. +Qed. + +Lemma RList_P22 : (l1,l2:Rlist) ~l1==nil -> (pos_Rl (cons_Rlist l1 l2) O)==(pos_Rl l1 O). +Induction l1; [Intros; Elim H; Reflexivity | Intros; Reflexivity]. +Qed. + +Lemma RList_P23 : (l1,l2:Rlist) (Rlength (cons_Rlist l1 l2))==(plus (Rlength l1) (Rlength l2)). +Induction l1; [Intro; Reflexivity | Intros; Simpl; Rewrite H; Reflexivity]. +Qed. + +Lemma RList_P24 : (l1,l2:Rlist) ~l2==nil -> (pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2)))) == (pos_Rl l2 (pred (Rlength l2))). +Induction l1. +Intros; Reflexivity. +Intros; Rewrite <- (H l2 H0); Induction l2. +Elim H0; Reflexivity. +Do 2 Rewrite RList_P23; Replace (plus (Rlength (cons r r0)) (Rlength (cons r1 l2))) with (S (S (plus (Rlength r0) (Rlength l2)))); [Replace (plus (Rlength r0) (Rlength (cons r1 l2))) with (S (plus (Rlength r0) (Rlength l2))); [Reflexivity | Simpl; Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring] | Simpl; Apply INR_eq; Do 3 Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring]. +Qed. + +Lemma RList_P25 : (l1,l2:Rlist) (ordered_Rlist l1) -> (ordered_Rlist l2) -> ``(pos_Rl l1 (pred (Rlength l1)))<=(pos_Rl l2 O)`` -> (ordered_Rlist (cons_Rlist l1 l2)). +Induction l1. +Intros; Simpl; Assumption. +Induction r0. +Intros; Simpl; Simpl in H2; Unfold ordered_Rlist; Intros; Simpl in H3. +Induction i. +Simpl; Assumption. +Change ``(pos_Rl l2 i)<=(pos_Rl l2 (S i))``; Apply (H1 i); Apply lt_S_n; Replace (S (pred (Rlength l2))) with (Rlength l2); [Assumption | Apply S_pred with O; Apply neq_O_lt; Red; Intro; Rewrite <- H4 in H3; Elim (lt_n_O ? H3)]. +Intros; Clear H; Assert H : (ordered_Rlist (cons_Rlist (cons r1 r2) l2)). +Apply H0; Try Assumption. +Apply RList_P4 with r; Assumption. +Unfold ordered_Rlist; Intros; Simpl in H4; Induction i. +Simpl; Apply (H1 O); Simpl; Apply lt_O_Sn. +Change ``(pos_Rl (cons_Rlist (cons r1 r2) l2) i)<=(pos_Rl (cons_Rlist (cons r1 r2) l2) (S i))``; Apply (H i); Simpl; Apply lt_S_n; Assumption. +Qed. + +Lemma RList_P26 : (l1,l2:Rlist;i:nat) (lt i (Rlength l1)) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l1 i). +Induction l1. +Intros; Elim (lt_n_O ? H). +Intros; Induction i. +Apply RList_P22; Discriminate. +Apply (H l2 i); Simpl in H0; Apply lt_S_n; Assumption. +Qed. + +Lemma RList_P27 : (l1,l2,l3:Rlist) (cons_Rlist l1 (cons_Rlist l2 l3))==(cons_Rlist (cons_Rlist l1 l2) l3). +Induction l1; Intros; [Reflexivity | Simpl; Rewrite (H l2 l3); Reflexivity]. +Qed. + +Lemma RList_P28 : (l:Rlist) (cons_Rlist l nil)==l. +Induction l; [Reflexivity | Intros; Simpl; Rewrite H; Reflexivity]. +Qed. + +Lemma RList_P29 : (l2,l1:Rlist;i:nat) (le (Rlength l1) i) -> (lt i (Rlength (cons_Rlist l1 l2))) -> (pos_Rl (cons_Rlist l1 l2) i)==(pos_Rl l2 (minus i (Rlength l1))). +Induction l2. +Intros; Rewrite RList_P28 in H0; Elim (lt_n_n ? (le_lt_trans ? ? ? H H0)). +Intros; Replace (cons_Rlist l1 (cons r r0)) with (cons_Rlist (cons_Rlist l1 (cons r nil)) r0). +Inversion H0. +Rewrite <- minus_n_n; Simpl; Rewrite RList_P26. +Clear l2 r0 H i H0 H1 H2; Induction l1. +Reflexivity. +Simpl; Assumption. +Rewrite RList_P23; Rewrite plus_sym; Simpl; Apply lt_n_Sn. +Replace (minus (S m) (Rlength l1)) with (S (minus (S m) (S (Rlength l1)))). +Rewrite H3; Simpl; Replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))). +Apply (H (cons_Rlist l1 (cons r nil)) i). +Rewrite RList_P23; Rewrite plus_sym; Simpl; Rewrite <- H3; Apply le_n_S; Assumption. +Repeat Rewrite RList_P23; Simpl; Rewrite RList_P23 in H1; Rewrite plus_sym in H1; Simpl in H1; Rewrite (plus_sym (Rlength l1)); Simpl; Rewrite plus_sym; Apply H1. +Rewrite RList_P23; Rewrite plus_sym; Reflexivity. +Change (S (minus m (Rlength l1)))=(minus (S m) (Rlength l1)); Apply minus_Sn_m; Assumption. +Replace (cons r r0) with (cons_Rlist (cons r nil) r0); [Symmetry; Apply RList_P27 | Reflexivity]. +Qed. |