diff options
Diffstat (limited to 'theories/QArith/Qreduction.v')
| -rw-r--r-- | theories/QArith/Qreduction.v | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 131214f5..17307c82 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Normalisation functions for rational numbers. *) @@ -11,22 +13,22 @@ Require Export QArith_base. Require Import Znumtheory. -Notation Z2P := Z.to_pos (compat "8.3"). -Notation Z2P_correct := Z2Pos.id (compat "8.3"). +Notation Z2P := Z.to_pos (only parsing). +Notation Z2P_correct := Z2Pos.id (only parsing). (** Simplification of fractions using [Z.gcd]. This version can compute within Coq. *) Definition Qred (q:Q) := let (q1,q2) := q in - let (r1,r2) := snd (Z.ggcd q1 ('q2)) + let (r1,r2) := snd (Z.ggcd q1 (Zpos q2)) in r1#(Z.to_pos r2). Lemma Qred_correct : forall q, (Qred q) == q. Proof. unfold Qred, Qeq; intros (n,d); simpl. - generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d)) - (Z.ggcd_correct_divisors n ('d)). + generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d)) + (Z.ggcd_correct_divisors n (Zpos d)). destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl. Open Scope Z_scope. intros Hg LE (Hn,Hd). rewrite Hd, Hn. @@ -43,13 +45,13 @@ Proof. unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. intros H. - generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) - (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b)) + (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). simpl. intros <- Hg1 Hg2 (Hg3,Hg4). assert (Hg0 : g <> 0) by (intro; now subst g). - generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) - (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). + generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d)) + (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). assert (Hg'0 : g' <> 0) by (intro; now subst g'). @@ -101,7 +103,7 @@ Proof. - apply Qred_complete. Qed. -Add Morphism Qred : Qred_comp. +Add Morphism Qred with signature (Qeq ==> Qeq) as Qred_comp. Proof. intros. now rewrite !Qred_correct. Qed. @@ -125,19 +127,19 @@ Proof. intros; unfold Qminus'; apply Qred_correct; auto. Qed. -Add Morphism Qplus' : Qplus'_comp. +Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp. Proof. intros; unfold Qplus'. rewrite H, H0; auto with qarith. Qed. -Add Morphism Qmult' : Qmult'_comp. +Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp. Proof. intros; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. -Add Morphism Qminus' : Qminus'_comp. +Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp. Proof. intros; unfold Qminus'. rewrite H, H0; auto with qarith. |