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.