From ffb64d16132dd80f72ecb619ef87e3eee1fa8bda Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:37 +0000 Subject: Kills the useless tactic annotations "in |- *" Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/QArith/Qcanon.v | 2 +- theories/QArith/Qreals.v | 60 ++++++++++++++++++++++++------------------------ 2 files changed, 31 insertions(+), 31 deletions(-) (limited to 'theories/QArith') diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 05a27cc43..c20c3ba7f 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -488,7 +488,7 @@ Definition Qc_eq_bool (x y : Qc) := Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y. Proof. - intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. + intros x y; unfold Qc_eq_bool; case (Qc_eq_dec x y); simpl; auto. intros _ H; inversion H. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 24f6d7204..3730bcd7f 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -21,7 +21,7 @@ Hint Resolve IZR_nz Rmult_integral_contrapositive. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. Proof. -unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply eq_IZR. do 2 rewrite mult_IZR. @@ -36,24 +36,24 @@ Qed. Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y. Proof. -unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert ((X1 * Y2)%R = (Y1 * X2)%R). - unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. apply IZR_eq; auto. clear H. field_simplify_eq; auto. ring_simplify X1 Y2 (Y2 * X1)%R. -rewrite H0 in |- *; ring. +rewrite H0; ring. Qed. Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y. Proof. -unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply le_IZR. do 2 rewrite mult_IZR. @@ -65,37 +65,37 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_le; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_le; auto with zarith. Qed. Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R. Proof. -unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert (X1 * Y2 <= Y1 * X2)%R. - unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. apply IZR_le; auto. clear H. replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. Qed. Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x (Q2R x < Q2R y)%R. Proof. -unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert (X1 * Y2 < Y1 * X2)%R. - unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. apply IZR_lt; auto. clear H. replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat; apply Rinv_0_lt_compat. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. Qed. Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R. Proof. -unfold Qplus, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); - unfold Qden, Qnum in |- *. +unfold Qplus, Qeq, Q2R; intros (x1, x2) (y1, y2); + unfold Qden, Qnum. simpl_mult. rewrite plus_IZR. do 3 rewrite mult_IZR. @@ -147,8 +147,8 @@ Qed. Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R. Proof. -unfold Qmult, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); - unfold Qden, Qnum in |- *. +unfold Qmult, Qeq, Q2R; intros (x1, x2) (y1, y2); + unfold Qden, Qnum. simpl_mult. do 2 rewrite mult_IZR. field; auto. @@ -156,24 +156,24 @@ Qed. Lemma Q2R_opp : forall x : Q, Q2R (- x) = (- Q2R x)%R. Proof. -unfold Qopp, Qeq, Q2R in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. +unfold Qopp, Qeq, Q2R; intros (x1, x2); unfold Qden, Qnum. rewrite Ropp_Ropp_IZR. field; auto. Qed. Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R. -unfold Qminus in |- *; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. +unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. Qed. Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R. Proof. -unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. +unfold Qinv, Q2R, Qeq; intros (x1, x2); unfold Qden, Qnum. case x1. -simpl in |- *; intros; elim H; trivial. +simpl; intros; elim H; trivial. intros; field; auto. intros; - change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *; - change (IZR (Zneg p)) with (- IZR (' p))%R in |- *; + change (IZR (Zneg x2)) with (- IZR (' x2))%R; + change (IZR (Zneg p)) with (- IZR (' p))%R; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. @@ -181,7 +181,7 @@ Qed. Lemma Q2R_div : forall x y : Q, ~ y==0 -> Q2R (x/y) = (Q2R x / Q2R y)%R. Proof. -unfold Qdiv, Rdiv in |- *. +unfold Qdiv, Rdiv. intros; rewrite Q2R_mult. rewrite Q2R_inv; auto. Qed. @@ -205,7 +205,7 @@ Qed. Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x. intros; QField. intro; apply H; apply eqR_Qeq. -rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real. +rewrite H0; unfold Q2R; simpl; field; auto with real. Qed. End LegacyQField. -- cgit v1.2.3