Library Coq.QArith.Qreduction



Normalisation functions for rational numbers.

Require Export QArith_base.
Require Import Znumtheory.

First, a function that (tries to) build a positive back from a Z.

Definition Z2P (z : Z) :=
  match z with
  | Z0 => 1%positive
  | Zpos p => p
  | Zneg p => p
  end.

Lemma Z2P_correct : forall z : Z, (0 < z)%Z -> Zpos (Z2P z) = z.

Lemma Z2P_correct2 : forall z : Z, 0%Z <> z -> Zpos (Z2P z) = Zabs z.

Simplification of fractions using Zgcd. This version can compute within Coq.

Definition Qred (q:Q) :=
  let (q1,q2) := q in
  let (r1,r2) := snd (Zggcd q1 ('q2))
  in r1#(Z2P r2).

Lemma Qred_correct : forall q, (Qred q) == q.
  Open Scope Z_scope.
  Close Scope Z_scope.

Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q.
  Open Scope Z_scope.
  Close Scope Z_scope.

Add Morphism Qred : Qred_comp.

Definition Qplus' (p q : Q) := Qred (Qplus p q).
Definition Qmult' (p q : Q) := Qred (Qmult p q).
Definition Qminus' x y := Qred (Qminus x y).

Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).

Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q).

Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).

Add Morphism Qplus' : Qplus'_comp.

Add Morphism Qmult' : Qmult'_comp.
Qed.

Add Morphism Qminus' : Qminus'_comp.
Qed.

Lemma Qred_opp: forall q, Qred (-q) = - (Qred q).

Theorem Qred_compare: forall x y,
  Qcompare x y = Qcompare (Qred x) (Qred y).