Library Coq.Reals.RList
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.
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.
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) {
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)).
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) {
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.
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).