CoRN.model.structures.Qpossec

Require Export QArith.
Require Import Qpower.
Require Import Qordfield.
Require Import COrdFields2.
Require Import Eqdep_dec.
Require Import CornTac.
Require Import Qround.
Require Import Qabs.
Require Import stdlib_omissions.Q.

Open Local Scope Q_scope.

Q⁺

Definition Q⁺: Set := sig (Qlt 0).

Program Definition QposMake (num den: positive): Q⁺ := num # den.

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

Delimit Scope Qpos_scope with Q⁺.

Program Definition integral_Qpos (p: positive): Q⁺ := (p:Q).

Coercion integral_Qpos: positive >-> Q⁺.

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

Definition QposAsQ: Q⁺ -> Q := @proj1_sig _ _.

Coercion QposAsQ : Q⁺ >-> Q.

Basic properties about Q⁺

Definition Qpos_prf : forall a:Q⁺, 0 < a := @proj2_sig _ _.

Hint Immediate Qpos_prf.

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

Lemma Qpos_nonzero' (q: Q⁺): ~ q == 0.

Hint Immediate Qpos_nonzero'.

Lemma Qpos_nonneg : forall a:Q⁺, 0 <= a.

Hint Immediate Qpos_nonneg.

Lemma Qopp_Qpos_neg (x: Q⁺): -x < 0.

Hint Immediate Qopp_Qpos_neg.

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

Definition mkQpos: forall (a:Q) (p:0 < a), Q⁺ := @exist Q (Qlt 0).

Lemma QposAsmkQpos : forall (a:Q) (p:0<a), (QposAsQ (mkQpos p))=a.

Lemma positive_Z (z: Z): Zlt 0 z -> sig (fun p: positive => Zpos p = z).

Require Eqdep_dec.
Definition comparison_eq_dec (a b: comparison): { a = b } + { a <> b }.
Defined.

Lemma Zlt_uniq (a b: Z) (p q: (a < b)%Z): p = q.

Lemma Qlt_uniq (a b: Q) (p q: a < b): p = q.

Program Definition Qpos_as_positive_ratio (q: Q⁺):
  sig (fun ps: positive * positive => q = QposMake (fst ps) (snd ps)) :=
  (positive_Z (Qnum q) _, Qden q ).

Lemma Qpos_positive_numerator_rect (P: Q⁺ -> Type):
  (forall (a b: positive), P (a # b)%Q⁺) -> forall q, P q.

Lemma QposAsQposMake : forall a b, (QposAsQ (QposMake a b)) = (Zpos a )#b.

Equality

Definition QposEq (a b:Q⁺) := Qeq a b.
Instance Qpos_default : @DefaultRelation Q⁺ QposEq | 2.

Add Relation Q⁺ QposEq
reflexivity proved by (fun (x:Q⁺) => Qeq_refl x)
symmetry proved by (fun (x y:Q⁺) => Qeq_sym x y)
transitivity proved by (fun (x y z:Q⁺) => Qeq_trans x y z) as QposSetoid.

Definition QposAp (a b:Q⁺) := Qap a b.

Definition Qpos_PI (a b: Q⁺): (a: Q ) = b -> a = b.

Addition

Program Definition Qpos_plus (x y:Q⁺) : Q⁺ := Qplus x y.

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

One

Program Definition Qpos_one : Q⁺ := 1.
Notation "1" := Qpos_one : Qpos_scope.

Lemma Q_Qpos_one : (1%Q⁺:Q )=(1:Q ).

Multiplication

Program Definition Qpos_mult (x y:Q⁺) : Q⁺ := Qmult x y.

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

Inverse

Program Definition Qpos_inv (x:Q⁺): Q⁺ := / x.

Lemma Q_Qpos_inv : forall (x:Q⁺), Qpos_inv x = / x :> Q.
Hint Rewrite Q_Qpos_inv : QposElim.

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.

Ltac QposRing :=
unfold canonical_names.equiv, QposEq;
autorewrite with QposElim;
ring.

Ltac QposField :=
unfold canonical_names.equiv, QposEq;
autorewrite with QposElim;
field.

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:Q⁺ | b ==(a +c)}.

Power

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

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

Infix "^" := Qpos_power : Qpos_scope.
Lemma Q_Qpos_power : forall (x:Q⁺) z, ((x ^z)%Q⁺:Q )==(x:Q )^z.
Hint Rewrite Q_Qpos_power : QposElim.

Summing lists

Definition QposSum (l:list Q⁺) : Q := fold_right
(fun (x:Q⁺) (y:Q) => x +y) (Zero: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:Q⁺) : Q⁺ := mkQpos (QposRed_prf a (Qpos_prf a)).

Instance QposRed_complete: Proper (QposEq ==> eq) QposRed.

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

Definition QposCeiling (q: Q⁺): positive :=
  match Qceiling q with
  | Zpos p => p
  | _ => 1%positive
  end.

Lemma QposCeiling_Qceiling (q: Q⁺): (QposCeiling q: Z ) = Qceiling q.

Definition QabsQpos (x : Q) : Q⁺ :=
  match x with
  | 0 # _ => (1%Q⁺)
  | (Zpos an) # ad => (an # ad)%Q⁺
  | (Zneg an) # ad => (an # ad)%Q⁺
  end.

Lemma QabsQpos_correct x : ~x == 0 -> QabsQpos x == Qabs x.

Lemma QabsQpos_Qpos (x : Q⁺) : QposEq (QabsQpos x) x.