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.

intros; induction  l as [| r l Hrecl].

simpl in H; elim H.

induction  l as [| r0 l Hrecl0].

simpl in H; elim H; intro.

simpl in |- *; right; assumption.

elim H0.

replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))).

simpl in H; decompose [or] H.

rewrite H0; apply RmaxLess1.

unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.

apply Hrecl; simpl in |- *; tauto.

apply Rle_trans with (MaxRlist (cons r0 l));

 [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].

unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.

apply Hrecl; simpl in |- *; tauto.

apply Rle_trans with (MaxRlist (cons r0 l));

 [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].

reflexivity.

Qed.




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.

intros; induction  l as [| r l Hrecl].

simpl in H; elim H.

induction  l as [| r0 l Hrecl0].

simpl in H; elim H; intro.

simpl in |- *; right; symmetry  in |- *; assumption.

elim H0.

replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).

simpl in H; decompose [or] H.

rewrite H0; apply Rmin_l.

unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.

apply Rle_trans with (MinRlist (cons r0 l)).

assumption.

apply Hrecl; simpl in |- *; tauto.

apply Hrecl; simpl in |- *; tauto.

apply Rle_trans with (MinRlist (cons r0 l)).

apply Rmin_r.

apply Hrecl; simpl in |- *; tauto.

reflexivity.

Qed.




Lemma AbsList_P1 :

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

intros; induction  l as [| r l Hrecl].

elim H.

simpl in |- *; simpl in H; elim H; intro.

left; rewrite H0; reflexivity.

right; apply Hrecl; assumption.

Qed.




Lemma MinRlist_P2 :

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

intros; induction  l as [| r l Hrecl].

apply Rlt_0_1.

induction  l as [| r0 l Hrecl0].

simpl in |- *; apply H; simpl in |- *; tauto.

replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).

unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.

apply H; simpl in |- *; tauto.

apply Hrecl; intros; apply H; simpl in |- *; simpl in H0; tauto.

reflexivity.

Qed.




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.

intros; induction  l as [| r l Hrecl].

elim H.

elim H; intro.

exists r; split.

simpl in |- *; tauto.

assumption.

assert (H1:= Hrecl H0); elim H1; intros; elim H2; clear H2; intros;

 exists x0; simpl in |- *; simpl in H2; tauto.

Qed.




Lemma MaxRlist_P2 :

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

intros; induction  l as [| r l Hrecl].

simpl in H; elim H; trivial.

induction  l as [| r0 l Hrecl0].

simpl in |- *; left; reflexivity.

change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))) in |- *;

 unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); 

 intro.

right; apply Hrecl; exists r0; left; reflexivity.

left; reflexivity.

Qed.




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

intros; induction  l as [| r l Hrecl];

 [ elim (lt_n_O _ H)

 | simpl in |- *; case (Rlength l); [ reflexivity | intro; reflexivity ] ].

Qed.




Lemma pos_Rl_P2 :

 forall (l:Rlist) (x:R),

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

intros; induction  l as [| r l Hrecl].

split; intro;

 [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ].

split; intro.

elim H; intro.

exists 0%nat; split;

 [ simpl in |- *; apply lt_O_Sn | simpl in |- *; apply H0 ].

elim Hrecl; intros; assert (H3:= H1 H0); elim H3; intros; elim H4; intros;

 exists (S x0); split;

 [ simpl in |- *; apply lt_n_S; assumption | simpl in |- *; assumption ].

elim H; intros; elim H0; intros; elim (zerop x0); intro.

rewrite a in H2; simpl in H2; left; assumption.

right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0).

symmetry  in |- *; apply S_pred with 0%nat; assumption.

exists (pred x0); split;

 [ simpl in H1; apply lt_S_n; rewrite H5; assumption
 | rewrite <- H5 in H2; simpl in H2; assumption ].

Qed.




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

intros; induction  l as [| r l Hrecl].

exists nil; intros; split;

 [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ].

assert (H0 : In r (cons r l)).

simpl in |- *; left; reflexivity.

assert (H1:= H _ H0);

 assert (H2 : forall x:R, In x l ->  exists y : R, P x y).

intros; apply H; simpl in |- *; right; assumption.

assert (H3:= Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);

 intros; elim H5; clear H5; intros; split.

simpl in |- *; rewrite H5; reflexivity.

intros; elim (zerop i); intro.

rewrite a; simpl in |- *; assumption.

assert (H8 : i = S (pred i)).

apply S_pred with 0%nat; assumption.

rewrite H8; simpl in |- *; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;

 assumption.

Qed.




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.

intros; induction  l as [| r l Hrecl];

 [ left; reflexivity

 | simpl in |- *; case (Rle_dec r a); intro;

    [ right; reflexivity | left; reflexivity ] ].

Qed.




Lemma RList_P1 :

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

intros; induction  l as [| r l Hrecl].

simpl in |- *; unfold ordered_Rlist in |- *; intros; simpl in H0;

 elim (lt_n_O _ H0).

simpl in |- *; case (Rle_dec r a); intro.

assert (H1 : ordered_Rlist l).

unfold ordered_Rlist in |- *; unfold ordered_Rlist in H; intros;

 assert (H1 : (S i < pred (Rlength (cons r l)))%nat);

 [ simpl in |- *; replace (Rlength l) with (S (pred (Rlength l)));

    [ apply lt_n_S; assumption
    | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
       intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ]

 | apply (H _ H1) ].

assert (H2:= Hrecl H1); unfold ordered_Rlist in |- *; intros;

 induction  i as [| i Hreci].

simpl in |- *; assert (H3:= RList_P0 l a); elim H3; intro.

rewrite H4; assumption.

induction  l as [| r1 l Hrecl0];

 [ simpl in |- *; assumption
 | rewrite H4; apply (H 0%nat); simpl in |- *; apply lt_O_Sn ].

simpl in |- *; apply H2; simpl in H0; apply lt_S_n;

 replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a));

 [ assumption
 | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
    rewrite <- H3 in H0; elim (lt_n_O _ H0) ].

unfold ordered_Rlist in |- *; intros; induction  i as [| i Hreci];

 [ simpl in |- *; auto with real
 | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)) in |- *; apply H;
    simpl in H0; simpl in |- *; apply (lt_S_n _ _ H0) ].

Qed.




Lemma RList_P2 :

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

simple induction l1;

 [ intros; simpl in |- *; apply H
 | intros; simpl in |- *; apply H; apply RList_P1; assumption ].

Qed.




Lemma RList_P3 :

 forall (l:Rlist) (x:R),

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

intros; split; intro;

 [ induction  l as [| r l Hrecl] | induction  l as [| r l Hrecl] ].

elim H.

elim H; intro;

 [ exists 0%nat; split; [ apply H0 | simpl in |- *; apply lt_O_Sn ]

 | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split;

    [ apply H1 | simpl in |- *; apply lt_n_S; assumption ] ].

elim H; intros; elim H0; intros; elim (lt_n_O _ H2).

simpl in |- *; elim H; intros; elim H0; clear H0; intros;

 induction  x0 as [| x0 Hrecx0];

 [ left; apply H0

 | right; apply Hrecl; exists x0; split;

    [ apply H0 | simpl in H1; apply lt_S_n; assumption ] ].

Qed.




Lemma RList_P4 :

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

intros; unfold ordered_Rlist in |- *; intros; apply (H (S i)); simpl in |- *;

 replace (Rlength l1) with (S (pred (Rlength l1)));

 [ apply lt_n_S; assumption
 | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
    intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ].

Qed.




Lemma RList_P5 :

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

intros; induction  l as [| r l Hrecl];

 [ elim H0

 | simpl in |- *; elim H0; intro;

    [ rewrite H1; right; reflexivity

    | apply Rle_trans with (pos_Rl l 0);

       [ apply (H 0%nat); simpl in |- *; induction  l as [| r0 l Hrecl0];

          [ elim H1 | simpl in |- *; apply lt_O_Sn ]

       | apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ].

Qed.




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

simple induction l; split; intro.

intros; right; reflexivity.

unfold ordered_Rlist in |- *; intros; simpl in H0; elim (lt_n_O _ H0).

intros; induction  i as [| i Hreci];

 [ induction  j as [| j Hrecj];

    [ right; reflexivity

    | simpl in |- *; apply Rle_trans with (pos_Rl r0 0);

       [ apply (H0 0%nat); simpl in |- *; simpl in H2; apply neq_O_lt;

          red in |- *; intro; rewrite <- H3 in H2;

          assert (H4:= lt_S_n _ _ H2); elim (lt_n_O _ H4)

       | elim H; intros; apply H3;

          [ apply RList_P4 with r; assumption
          | apply le_O_n
          | simpl in H2; apply lt_S_n; assumption ] ] ]

 | induction  j as [| j Hrecj];

    [ elim (le_Sn_O _ H1)

    | simpl in |- *; elim H; intros; apply H3;

       [ apply RList_P4 with r; assumption
       | apply le_S_n; assumption
       | simpl in H2; apply lt_S_n; assumption ] ] ].

unfold ordered_Rlist in |- *; intros; apply H0;

 [ apply le_n_Sn | simpl in |- *; simpl in H1; apply lt_n_S; assumption ].

Qed.




Lemma RList_P7 :

 forall (l:Rlist) (x:R),

   ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)).

intros; assert (H1:= RList_P6 l); elim H1; intros H2 _; assert (H3:= H2 H);

 clear H1 H2; assert (H1:= RList_P3 l x); elim H1; 

 clear H1; intros; assert (H4:= H1 H0); elim H4; clear H4; 

 intros; elim H4; clear H4; intros; rewrite H4;

 assert (H6 : Rlength l = S (pred (Rlength l))).

apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;

 rewrite <- H6 in H5; elim (lt_n_O _ H5).

apply H3;

 [ rewrite H6 in H5; apply lt_n_Sm_le; assumption
 | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H7 in H5;
    elim (lt_n_O _ H5) ].

Qed.




Lemma RList_P8 :

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

simple induction l.

intros; split; intro; simpl in H; apply H.

intros; split; intro;

 [ simpl in H0; generalize H0; case (Rle_dec r a); intros;

    [ simpl in H1; elim H1; intro;

       [ right; left; assumption

       | elim (H a x); intros; elim (H3 H2); intro;

          [ left; assumption | right; right; assumption ] ]

    | simpl in H1; decompose [or] H1;

       [ left; assumption
       | right; left; assumption
       | right; right; assumption ] ]

 | simpl in |- *; case (Rle_dec r a); intro;

    [ simpl in H0; decompose [or] H0;

       [ right; elim (H a x); intros; apply H3; left
       | left
       | right; elim (H a x); intros; apply H3; right ]

    | simpl in H0; decompose [or] H0; [ left | right; left | right; right ] ];

    assumption ].

Qed.




Lemma RList_P9 :

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

simple induction l1.

intros; split; intro;

 [ simpl in H; right; assumption

 | simpl in |- *; elim H; intro; [ elim H0 | assumption ] ].

intros; split.

simpl in |- *; intros; elim (H (insert l2 r) x); intros; assert (H3:= H1 H0);

 elim H3; intro;

 [ left; right; assumption

 | elim (RList_P8 l2 r x); intros H5 _; assert (H6:= H5 H4); elim H6; intro;

    [ left; left; assumption | right; assumption ] ].

intro; simpl in |- *; elim (H (insert l2 r) x); intros _ H1; apply H1;

 elim H0; intro;

 [ elim H2; intro;

    [ right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left; assumption
    | left; assumption ]

 | right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption ].

Qed.




Lemma RList_P10 :

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

intros; induction  l as [| r l Hrecl];

 [ reflexivity

 | simpl in |- *; case (Rle_dec r a); intro;

    [ simpl in |- *; rewrite Hrecl; reflexivity | reflexivity ] ].

Qed.




Lemma RList_P11 :

 forall l1 l2:Rlist,

   Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat.

simple induction l1;

 [ intro; reflexivity
 | intros; simpl in |- *; rewrite (H (insert l2 r)); rewrite RList_P10;
    apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; 
    rewrite S_INR; ring ].

Qed.




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

simple induction l;

 [ intros; elim (lt_n_O _ H)

 | intros; induction  i as [| i Hreci];

    [ reflexivity | simpl in |- *; apply H; apply lt_S_n; apply H0 ] ].

Qed.




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.

simple induction l.

intros; simpl in H; elim (lt_n_O _ H).

simple induction r0.

intros; simpl in H0; elim (lt_n_O _ H0).

intros; simpl in H1; induction  i as [| i Hreci].

reflexivity.

change

  (pos_Rl (mid_Rlist (cons r1 r2) r) (S i) =

   (pos_Rl (cons r1 r2) i + pos_Rl (cons r1 r2) (S i)) / 2) 

 in |- *; apply H0; simpl in |- *; apply lt_S_n; assumption.

Qed.




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

simple induction l; intros;

 [ reflexivity | simpl in |- *; rewrite (H r); reflexivity ].

Qed.




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.

intros; apply Rle_antisym.

induction  l1 as [| r l1 Hrecl1];

 [ simpl in |- *; simpl in H1; right; symmetry  in |- *; assumption

 | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros;

    assert

     (H4 :

      In (pos_Rl (cons r l1) 0) (cons r l1) \/ In (pos_Rl (cons r l1) 0) l2);

    [ left; left; reflexivity

    | assert (H5:= H3 H4); apply RList_P5;

       [ apply RList_P2; assumption | assumption ] ] ].

induction  l1 as [| r l1 Hrecl1];

 [ simpl in |- *; simpl in H1; right; assumption

 | assert

    (H2 :

     In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2));

    [ elim

       (RList_P3 (cons_ORlist (cons r l1) l2)

          (pos_Rl (cons_ORlist (cons r l1) l2) 0)); 

       intros; apply H3; exists 0%nat; split;

       [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ]

    | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) 0));

       intros; assert (H5:= H3 H2); elim H5; intro;

       [ apply RList_P5; assumption
       | rewrite H1; apply RList_P5; assumption ] ] ].

Qed.




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

intros; apply Rle_antisym.

induction  l1 as [| r l1 Hrecl1].

simpl in |- *; simpl in H1; right; symmetry  in |- *; assumption. 

assert

 (H2 :

  In

    (pos_Rl (cons_ORlist (cons r l1) l2)

       (pred (Rlength (cons_ORlist (cons r l1) l2))))

    (cons_ORlist (cons r l1) l2));

 [ elim

    (RList_P3 (cons_ORlist (cons r l1) l2)

       (pos_Rl (cons_ORlist (cons r l1) l2)

          (pred (Rlength (cons_ORlist (cons r l1) l2))))); 

    intros; apply H3; exists (pred (Rlength (cons_ORlist (cons r l1) l2)));

    split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ]

 | elim

    (RList_P9 (cons r l1) l2

       (pos_Rl (cons_ORlist (cons r l1) l2)

          (pred (Rlength (cons_ORlist (cons r l1) l2))))); 

    intros; assert (H5:= H3 H2); elim H5; intro;

    [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ].

induction  l1 as [| r l1 Hrecl1].

simpl in |- *; simpl in H1; right; assumption.

elim

 (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));

 intros;

 assert

  (H4 :

   In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1) \/

   In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2);

 [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1)) in |- *;

    elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); 

    intros; apply H5; exists (Rlength l1); split;

    [ reflexivity | simpl in |- *; apply lt_n_Sn ]

 | assert (H5:= H3 H4); apply RList_P7;

    [ apply RList_P2; assumption

    | elim

       (RList_P9 (cons r l1) l2

          (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); 

       intros; apply H7; left;

       elim

        (RList_P3 (cons r l1)

           (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); 

       intros; apply H9; exists (pred (Rlength (cons r l1))); 

       split; [ reflexivity | simpl in |- *; apply lt_n_Sn ] ] ].

Qed.




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.

simple induction l1.

intros; elim H0.

intros; induction  i as [| i Hreci].

simpl in |- *; elim H1; intro;

 [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2)

 | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ].

simpl in |- *; simpl in H2; elim H1; intro.

rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i);

 [ apply Rle_trans with (pos_Rl r0 0);

    [ apply (H0 0%nat); simpl in |- *; simpl in H3; apply neq_O_lt;

       red in |- *; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3)

    | elim (RList_P6 r0); intros; apply H5;

       [ apply RList_P4 with r; assumption

       | apply le_O_n

       | simpl in H3; apply lt_S_n; apply lt_trans with (Rlength r0);

          [ apply H3 | apply lt_n_Sn ] ] ]

 | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H2)) ].

apply H; try assumption;

 [ apply RList_P4 with r; assumption

 | simpl in H3; apply lt_S_n;

    replace (S (pred (Rlength r0))) with (Rlength r0);

    [ apply H3
    | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
       rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ].

Qed.




Lemma RList_P18 :

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

simple induction l; intros;

 [ reflexivity | simpl in |- *; rewrite H; reflexivity ].

Qed.




Lemma RList_P19 :

 forall l:Rlist,

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

intros; induction  l as [| r l Hrecl];

 [ elim H; reflexivity | exists r; exists l; reflexivity ].

Qed.




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

intros; induction  l as [| r l Hrecl];

 [ simpl in H; elim (le_Sn_O _ H)

 | induction  l as [| r0 l Hrecl0];

    [ simpl in H; elim (le_Sn_O _ (le_S_n _ _ H))
    | exists r; exists r0; exists l; reflexivity ] ].

Qed.




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

intros; rewrite H; reflexivity.

Qed.




Lemma RList_P22 :

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

simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ].

Qed.




Lemma RList_P23 :

 forall l1 l2:Rlist,

   Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.

simple induction l1;

 [ intro; reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].

Qed.




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

simple induction l1.

intros; reflexivity.

intros; rewrite <- (H l2 H0); induction  l2 as [| r1 l2 Hrecl2].

elim H0; reflexivity.

do 2 rewrite RList_P23;

 replace (Rlength (cons r r0) + Rlength (cons r1 l2))%nat with

  (S (S (Rlength r0 + Rlength l2)));

 [ replace (Rlength r0 + Rlength (cons r1 l2))%nat with

    (S (Rlength r0 + Rlength l2));

    [ reflexivity
    | simpl in |- *; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
       rewrite S_INR; ring ]

 | simpl in |- *; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR;

    rewrite S_INR; ring ].

Qed.




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

simple induction l1.

intros; simpl in |- *; assumption.

simple induction r0.

intros; simpl in |- *; simpl in H2; unfold ordered_Rlist in |- *; intros;

 simpl in H3.

induction  i as [| i Hreci].

simpl in |- *; assumption.

change (pos_Rl l2 i <= pos_Rl l2 (S i)) in |- *; apply (H1 i); apply lt_S_n;

 replace (S (pred (Rlength l2))) with (Rlength l2);

 [ assumption
 | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
    rewrite <- H4 in H3; elim (lt_n_O _ H3) ].

intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)).

apply H0; try assumption.

apply RList_P4 with r; assumption.

unfold ordered_Rlist in |- *; intros; simpl in H4;

 induction  i as [| i Hreci].

simpl in |- *; apply (H1 0%nat); simpl in |- *; apply lt_O_Sn.

change

  (pos_Rl (cons_Rlist (cons r1 r2) l2) i <=

   pos_Rl (cons_Rlist (cons r1 r2) l2) (S i)) in |- *; 

 apply (H i); simpl in |- *; apply lt_S_n; assumption.

Qed.




Lemma RList_P26 :

 forall (l1 l2:Rlist) (i:nat),

   (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i.

simple induction l1.

intros; elim (lt_n_O _ H).

intros; induction  i as [| i Hreci].

apply RList_P22; discriminate.

apply (H l2 i); simpl in H0; apply lt_S_n; assumption.

Qed.




Lemma RList_P27 :

 forall l1 l2 l3:Rlist,

   cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3.

simple induction l1; intros;

 [ reflexivity | simpl in |- *; rewrite (H l2 l3); reflexivity ].

Qed.




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

simple induction l;

 [ reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].

Qed.




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

simple induction l2.

intros; rewrite RList_P28 in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)).

intros;

 replace (cons_Rlist l1 (cons r r0)) with

  (cons_Rlist (cons_Rlist l1 (cons r nil)) r0).

inversion H0.

rewrite <- minus_n_n; simpl in |- *; rewrite RList_P26.

clear l2 r0 H i H0 H1 H2; induction  l1 as [| r0 l1 Hrecl1].

reflexivity.

simpl in |- *; assumption.

rewrite RList_P23; rewrite plus_comm; simpl in |- *; apply lt_n_Sn.

replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))).

rewrite H3; simpl in |- *;

 replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))).

apply (H (cons_Rlist l1 (cons r nil)) i).

rewrite RList_P23; rewrite plus_comm; simpl in |- *; rewrite <- H3;

 apply le_n_S; assumption.

repeat rewrite RList_P23; simpl in |- *; rewrite RList_P23 in H1;

 rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1));

 simpl in |- *; rewrite plus_comm; apply H1.

rewrite RList_P23; rewrite plus_comm; reflexivity.

change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *;

 apply minus_Sn_m; assumption.

replace (cons r r0) with (cons_Rlist (cons r nil) r0);

 [ symmetry  in |- *; apply RList_P27 | reflexivity ].

Qed.
Index
This page has been generated by coqdoc