diff options
Diffstat (limited to 'theories/Reals/RList.v')
| -rw-r--r-- | theories/Reals/RList.v | 1137 |
1 files changed, 588 insertions, 549 deletions
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 551aec98..19f2b4ff 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -5,208 +5,217 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: RList.v 5920 2004-07-16 20:01:26Z herbelin $ i*) + +(*i $Id: RList.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. Open Local Scope R_scope. Inductive Rlist : Type := - | nil : Rlist - | cons : R -> Rlist -> Rlist. +| 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' + | 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') + | nil => 0%nat + | cons a l' => S (Rlength l') end. Fixpoint MaxRlist (l:Rlist) : R := match l with - | nil => 0 - | cons a l1 => + | nil => 0 + | cons a l1 => match l1 with - | nil => a - | cons a' l2 => Rmax a (MaxRlist l1) + | nil => a + | cons a' l2 => Rmax a (MaxRlist l1) end end. Fixpoint MinRlist (l:Rlist) : R := match l with - | nil => 1 - | cons a l1 => + | nil => 1 + | cons a l1 => match l1 with - | nil => a - | cons a' l2 => Rmin a (MinRlist l1) + | 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. +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 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) + | 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. +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 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. + forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x). +Proof. + 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. + forall l:Rlist, (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 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. + forall (l:Rlist) (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]. + 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. + forall l:Rlist, (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 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 + | 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 ] ]. + forall (l:Rlist) (a:R), + (0 < Rlength l)%nat -> + pos_Rl (cons a l) (Rlength l) = pos_Rl l (pred (Rlength l)). +Proof. + 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 ]. + forall (l:Rlist) (x:R), + In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i). +Proof. + 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) -> + 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. + Rlength l = Rlength l' /\ + (forall i:nat, (i < Rlength 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)). + 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 := @@ -214,531 +223,561 @@ Definition ordered_Rlist (l:Rlist) : Prop := Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist := match l with - | nil => cons x nil - | cons a l' => + | nil => cons x nil + | cons a l' => match Rle_dec a x with - | left _ => cons a (insert l' x) - | right _ => cons x l + | 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) + | 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) + | 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) + | 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) + | 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' + | 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 + | 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 ] ]. + forall (l:Rlist) (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]; + [ 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) ]. + forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a). +Proof. + 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 ]. + forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2). +Proof. + 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 ] ]. + forall (l:Rlist) (x:R), + In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength 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 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) ]. + forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1. +Proof. + 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 ] ] ] ]. + forall (l:Rlist) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x. +Proof. + 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, + 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 ]. +Proof. + 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) ]. + forall (l:Rlist) (x:R), + ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength 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))). + 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 ]. + 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 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 ]. + forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2. +Proof. + 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 ] ]. + forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l). +Proof. + 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 ]. + forall l1 l2:Rlist, + Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat. +Proof. + 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 ] ]. + forall (l:Rlist) (i:nat) (f:R -> R), + (i < Rlength l)%nat -> pos_Rl (app_Rlist l f) i = f (pos_Rl l i). +Proof. + 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. + 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. +Proof. + 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 ]. +Proof. + 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 ] ] ]. + 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. +Proof. + 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) + 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)). +Proof. + 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; 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 ] ] ]. + 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) ] ]. + 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. +Proof. + 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 ]. + forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l. +Proof. + 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 ]. + forall l:Rlist, + l <> nil -> exists r : R, (exists r0 : Rlist, l = cons 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: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 ] ]. + (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). +Proof. + 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. +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. -simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ]. + forall l1 l2:Rlist, l1 <> nil -> pos_Rl (cons_Rlist 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. -simple induction l1; - [ intro; reflexivity | intros; simpl in |- *; rewrite H; reflexivity ]. + forall l1 l2:Rlist, + Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat. +Proof. + 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 ]. + forall l1 l2:Rlist, + l2 <> nil -> + pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2))) = + pos_Rl l2 (pred (Rlength l2)). +Proof. + 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. + 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). +Proof. + 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. + forall (l1 l2:Rlist) (i:nat), + (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i. +Proof. + 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 ]. + 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 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 ]. +Proof. + 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 ]. + 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). +Proof. + 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. |