diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 10:26:26 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 11:33:55 +0200 |
commit | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch) | |
tree | f8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/Reals/Sqrt_reg.v | |
parent | be01deca2b8ff22505adaa66f55f005673bf2d85 (diff) |
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Diffstat (limited to 'theories/Reals/Sqrt_reg.v')
-rw-r--r-- | theories/Reals/Sqrt_reg.v | 39 |
1 files changed, 18 insertions, 21 deletions
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 985faa21e..87c624182 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -18,8 +18,7 @@ Lemma sqrt_var_maj : Proof. intros; cut (0 <= 1 + h). intro; apply Rle_trans with (Rabs (sqrt (Rsqr (1 + h)) - 1)). - case (total_order_T h 0); intro. - elim s; intro. + destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. repeat rewrite Rabs_left. unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)). do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive; @@ -51,7 +50,7 @@ Proof. left; apply Rlt_0_1. pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. - rewrite b; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right; + rewrite Heq; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right; reflexivity. repeat rewrite Rabs_right. unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)); @@ -86,16 +85,15 @@ Proof. rewrite sqrt_Rsqr. replace (1 + h - 1) with h; [ right; reflexivity | ring ]. apply H0. - case (total_order_T h 0); intro. - elim s; intro. - rewrite (Rabs_left h a) in H. + destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. + rewrite (Rabs_left h Hlt) in H. apply Rplus_le_reg_l with (- h). rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; exact H. - left; rewrite b; rewrite Rplus_0_r; apply Rlt_0_1. + left; rewrite Heq; rewrite Rplus_0_r; apply Rlt_0_1. left; apply Rplus_lt_0_compat. apply Rlt_0_1. - apply r. + apply Hgt. Qed. (** sqrt is continuous in 1 *) @@ -203,8 +201,8 @@ Proof. left; apply Rlt_0_1. left; apply H. elim H6; intros. - case (Rcase_abs (x0 - x)); intro. - rewrite (Rabs_left (x0 - x) r) in H8. + destruct (Rcase_abs (x0 - x)) as [Hlt|Hgt]. + rewrite (Rabs_left (x0 - x) Hlt) in H8. rewrite Rplus_comm. apply Rplus_le_reg_l with (- ((x0 - x) / x)). rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; @@ -220,7 +218,7 @@ Proof. apply Rplus_le_le_0_compat. left; apply Rlt_0_1. unfold Rdiv; apply Rmult_le_pos. - apply Rge_le; exact r. + apply Rge_le; exact Hgt. left; apply Rinv_0_lt_compat; apply H. unfold Rdiv; apply Rmult_lt_0_compat. apply H1. @@ -273,8 +271,8 @@ Proof. apply Rplus_lt_le_0_compat. apply sqrt_lt_R0; apply H. apply sqrt_positivity; apply H10. - case (Rcase_abs h); intro. - rewrite (Rabs_left h r) in H9. + destruct (Rcase_abs h) as [Hlt|Hgt]. + rewrite (Rabs_left h Hlt) in H9. apply Rplus_le_reg_l with (- h). rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; left; apply Rlt_le_trans with alpha1. @@ -282,7 +280,7 @@ Proof. unfold alpha1; apply Rmin_r. apply Rplus_le_le_0_compat. left; assumption. - apply Rge_le; apply r. + apply Rge_le; apply Hgt. unfold alpha1; unfold Rmin; case (Rle_dec alpha x); intro. apply H5. apply H. @@ -341,17 +339,16 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - case (Rcase_abs x0); intro. - unfold sqrt; case (Rcase_abs x0); intro. + destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. - assert (H6 := Rge_le _ _ r0); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 r)). rewrite Rabs_right. apply Rsqr_incrst_0. rewrite Rsqr_sqrt. - rewrite (Rabs_right x0 r) in H5; apply H5. - apply Rge_le; exact r. - apply sqrt_positivity; apply Rge_le; exact r. + rewrite (Rabs_right x0 Hgt) in H5; apply H5. + apply Rge_le; exact Hgt. + apply sqrt_positivity; apply Rge_le; exact Hgt. left; exact H2. - apply Rle_ge; apply sqrt_positivity; apply Rge_le; exact r. + apply Rle_ge; apply sqrt_positivity; apply Rge_le; exact Hgt. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H1 H)). Qed. |