diff options
Diffstat (limited to 'theories/QArith/Qreduction.v')
| -rw-r--r-- | theories/QArith/Qreduction.v | 169 |
1 files changed, 85 insertions, 84 deletions
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index c503daad..340cac83 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreduction.v 8989 2006-06-25 22:17:49Z letouzey $ i*) +(*i $Id: Qreduction.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** * Normalisation functions for rational numbers. *) +(** Normalisation functions for rational numbers. *) Require Export QArith_base. -Require Export Znumtheory. +Require Import Znumtheory. (** First, a function that (tries to) build a positive back from a Z. *) @@ -42,104 +42,105 @@ 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)). -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). + 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)). + 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). + + 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. + rewrite Z2P_correct; auto. + ring. + Close Scope Z_scope. Qed. Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q. Proof. -intros (a,b) (c,d). -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)). -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)). -destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). -simpl. -intro H; rewrite <- H; clear H. -intros Hg'1 Hg'2 (Hg'3,Hg'4). -intro H; rewrite <- H; clear H. -intros Hg1 Hg2 (Hg3,Hg4). -intros. -assert (g <> 0). + intros (a,b) (c,d). + 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)). + 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)). + destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). + simpl. + intro H; rewrite <- H; clear H. + intros Hg'1 Hg'2 (Hg'3,Hg'4). + intro H; rewrite <- H; clear H. + intros Hg1 Hg2 (Hg3,Hg4). + intros. + assert (g <> 0). intro; subst g; discriminate. -assert (g' <> 0). + assert (g' <> 0). intro; subst g'; discriminate. -elim (rel_prime_cross_prod aa bb cc dd). -congruence. -unfold rel_prime in |- *. -(*rel_prime*) -constructor. -exists aa; auto with zarith. -exists bb; auto with zarith. -intros. -inversion Hg1. -destruct (H6 (g*x)). -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. -(* /rel_prime *) -unfold rel_prime in |- *. -(* rel_prime *) -constructor. -exists cc; auto with zarith. -exists dd; auto with zarith. -intros. -inversion Hg'1. -destruct (H6 (g'*x)). -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. -(* /rel_prime *) -assert (0<bb); [|auto with zarith]. + elim (rel_prime_cross_prod aa bb cc dd). + congruence. + unfold rel_prime in |- *. + (*rel_prime*) + constructor. + exists aa; auto with zarith. + exists bb; auto with zarith. + intros. + inversion Hg1. + destruct (H6 (g*x)). + 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. + (* /rel_prime *) + unfold rel_prime in |- *. + (* rel_prime *) + constructor. + exists cc; auto with zarith. + exists dd; auto with zarith. + intros. + inversion Hg'1. + destruct (H6 (g'*x)). + 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. + (* /rel_prime *) + assert (0<bb); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g. omega. rewrite Zmult_comm. rewrite <- Hg4; compute; auto. -assert (0<dd); [|auto with zarith]. + assert (0<dd); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g'. omega. rewrite Zmult_comm. rewrite <- Hg'4; compute; auto. -apply Zmult_reg_l with (g'*g). -intro H2; elim (Zmult_integral _ _ H2); auto. -replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring]. -replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring]. -rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto. -Open Scope Q_scope. + apply Zmult_reg_l with (g'*g). + intro H2; elim (Zmult_integral _ _ H2); auto. + replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring]. + replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring]. + rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto. + Close Scope Z_scope. Qed. Add Morphism Qred : Qred_comp. Proof. -intros q q' H. -rewrite (Qred_correct q); auto. -rewrite (Qred_correct q'); auto. + intros q q' H. + rewrite (Qred_correct q); auto. + rewrite (Qred_correct q'); auto. Qed. Definition Qplus' (p q : Q) := Qred (Qplus p q). @@ -147,22 +148,22 @@ Definition Qmult' (p q : Q) := Qred (Qmult p q). Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). Proof. -intros; unfold Qplus' in |- *; apply Qred_correct; auto. + intros; unfold Qplus' in |- *; apply Qred_correct; auto. Qed. Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q). Proof. -intros; unfold Qmult' in |- *; apply Qred_correct; auto. + intros; unfold Qmult' in |- *; apply Qred_correct; auto. Qed. Add Morphism Qplus' : Qplus'_comp. Proof. -intros; unfold Qplus' in |- *. -rewrite H; rewrite H0; auto with qarith. + intros; unfold Qplus' in |- *. + rewrite H; rewrite H0; auto with qarith. Qed. Add Morphism Qmult' : Qmult'_comp. -intros; unfold Qmult' in |- *. -rewrite H; rewrite H0; auto with qarith. + intros; unfold Qmult' in |- *. + rewrite H; rewrite H0; auto with qarith. Qed. |