Library Coq.Reals.RList
Require Import List.
Require Import Rbase.
Require Import Rfunctions.
Local Open Scope R_scope.
#[deprecated(since="8.12",note="use (list R) instead")]
Notation Rlist := (list R).
#[deprecated(since="8.12",note="use List.length instead")]
Notation Rlength := List.length.
Fixpoint MaxRlist (l:list R) : R :=
match l with
| nil => 0
| a :: l1 =>
match l1 with
| nil => a
| a' :: l2 => Rmax a (MaxRlist l1)
end
end.
Fixpoint MinRlist (l:list R) : R :=
match l with
| nil => 1
| a :: l1 =>
match l1 with
| nil => a
| a' :: l2 => Rmin a (MinRlist l1)
end
end.
Lemma MaxRlist_P1 : forall (l:list R) (x:R), In x l -> x <= MaxRlist l.
Fixpoint AbsList (l:list R) (x:R) : list R :=
match l with
| nil => nil
| a :: l' => (Rabs (a - x) / 2) :: (AbsList l' x)
end.
Lemma MinRlist_P1 : forall (l:list R) (x:R), In x l -> MinRlist l <= x.
Lemma AbsList_P1 :
forall (l:list R) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x).
Lemma MinRlist_P2 :
forall l:list R, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l.
Lemma AbsList_P2 :
forall (l:list R) (x y:R),
In y (AbsList l x) -> exists z : R, In z l /\ y = Rabs (z - x) / 2.
Lemma MaxRlist_P2 :
forall l:list R, (exists y : R, In y l) -> In (MaxRlist l) l.
Fixpoint pos_Rl (l:list R) (i:nat) : R :=
match l with
| nil => 0
| a :: l' => match i with
| O => a
| S i' => pos_Rl l' i'
end
end.
Lemma pos_Rl_P1 :
forall (l:list R) (a:R),
(0 < length l)%nat ->
pos_Rl (a :: l) (length l) = pos_Rl l (pred (length l)).
Lemma pos_Rl_P2 :
forall (l:list R) (x:R),
In x l <-> (exists i : nat, (i < length l)%nat /\ x = pos_Rl l i).
Lemma Rlist_P1 :
forall (l:list R) (P:R -> R -> Prop),
(forall x:R, In x l -> exists y : R, P x y) ->
exists l' : list R,
length l = length l' /\
(forall i:nat, (i < length l)%nat -> P (pos_Rl l i) (pos_Rl l' i)).
Definition ordered_Rlist (l:list R) : Prop :=
forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <= pos_Rl l (S i).
Fixpoint insert (l:list R) (x:R) : list R :=
match l with
| nil => x :: nil
| a :: l' =>
match Rle_dec a x with
| left _ => a :: (insert l' x)
| right _ => x :: l
end
end.
Fixpoint cons_ORlist (k l:list R) : list R :=
match k with
| nil => l
| a :: k' => cons_ORlist k' (insert l a)
end.
Fixpoint mid_Rlist (l:list R) (x:R) : list R :=
match l with
| nil => nil
| a :: l' => ((x + a) / 2) :: (mid_Rlist l' a)
end.
Definition Rtail (l:list R) : list R :=
match l with
| nil => nil
| a :: l' => l'
end.
Definition FF (l:list R) (f:R -> R) : list R :=
match l with
| nil => nil
| a :: l' => map f (mid_Rlist l' a)
end.
Lemma RList_P0 :
forall (l:list R) (a:R),
pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0.
Lemma RList_P1 :
forall (l:list R) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).
Lemma RList_P2 :
forall l1 l2:list R, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).
Lemma RList_P3 :
forall (l:list R) (x:R),
In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < length l)%nat).
Lemma RList_P4 :
forall (l1:list R) (a:R), ordered_Rlist (a :: l1) -> ordered_Rlist l1.
Lemma RList_P5 :
forall (l:list R) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x.
Lemma RList_P6 :
forall l:list R,
ordered_Rlist l <->
(forall i j:nat,
(i <= j)%nat -> (j < length l)%nat -> pos_Rl l i <= pos_Rl l j).
Lemma RList_P7 :
forall (l:list R) (x:R),
ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (length l)).
Lemma RList_P8 :
forall (l:list R) (a x:R), In x (insert l a) <-> x = a \/ In x l.
Lemma RList_P9 :
forall (l1 l2:list R) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2.
Lemma RList_P10 :
forall (l:list R) (a:R), length (insert l a) = S (length l).
Lemma RList_P11 :
forall l1 l2:list R,
length (cons_ORlist l1 l2) = (length l1 + length l2)%nat.
Lemma RList_P12 :
forall (l:list R) (i:nat) (f:R -> R),
(i < length l)%nat -> pos_Rl (map f l) i = f (pos_Rl l i).
Lemma RList_P13 :
forall (l:list R) (i:nat) (a:R),
(i < pred (length 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:list R) (a:R), length (mid_Rlist l a) = length l.
Lemma RList_P15 :
forall l1 l2:list R,
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:list R,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 (pred (length l1)) = pos_Rl l2 (pred (length l2)) ->
pos_Rl (cons_ORlist l1 l2) (pred (length (cons_ORlist l1 l2))) =
pos_Rl l1 (pred (length l1)).
Lemma RList_P17 :
forall (l1:list R) (x:R) (i:nat),
ordered_Rlist l1 ->
In x l1 ->
pos_Rl l1 i < x -> (i < pred (length l1))%nat -> pos_Rl l1 (S i) <= x.
Lemma RList_P18 :
forall (l:list R) (f:R -> R), length (map f l) = length l.
Lemma RList_P19 :
forall l:list R,
l <> nil -> exists r : R, (exists r0 : list R, l = r :: r0).
Lemma RList_P20 :
forall l:list R,
(2 <= length l)%nat ->
exists r : R,
(exists r1 : R, (exists l' : list R, l = r :: r1 :: l')).
Lemma RList_P21 : forall l l':list R, l = l' -> Rtail l = Rtail l'.
Lemma RList_P22 :
forall l1 l2:list R, l1 <> nil -> pos_Rl (app l1 l2) 0 = pos_Rl l1 0.
Lemma RList_P24 :
forall l1 l2:list R,
l2 <> nil ->
pos_Rl (app l1 l2) (pred (length (app l1 l2))) =
pos_Rl l2 (pred (length l2)).
Lemma RList_P25 :
forall l1 l2:list R,
ordered_Rlist l1 ->
ordered_Rlist l2 ->
pos_Rl l1 (pred (length l1)) <= pos_Rl l2 0 ->
ordered_Rlist (app l1 l2).
Lemma RList_P26 :
forall (l1 l2:list R) (i:nat),
(i < length l1)%nat -> pos_Rl (app l1 l2) i = pos_Rl l1 i.
Lemma RList_P29 :
forall (l2 l1:list R) (i:nat),
(length l1 <= i)%nat ->
(i < length (app l1 l2))%nat ->
pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1).
#[deprecated(since="8.12",note="use List.cons instead")]
Notation cons := List.cons.
#[deprecated(since="8.12",note="use List.nil instead")]
Notation nil := List.nil.