path: root/theories/Reals/RList.v

(************************************************************************)
(*  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 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.

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.
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)
  end.

Lemma MinRlist_P1 : forall (l:Rlist) (x:R), In x l -> MinRlist l <= x.
Proof.
  intros; induction  l as [| r l Hrecl].
  simpl in H; elim H.
  induction  l as [| r0 l Hrecl0].
  simpl in H; elim H; intro.
  simpl 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).
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.
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.
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.
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
  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)).
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).
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) ->
    exists l' : Rlist,
      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 :=
  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.
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).
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).
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).
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.
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.
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,
      (i <= j)%nat -> (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j).
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)).
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.
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.
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).
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.
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).
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.
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.
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.
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)).
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; 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.
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.
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).
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 ->
    exists r : R,
      (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'.
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.
Proof.
  simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ].
Qed.

Lemma RList_P23 :
  forall l1 l2:Rlist,
    Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.
Proof.
  simple induction l1;
    [ intro; reflexivity | intros; simpl 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)).
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).
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.
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.
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.
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).
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.