Q⁺

We define Q⁺ as a pair of positives (n,d) which represents the fraction n/d.

Record Q⁺ : Set := QposMake
{QposNumerator : positive
;QposDenominator : positive
}.

Notation "a # b" := (QposMake a b) (at level 55, no associativity) : Qpos_scope.

There is an injection from Q⁺ to Q that we make into a coersion.

Definition QposAsQ (a:Qpos) : Q :=
(Zpos (QposNumerator a))#(QposDenominator a).

Coercion QposAsQ : Q⁺ >-> Q.

Basic properties about Q⁺

Lemma Qpos_prf : forall a:Qpos, 0 < a.

Lemma Qpos_nonzero : forall x:Qpos, (x:Q)[#]0.

Lemma Qpos_nonneg : forall a:Qpos, 0 <= a.

Any positive rational number can be transformed into a Q⁺.

Definition mkQpos (a:Q) (p:0 < a) : Q⁺.
Defined.
Lemma QposAsmkQpos : forall (a:Q) (p:0<a), (QposAsQ (mkQpos p))=a.
Lemma QposAsQposMake : forall a b, (QposAsQ (QposMake a b)) = (Zpos a)#b.

Equality

Definition QposEq (a b:Qpos) := Qeq a b.

Add Relation Q⁺ QposEq
reflexivity proved by (fun (x:Qpos) => refl_Qeq x)
symmetry proved by (fun (x y:Qpos) => sym_Qeq x y)
transitivity proved by (fun (x y z:Qpos) => trans_Qeq x y z) as QposSetoid.

Definition QposAp (a b:Qpos) := Qap a b.

Addition

Definition Qpos_plus (x y:Qpos) : Q⁺.
Defined.

Infix "+" := Qpos_plus : Qpos_scope.
Lemma Q_Qpos_plus : forall (x y:Qpos), ((x + y)%Qpos:Q)=(x:Q)+(y:Q).

Multiplicaiton

Definition Qpos_mult (x y:Qpos) : Q⁺.
Defined.

Infix "*" := Qpos_mult : Qpos_scope.
Lemma Q_Qpos_mult : forall (x y:Qpos), ((x * y)%Qpos:Q)=(x:Q)*(y:Q).

Inverse

Definition Qpos_inv (x:Qpos) : Q⁺ :=
((QposDenominator x)#(QposNumerator x))%Qpos.
Lemma Q_Qpos_inv : forall (x:Qpos), Qpos_inv x = / x :> Q.

Notation "a / b" := (Qpos_mult a (Qpos_inv b)) : Qpos_scope.

Tactics

These tactics solve Ring and Field equations over Q⁺ by converting them to problems over Q.

This is a standard way of decomposing a rational b that is greater than a into a plus a positive value c.

Lemma Qpos_lt_plus : forall (a b:Q),
a< b ->
{c:Qpos | b==(a+c)}.

Power

Lemma Qpos_power_pos : forall (x:Qpos) z, 0 < x^z.

Definition Qpos_power (x:Qpos) (z:Z) : Q⁺.
Defined.

Infix "^" := Qpos_power : Qpos_scope.

The default relation on Z is eqm otherwise.

Instance Z_default : @DefaultRelation Z (@eq Z).
Lemma Q_Qpos_power : forall (x:Qpos) z, ((x^z)%Qpos:Q)==(x:Q)^z.

Summing lists

Definition QposSum (l:list Q⁺) : Q := fold_right
(fun (x:Qpos) (y:Q) => x+y) (0:Q) l.

Lemma QposSumNonNeg : forall l, 0 <= QposSum l.

A version of Qred for Q⁺.

Lemma QposRed_prf : forall (a:Q), (0 < a) -> (0 < Qred a).

Definition QposRed (a:Qpos) : Q⁺ := mkQpos (QposRed_prf a (Qpos_prf a)).

Lemma QposRed_complete : forall p q : Q⁺, p == q -> QposRed p = QposRed q.

Lemma QposRed_correct : forall p, QposRed p == p.

Q+