diff options
Diffstat (limited to 'theories/Reals/RList.v')
| -rw-r--r-- | theories/Reals/RList.v | 232 |
1 files changed, 116 insertions, 116 deletions
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index dbd2e52f..6d42434a 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -8,7 +8,7 @@ Require Import Rbase. Require Import Rfunctions. -Open Local Scope R_scope. +Local Open Scope R_scope. Inductive Rlist : Type := | nil : Rlist @@ -52,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. @@ -80,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. @@ -101,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. @@ -112,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. @@ -128,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 : @@ -140,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. @@ -164,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 : @@ -177,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 ]. @@ -201,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. @@ -271,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. @@ -279,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 : @@ -324,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; @@ -338,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. @@ -350,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. @@ -366,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 @@ -380,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 : @@ -397,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. @@ -420,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 @@ -435,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 @@ -455,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 : @@ -465,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. @@ -477,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 : @@ -494,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 : @@ -511,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 : @@ -520,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)); @@ -528,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 @@ -545,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 @@ -557,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) @@ -565,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; @@ -573,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 @@ -587,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 : @@ -599,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 @@ -618,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. @@ -626,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 : @@ -666,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 : @@ -685,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. @@ -699,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 : @@ -738,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 : @@ -759,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. |