summaryrefslogtreecommitdiff
path: root/theories/Reals/RList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/RList.v')
-rw-r--r--theories/Reals/RList.v234
1 files changed, 116 insertions, 118 deletions
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 4e4fb378..6d42434a 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -1,16 +1,14 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RList.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
Inductive Rlist : Type :=
| nil : Rlist
@@ -54,19 +52,19 @@ Proof.
simpl in H; elim H.
induction l as [| r0 l Hrecl0].
simpl in H; elim H; intro.
- simpl in |- *; right; assumption.
+ simpl; 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.
+ unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
+ apply Hrecl; simpl; 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 Hrecl; simpl; tauto | left; auto with real ].
+ unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
+ apply Hrecl; simpl; tauto.
apply Rle_trans with (MaxRlist (cons r0 l));
- [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
+ [ apply Hrecl; simpl; tauto | left; auto with real ].
reflexivity.
Qed.
@@ -82,19 +80,19 @@ Proof.
simpl in H; elim H.
induction l as [| r0 l Hrecl0].
simpl in H; elim H; intro.
- simpl in |- *; right; symmetry in |- *; assumption.
+ simpl; right; symmetry ; 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.
+ unfold Rmin; 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 Hrecl; simpl; tauto.
+ apply Hrecl; simpl; tauto.
apply Rle_trans with (MinRlist (cons r0 l)).
apply Rmin_r.
- apply Hrecl; simpl in |- *; tauto.
+ apply Hrecl; simpl; tauto.
reflexivity.
Qed.
@@ -103,7 +101,7 @@ Lemma AbsList_P1 :
Proof.
intros; induction l as [| r l Hrecl].
elim H.
- simpl in |- *; simpl in H; elim H; intro.
+ simpl; simpl in H; elim H; intro.
left; rewrite H0; reflexivity.
right; apply Hrecl; assumption.
Qed.
@@ -114,11 +112,11 @@ Proof.
intros; induction l as [| r l Hrecl].
apply Rlt_0_1.
induction l as [| r0 l Hrecl0].
- simpl in |- *; apply H; simpl in |- *; tauto.
+ simpl; apply H; simpl; 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.
+ unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro.
+ apply H; simpl; tauto.
+ apply Hrecl; intros; apply H; simpl; simpl in H0; tauto.
reflexivity.
Qed.
@@ -130,10 +128,10 @@ Proof.
elim H.
elim H; intro.
exists r; split.
- simpl in |- *; tauto.
+ simpl; tauto.
assumption.
assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros;
- exists x0; simpl in |- *; simpl in H2; tauto.
+ exists x0; simpl; simpl in H2; tauto.
Qed.
Lemma MaxRlist_P2 :
@@ -142,9 +140,9 @@ Proof.
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)));
+ simpl; left; reflexivity.
+ change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l)));
+ unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l)));
intro.
right; apply Hrecl; exists r0; left; reflexivity.
left; reflexivity.
@@ -166,7 +164,7 @@ Lemma pos_Rl_P1 :
Proof.
intros; induction l as [| r l Hrecl];
[ elim (lt_n_O _ H)
- | simpl in |- *; case (Rlength l); [ reflexivity | intro; reflexivity ] ].
+ | simpl; case (Rlength l); [ reflexivity | intro; reflexivity ] ].
Qed.
Lemma pos_Rl_P2 :
@@ -179,14 +177,14 @@ Proof.
split; intro.
elim H; intro.
exists 0%nat; split;
- [ simpl in |- *; apply lt_O_Sn | simpl in |- *; apply H0 ].
+ [ simpl; apply lt_O_Sn | simpl; 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 ].
+ [ simpl; apply lt_n_S; assumption | simpl; 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.
+ symmetry ; 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 ].
@@ -203,18 +201,18 @@ Proof.
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.
+ simpl; 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.
+ intros; apply H; simpl; 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.
+ simpl; rewrite H5; reflexivity.
intros; elim (zerop i); intro.
- rewrite a; simpl in |- *; assumption.
+ rewrite a; simpl; 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;
+ rewrite H8; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;
assumption.
Qed.
@@ -273,7 +271,7 @@ Lemma RList_P0 :
Proof.
intros; induction l as [| r l Hrecl];
[ left; reflexivity
- | simpl in |- *; case (Rle_dec r a); intro;
+ | simpl; case (Rle_dec r a); intro;
[ right; reflexivity | left; reflexivity ] ].
Qed.
@@ -281,41 +279,41 @@ Lemma RList_P1 :
forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).
Proof.
intros; induction l as [| r l Hrecl].
- simpl in |- *; unfold ordered_Rlist in |- *; intros; simpl in H0;
+ simpl; unfold ordered_Rlist; intros; simpl in H0;
elim (lt_n_O _ H0).
- simpl in |- *; case (Rle_dec r a); intro.
+ simpl; case (Rle_dec r a); intro.
assert (H1 : ordered_Rlist l).
- unfold ordered_Rlist in |- *; unfold ordered_Rlist in H; intros;
+ unfold ordered_Rlist; 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)));
+ [ simpl; 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 |- *;
+ | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
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;
+ assert (H2 := Hrecl H1); unfold ordered_Rlist; intros;
induction i as [| i Hreci].
- simpl in |- *; assert (H3 := RList_P0 l a); elim H3; intro.
+ simpl; 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;
+ [ simpl; assumption
+ | rewrite H4; apply (H 0%nat); simpl; apply lt_O_Sn ].
+ simpl; 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;
+ | apply S_pred with 0%nat; apply neq_O_lt; red; 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) ].
+ unfold ordered_Rlist; intros; induction i as [| i Hreci];
+ [ simpl; auto with real
+ | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)); apply H;
+ simpl in H0; simpl; apply (lt_S_n _ _ H0) ].
Qed.
Lemma RList_P2 :
forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).
Proof.
simple induction l1;
- [ intros; simpl in |- *; apply H
- | intros; simpl in |- *; apply H; apply RList_P1; assumption ].
+ [ intros; simpl; apply H
+ | intros; simpl; apply H; apply RList_P1; assumption ].
Qed.
Lemma RList_P3 :
@@ -326,11 +324,11 @@ Proof.
[ 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 ]
+ [ exists 0%nat; split; [ apply H0 | simpl; 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 ] ].
+ [ apply H1 | simpl; 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;
+ simpl; elim H; intros; elim H0; clear H0; intros;
induction x0 as [| x0 Hrecx0];
[ left; apply H0
| right; apply Hrecl; exists x0; split;
@@ -340,10 +338,10 @@ Qed.
Lemma RList_P4 :
forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1.
Proof.
- intros; unfold ordered_Rlist in |- *; intros; apply (H (S i)); simpl in |- *;
+ intros; unfold ordered_Rlist; intros; apply (H (S i)); simpl;
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 |- *;
+ | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ].
Qed.
@@ -352,11 +350,11 @@ Lemma RList_P5 :
Proof.
intros; induction l as [| r l Hrecl];
[ elim H0
- | simpl in |- *; elim H0; intro;
+ | simpl; 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 (H 0%nat); simpl; induction l as [| r0 l Hrecl0];
+ [ elim H1 | simpl; apply lt_O_Sn ]
| apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ].
Qed.
@@ -368,13 +366,13 @@ Lemma RList_P6 :
Proof.
simple induction l; split; intro.
intros; right; reflexivity.
- unfold ordered_Rlist in |- *; intros; simpl in H0; elim (lt_n_O _ H0).
+ unfold ordered_Rlist; 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;
+ | simpl; apply Rle_trans with (pos_Rl r0 0);
+ [ apply (H0 0%nat); simpl; simpl in H2; apply neq_O_lt;
+ red; 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
@@ -382,12 +380,12 @@ Proof.
| 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;
+ | simpl; 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 ].
+ unfold ordered_Rlist; intros; apply H0;
+ [ apply le_n_Sn | simpl; simpl in H1; apply lt_n_S; assumption ].
Qed.
Lemma RList_P7 :
@@ -399,11 +397,11 @@ Proof.
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;
+ apply S_pred with 0%nat; apply neq_O_lt; red; 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;
+ | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H7 in H5;
elim (lt_n_O _ H5) ].
Qed.
@@ -422,7 +420,7 @@ Proof.
[ left; assumption
| right; left; assumption
| right; right; assumption ] ]
- | simpl in |- *; case (Rle_dec r a); intro;
+ | simpl; case (Rle_dec r a); intro;
[ simpl in H0; decompose [or] H0;
[ right; elim (H a x); intros; apply H3; left
| left
@@ -437,14 +435,14 @@ Proof.
simple induction l1.
intros; split; intro;
[ simpl in H; right; assumption
- | simpl in |- *; elim H; intro; [ elim H0 | assumption ] ].
+ | simpl; elim H; intro; [ elim H0 | assumption ] ].
intros; split.
- simpl in |- *; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0);
+ simpl; 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;
+ intro; simpl; 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
@@ -457,8 +455,8 @@ Lemma RList_P10 :
Proof.
intros; induction l as [| r l Hrecl];
[ reflexivity
- | simpl in |- *; case (Rle_dec r a); intro;
- [ simpl in |- *; rewrite Hrecl; reflexivity | reflexivity ] ].
+ | simpl; case (Rle_dec r a); intro;
+ [ simpl; rewrite Hrecl; reflexivity | reflexivity ] ].
Qed.
Lemma RList_P11 :
@@ -467,7 +465,7 @@ Lemma RList_P11 :
Proof.
simple induction l1;
[ intro; reflexivity
- | intros; simpl in |- *; rewrite (H (insert l2 r)); rewrite RList_P10;
+ | intros; simpl; rewrite (H (insert l2 r)); rewrite RList_P10;
apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
rewrite S_INR; ring ].
Qed.
@@ -479,7 +477,7 @@ Proof.
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 ] ].
+ [ reflexivity | simpl; apply H; apply lt_S_n; apply H0 ] ].
Qed.
Lemma RList_P13 :
@@ -496,13 +494,13 @@ Proof.
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.
+ ; apply H0; simpl; apply lt_S_n; assumption.
Qed.
Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l.
Proof.
simple induction l; intros;
- [ reflexivity | simpl in |- *; rewrite (H r); reflexivity ].
+ [ reflexivity | simpl; rewrite (H r); reflexivity ].
Qed.
Lemma RList_P15 :
@@ -513,7 +511,7 @@ Lemma RList_P15 :
Proof.
intros; apply Rle_antisym.
induction l1 as [| r l1 Hrecl1];
- [ simpl in |- *; simpl in H1; right; symmetry in |- *; assumption
+ [ simpl; simpl in H1; right; symmetry ; assumption
| elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros;
assert
(H4 :
@@ -522,7 +520,7 @@ Proof.
| 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
+ [ simpl; simpl in H1; right; assumption
| assert
(H2 :
In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2));
@@ -530,7 +528,7 @@ Proof.
(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 ]
+ [ reflexivity | rewrite RList_P11; simpl; 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
@@ -547,7 +545,7 @@ Lemma RList_P16 :
Proof.
intros; apply Rle_antisym.
induction l1 as [| r l1 Hrecl1].
- simpl in |- *; simpl in H1; right; symmetry in |- *; assumption.
+ simpl; simpl in H1; right; symmetry ; assumption.
assert
(H2 :
In
@@ -559,7 +557,7 @@ Proof.
(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 ]
+ split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]
| elim
(RList_P9 (cons r l1) l2
(pos_Rl (cons_ORlist (cons r l1) l2)
@@ -567,7 +565,7 @@ Proof.
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.
+ simpl; simpl in H1; right; assumption.
elim
(RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));
intros;
@@ -575,10 +573,10 @@ Proof.
(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 |- *;
+ [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1));
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 ]
+ [ reflexivity | simpl; apply lt_n_Sn ]
| assert (H5 := H3 H4); apply RList_P7;
[ apply RList_P2; assumption
| elim
@@ -589,7 +587,7 @@ Proof.
(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 ] ] ].
+ split; [ reflexivity | simpl; apply lt_n_Sn ] ] ].
Qed.
Lemma RList_P17 :
@@ -601,14 +599,14 @@ Proof.
simple induction l1.
intros; elim H0.
intros; induction i as [| i Hreci].
- simpl in |- *; elim H1; intro;
+ simpl; 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.
+ simpl; 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)
+ [ apply (H0 0%nat); simpl; simpl in H3; apply neq_O_lt;
+ red; 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
@@ -620,7 +618,7 @@ Proof.
| 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;
+ | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ].
Qed.
@@ -628,7 +626,7 @@ Lemma RList_P18 :
forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l.
Proof.
simple induction l; intros;
- [ reflexivity | simpl in |- *; rewrite H; reflexivity ].
+ [ reflexivity | simpl; rewrite H; reflexivity ].
Qed.
Lemma RList_P19 :
@@ -668,7 +666,7 @@ Lemma RList_P23 :
Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.
Proof.
simple induction l1;
- [ intro; reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].
+ [ intro; reflexivity | intros; simpl; rewrite H; reflexivity ].
Qed.
Lemma RList_P24 :
@@ -687,9 +685,9 @@ Proof.
[ 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;
+ | simpl; 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;
+ | simpl; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR;
rewrite S_INR; ring ].
Qed.
@@ -701,27 +699,27 @@ Lemma RList_P25 :
ordered_Rlist (cons_Rlist l1 l2).
Proof.
simple induction l1.
- intros; simpl in |- *; assumption.
+ intros; simpl; assumption.
simple induction r0.
- intros; simpl in |- *; simpl in H2; unfold ordered_Rlist in |- *; intros;
+ intros; simpl; simpl in H2; unfold ordered_Rlist; 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;
+ simpl; assumption.
+ change (pos_Rl l2 i <= pos_Rl l2 (S i)); 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;
+ | apply S_pred with 0%nat; apply neq_O_lt; red; 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;
+ unfold ordered_Rlist; intros; simpl in H4;
induction i as [| i Hreci].
- simpl in |- *; apply (H1 0%nat); simpl in |- *; apply lt_O_Sn.
+ simpl; apply (H1 0%nat); simpl; 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.
+ pos_Rl (cons_Rlist (cons r1 r2) l2) (S i));
+ apply (H i); simpl; apply lt_S_n; assumption.
Qed.
Lemma RList_P26 :
@@ -740,13 +738,13 @@ Lemma RList_P27 :
cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3.
Proof.
simple induction l1; intros;
- [ reflexivity | simpl in |- *; rewrite (H l2 l3); reflexivity ].
+ [ reflexivity | simpl; rewrite (H l2 l3); reflexivity ].
Qed.
Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l.
Proof.
simple induction l;
- [ reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].
+ [ reflexivity | intros; simpl; rewrite H; reflexivity ].
Qed.
Lemma RList_P29 :
@@ -761,23 +759,23 @@ Proof.
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.
+ rewrite <- minus_n_n; simpl; 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.
+ simpl; assumption.
+ rewrite RList_P23; rewrite plus_comm; simpl; apply lt_n_Sn.
replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))).
- rewrite H3; simpl in |- *;
+ rewrite H3; simpl;
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;
+ rewrite RList_P23; rewrite plus_comm; simpl; rewrite <- H3;
apply le_n_S; assumption.
- repeat rewrite RList_P23; simpl in |- *; rewrite RList_P23 in H1;
+ repeat rewrite RList_P23; simpl; 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.
+ simpl; rewrite plus_comm; apply H1.
rewrite RList_P23; rewrite plus_comm; reflexivity.
- change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *;
+ change (S (m - Rlength l1) = (S m - Rlength l1)%nat);
apply minus_Sn_m; assumption.
replace (cons r r0) with (cons_Rlist (cons r nil) r0);
- [ symmetry in |- *; apply RList_P27 | reflexivity ].
+ [ symmetry ; apply RList_P27 | reflexivity ].
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 04:06:11 +0000