Library Coq.QArith.Qreduction

Normalisation functions for rational numbers.

Require Export QArith_base.
Require Import Znumtheory.

Notation Z2P := Z.to_pos (compat "8.3").
Notation Z2P_correct := Z2Pos.id (compat "8.3").

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))
  in r1 #(Z.to_pos 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).

Navigation