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