Q

About Q

We define the structure of rational numbers as follows. First of all, it consists of the set of rational numbers, defined as the set of pairs ⟨a,n⟩ with a:Z and n:positive. Intuitively, ⟨a,n⟩ represents the rational number a[/]n. Then there is the equality on Q: ⟨a,m⟩=⟨b,n⟩ iff an [=] bm. We also define apartness, order, addition, multiplication, opposite, inverse an de constants 0 and 1.

Section Q.
Definition Qap (x y : Q) := ~(Qeq x y).

Definition 0_Q := Qmake 0 1.

Definition 1_Q := Qmake 1 1.

Definition Qinv (x : Q) (x_ : ~(Qeq x 0_Q)) := Qinv x.

End Q.

Infix "/=" := Qap (no associativity, at level 70) : Q_scope.

Constants

Definition 2_Q := Qmake 2%positive 1%positive.

Definition 4_Q := Qmake 4%positive 1%positive.

Equality

Here we prove that 1_Q is not equal to 0_Q:

Theorem ONEQ_neq_ZEROQ : ~ (1_Q==QZERO).

Theorem refl_Qeq : forall x :Q, x==x.

Theorem sym_Qeq : forall x y : Q, (x==y) -> y==x.

Theorem trans_Qeq : forall x y z : Q, (x==y) -> (y==z) -> x==z.

The equality is decidable:

Theorem dec_Qeq : forall x y : Q, {x==y} + {~ (x==y)}.

Apartness

Lemma Q_non_zero : forall x : Q, (x/=QZERO) -> Qnum x <> 0%Z.

Lemma ap_Q_irreflexive0 : forall x : Q, ~ (x/=x).

Lemma ap_Q_symmetric0 : forall x y : Q, (x/=y) -> y/=x.

Lemma ap_Q_cotransitive0 : forall x y : Q, (x/=y) ->
forall z : Q, (x/=z) or (z/=y).

Lemma ap_Q_tight0 : forall x y : Q, ~ (x/=y) <-> x==y.

Addition

Theorem Qplus_simpl : forall n m p q : Q,
(n==m) -> (p==q) -> n+p==m+q.

Addition is associative:

Theorem Qplus_assoc : forall x y z : Q, x+(y+z)==(x+y)+z.

0_Q as the neutral element for addition:

Theorem QZERO_right : forall x : Q, x+QZERO==x.

Commutativity of addition:

Theorem Qplus_sym : forall x y : Q, x+y==y+x.

Lemma Qplus_strext0 : forall x1 x2 y1 y2 : Q,
(x1+y1/=x2+y2) -> (x1/=x2) or (y1/=y2).

Lemma ZEROQ_as_rht_unit0 : forall x : Q, x+QZERO==x.

Lemma ZEROQ_as_lft_unit0 : forall x : Q, 0_Q+x==x.

Lemma Qplus_is_commut0 : forall x y : Q, x+y==y+x.

Opposite

- is a well defined unary operation:

Lemma Qopp_simpl : forall x y : Q, (x==y) -> - x==- y.

The group equation for -

Theorem Qplus_inverse_r : forall q : Q, q+-q==QZERO.

Multiplication

Next we shall prove the properties of multiplication. First we prove that * is well-defined

Theorem Qmult_simpl : forall n m p q : Q,
(n==m) -> (p==q) -> n*p==m*q.

and it is associative:

Theorem Qmult_assoc : forall n m p : Q, n*(m*p)==(n*m)*p.

1_Q is the neutral element for multiplication:

Theorem Qmult_n_1 : forall n : Q, n*QONE==n.

The commutativity for *:

Theorem Qmult_sym : forall x y : Q, x*y==y*x.

Theorem Qmult_plus_distr_r : forall x y z : Q,
x*(y+z)==x*y+x*z.

And a property of multiplication which says if x [~=] Zero and xy [=] Zero then y [=] Zero:

Theorem Qmult_eq : forall x y : Q,
~ (x==QZERO) -> (x*y==QZERO) -> y==QZERO.

Lemma Qmult_strext0 : forall x1 x2 y1 y2 : Q,
(x1*y1/=x2*y2) -> (x1/=x2) or (y1/=y2).

Lemma nonZero : forall x : Q, ~(x==QZERO) ->
~(Qmake (Zsgn (Qnum x) * Qden x)%Z (posZ (Qnum x))==QZERO).

Inverse

Lemma Qinv_strext : forall (x y : Q) x_ y_,
~(Qinv x x_==Qinv y y_) -> ~(x==y).

Lemma Qinv_is_inv : forall (x : Q) (Hx : x/=QZERO),
(x*Qinv x Hx==QONE) /\ (Qinv x Hx*x==QONE).

Less-than

Lemma Qlt_wd_right : forall x y z : Q, (x<y) -> (y==z) -> x<z.

Lemma Qlt_wd_left : forall x y z : Q, (x<y) -> (x==z) -> z<y.

Lemma Qlt_eq_gt_dec : forall q1 q2 : Q, ((q1<q2) or (q1==q2)) or (q2<q1).

Lemma Qlt_is_transitive_unfolded : forall x y z : Q, (x<y) -> (y<z) -> x<z.

Lemma Qlt_strext_unfolded : forall x1 x2 y1 y2 : Q,
(x1<y1) -> (x2<y2) or (x1/=x2) or (y1/=y2).

Lemma Qlt_is_irreflexive_unfolded : forall x : Q, ~ (x<x).

Lemma Qlt_is_antisymmetric_unfolded : forall x y : Q, (x<y) -> ~ (y<x).

Lemma Qplus_resp_Qlt : forall x y : Q, (x<y) -> forall z : Q, x+z<y+z.

Lemma Qmult_resp_pos_Qlt : forall x y : Q, (0_Q<x) -> (0_Q<y) -> 0_Q<x*y.

Lemma Qlt_gives_apartness : forall x y : Q, ⇔ (x/=y) ((x<y) or (y<x)).

Miscellaneous

We consider the injection inject_Z from Z to Q as a coercion.

Coercion inject_Z : Z >-> Q.

Lemma injz_plus : forall m n : Z,
(inject_Z (m + n):Q)==(inject_Z m:Q)+inject_Z n.

Lemma injZ_One : (inject_Z 1:Q)==QONE.

We can always find a natural Qnumber that is bigger than a given rational Qnumber.

Theorem Q_is_archemaedian0 : forall x : Q,
{n : positive | x<Qmake n 1%positive}.

Lemma Qle_is_not_lt : forall x y : Q, x <= y <-> ~ y < x.

Lemma Qge_is_not_gt : forall x y : Q, x >= y <-> y <= x.

Lemma Qgt_is_lt : forall x y : Q, x > y IFF y < x.