diff options
Diffstat (limited to 'theories/QArith/Qreduction.v')
| -rw-r--r-- | theories/QArith/Qreduction.v | 52 |
1 files changed, 20 insertions, 32 deletions
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index eb8c1164..e39eca0c 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -1,13 +1,11 @@ (************************************************************************) (* 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-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreduction.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Normalisation functions for rational numbers. *) Require Export QArith_base. @@ -43,23 +41,16 @@ Definition Qred (q:Q) := Lemma Qred_correct : forall q, (Qred q) == q. Proof. unfold Qred, Qeq; intros (n,d); simpl. - generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) - (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)). + generalize (Zggcd_gcd n ('d)) (Zgcd_nonneg n ('d)) + (Zggcd_correct_divisors n ('d)). destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl. Open Scope Z_scope. - intuition. - rewrite <- H in H0,H1; clear H. - rewrite H3; rewrite H4. - assert (0 <> g). - intro; subst g; discriminate. - - assert (0 < dd). - apply Zmult_gt_0_lt_0_reg_r with g. - omega. - rewrite Zmult_comm. - rewrite <- H4; compute; auto. - rewrite Z2P_correct; auto. - ring. + intros Hg LE (Hn,Hd). rewrite Hd, Hn. + rewrite <- Hg in LE; clear Hg. + assert (0 <> g) by (intro; subst; discriminate). + rewrite Z2P_correct. ring. + apply Zmult_gt_0_lt_0_reg_r with g; auto with zarith. + now rewrite Zmult_comm, <- Hd. Close Scope Z_scope. Qed. @@ -69,10 +60,10 @@ Proof. unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) - (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)). + (Zgcd_nonneg a ('b)) (Zggcd_correct_divisors a ('b)). destruct (Zggcd a (Zpos b)) as (g,(aa,bb)). generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) - (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)). + (Zgcd_nonneg c ('d)) (Zggcd_correct_divisors c ('d)). destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). simpl. intro H; rewrite <- H; clear H. @@ -80,10 +71,9 @@ Proof. intro H; rewrite <- H; clear H. intros Hg1 Hg2 (Hg3,Hg4). intros. - assert (g <> 0). - intro; subst g; discriminate. - assert (g' <> 0). - intro; subst g'; discriminate. + assert (g <> 0) by (intro; subst g; discriminate). + assert (g' <> 0) by (intro; subst g'; discriminate). + elim (rel_prime_cross_prod aa bb cc dd). congruence. unfold rel_prime in |- *. @@ -93,14 +83,13 @@ Proof. exists bb; auto with zarith. intros. inversion Hg1. - destruct (H6 (g*x)). + destruct (H6 (g*x)) as (x',Hx). rewrite Hg3. destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring. rewrite Hg4. destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring. - exists q. - apply Zmult_reg_l with g; auto. - pattern g at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring. (* /rel_prime *) unfold rel_prime in |- *. (* rel_prime *) @@ -109,14 +98,13 @@ Proof. exists dd; auto with zarith. intros. inversion Hg'1. - destruct (H6 (g'*x)). + destruct (H6 (g'*x)) as (x',Hx). rewrite Hg'3. destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring. rewrite Hg'4. destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring. - exists q. - apply Zmult_reg_l with g'; auto. - pattern g' at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring. (* /rel_prime *) assert (0<bb); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g. |