diff options
Diffstat (limited to 'theories/Reals/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 620561dc..c817bdfa 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.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 *) @@ -12,12 +12,12 @@ Require Import Even. Require Import Div2. Require Import ArithRing. -Open Local Scope Z_scope. -Open Local Scope R_scope. +Local Open Scope Z_scope. +Local Open Scope R_scope. Lemma minus_neq_O : forall n i:nat, (i < n)%nat -> (n - i)%nat <> 0%nat. Proof. - intros; red in |- *; intro. + intros; red; intro. cut (forall n m:nat, (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m). intro; assert (H2 := H1 _ _ (lt_le_weak _ _ H) H0); rewrite H2 in H; elim (lt_irrefl _ H). @@ -27,11 +27,11 @@ Proof. forall n0 m:nat, (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m). intro; apply H1. apply nat_double_ind. - unfold R in |- *; intros; inversion H2; reflexivity. - unfold R in |- *; intros; simpl in H3; assumption. - unfold R in |- *; intros; simpl in H4; assert (H5 := le_S_n _ _ H3); + unfold R; intros; inversion H2; reflexivity. + unfold R; intros; simpl in H3; assumption. + unfold R; intros; simpl in H4; assert (H5 := le_S_n _ _ H3); assert (H6 := H2 H5 H4); rewrite H6; reflexivity. - unfold R in |- *; intros; apply H1; assumption. + unfold R; intros; apply H1; assumption. Qed. Lemma le_minusni_n : forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat. @@ -41,20 +41,20 @@ Proof. ((forall m n:nat, R m n) -> forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat). intro; apply H. apply nat_double_ind. - unfold R in |- *; intros; simpl in |- *; apply le_n. - unfold R in |- *; intros; simpl in |- *; apply le_n. - unfold R in |- *; intros; simpl in |- *; apply le_trans with n. + unfold R; intros; simpl; apply le_n. + unfold R; intros; simpl; apply le_n. + unfold R; intros; simpl; apply le_trans with n. apply H0; apply le_S_n; assumption. apply le_n_Sn. - unfold R in |- *; intros; apply H; assumption. + unfold R; intros; apply H; assumption. Qed. Lemma lt_minus_O_lt : forall m n:nat, (m < n)%nat -> (0 < n - m)%nat. Proof. - intros n m; pattern n, m in |- *; apply nat_double_ind; + intros n m; pattern n, m; apply nat_double_ind; [ intros; rewrite <- minus_n_O; assumption | intros; elim (lt_n_O _ H) - | intros; simpl in |- *; apply H; apply lt_S_n; assumption ]. + | intros; simpl; apply H; apply lt_S_n; assumption ]. Qed. Lemma even_odd_cor : @@ -73,7 +73,7 @@ Proof. apply H3; assumption. right. apply H4; assumption. - unfold double in |- *;ring. + unfold double;ring. Qed. (* 2m <= 2n => m<=n *) @@ -105,9 +105,9 @@ Proof. exists (x - IZR k0 * y). split. ring. - unfold k0 in |- *; case (Rcase_abs y); intro. - assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl in |- *; - unfold Rminus in |- *. + unfold k0; case (Rcase_abs y); intro. + assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; + unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. split. @@ -118,7 +118,7 @@ Proof. rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ]. apply Rplus_le_reg_l with (IZR (up (x / - y)) - x / - y). - rewrite Rplus_0_r; unfold Rdiv in |- *; pattern (/ - y) at 4 in |- *; + rewrite Rplus_0_r; unfold Rdiv; pattern (/ - y) at 4; rewrite <- Ropp_inv_permute; [ idtac | assumption ]. replace (IZR (up (x * / - y)) - x * - / y + @@ -138,11 +138,11 @@ Proof. replace (IZR (up (x / - y)) - 1 + (- (x * / y) + - (IZR (up (x / - y)) - 1))) with (- (x * / y)); [ idtac | ring ]. rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0; - unfold Rdiv in |- *; intros H1 _; exact H1. + unfold Rdiv; intros H1 _; exact H1. apply Ropp_neq_0_compat; assumption. - assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl in |- *; + assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl; cut (0 < y). - intro; unfold Rminus in |- *; + intro; unfold Rminus; replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y); [ idtac | ring ]. split. @@ -152,7 +152,7 @@ Proof. rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ]; apply Rplus_le_reg_l with (IZR (up (x / y)) - x / y); - rewrite Rplus_0_r; unfold Rdiv in |- *; + rewrite Rplus_0_r; unfold Rdiv; replace (IZR (up (x * / y)) - x * / y + (x * / y + (1 - IZR (up (x * / y))))) with 1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2; @@ -166,12 +166,12 @@ Proof. replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y))); [ idtac | ring ]; replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with - (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv in |- *; + (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv; intros H2 _; exact H2. case (total_order_T 0 y); intro. elim s; intro. assumption. - elim H; symmetry in |- *; exact b. + elim H; symmetry ; exact b. assert (H1 := Rge_le _ _ r); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r0)). Qed. |