Library Coq.Reals.RList

Require Import Rbase.
Require Import Rfunctions.
Local Open Scope R_scope.

Inductive Rlist : Type :=
| nil : Rlist
| cons : R -> Rlist -> Rlist.

Fixpoint In (x:R) (l:Rlist) : Prop :=
  match l with
    | nil => False
    | cons a l' => x = a \/ In x l'
  end.

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.

Fixpoint AbsList (l:Rlist) (x:R) : 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.

Lemma AbsList_P1 :
  forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x).

Lemma MinRlist_P2 :
  forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l.

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.

Lemma MaxRlist_P2 :
  forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l.

Fixpoint pos_Rl (l:Rlist) (i:nat) : 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)).

Lemma pos_Rl_P2 :
  forall (l:Rlist) (x:R),
    In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i).

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

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) : 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) : Rlist :=
  match l with
    | nil => k
    | cons a l' => cons a (cons_Rlist l' k)
  end.

Fixpoint cons_ORlist (k l:Rlist) : Rlist :=
  match k with
    | nil => l
    | cons a k' => cons_ORlist k' (insert l a)
  end.

Fixpoint app_Rlist (l:Rlist) (f:R -> R) : Rlist :=
  match l with
    | nil => nil
    | cons a l' => cons (f a) (app_Rlist l' f)
  end.

Fixpoint mid_Rlist (l:Rlist) (x:R) : 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.

Lemma RList_P1 :
  forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).

Lemma RList_P2 :
  forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).

Lemma RList_P3 :
  forall (l:Rlist) (x:R),
    In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat).

Lemma RList_P4 :
  forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1.

Lemma RList_P5 :
  forall (l:Rlist) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x.

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

Lemma RList_P7 :
  forall (l:Rlist) (x:R),
    ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)).

Lemma RList_P8 :
  forall (l:Rlist) (a x:R), In x (insert l a) <-> x = a \/ In x l.

Lemma RList_P9 :
  forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2.

Lemma RList_P10 :
  forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l).

Lemma RList_P11 :
  forall l1 l2:Rlist,
    Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat.

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

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.

Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l.

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.

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

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.

Lemma RList_P18 :
  forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l.

Lemma RList_P19 :
  forall l:Rlist,
    l <> nil -> exists r : R, (exists r0 : Rlist, l = cons r r0).

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

Lemma RList_P21 : forall l l':Rlist, l = l' -> Rtail l = Rtail l'.

Lemma RList_P22 :
  forall l1 l2:Rlist, l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0.

Lemma RList_P23 :
  forall l1 l2:Rlist,
    Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.

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

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

Lemma RList_P26 :
  forall (l1 l2:Rlist) (i:nat),
    (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i.

Lemma RList_P27 :
  forall l1 l2 l3:Rlist,
    cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3.

Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l.

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