Library ssrrat

Require Import Rbase ProofIrrelevance Eqdep_dec List.
Require Import ssreflect ssrnat eqtype ssrbool ssrfun.
Require Import ZArith_ext Arith_ext seq_ext div_ext.
Require Import order.

Close Local Scope Z_scope.
Close Local Scope positive_scope.

Record pos_nat : Type := PosNat { pos_nat_val :> nat; _ : pos_nat_val > 0 }.

This file provides an implementation of rational numbers.

Record rat : Set := Rat {
  num : Z ;
  den : pos_nat ;
  irr : gcdn (Zabs_nat num) den = 1
}.

Definition p1 := @PosNat 1 is_true_true.
Definition inj_nat_rat n : rat := Rat (Z_of_nat n) p1 (gcdn1 (Zabs_nat _)).
Coercion inj_nat_rat : nat >-> rat.
Definition q0 : rat := 0%nat.
Definition q1 : rat := 1%nat.
Definition q2 : rat := 2%nat.
Definition q3 : rat := 3%nat.
Definition q4 : rat := 4%nat.

Definition p2 := @PosNat 2 is_true_true.
Definition p3 := @PosNat 3 is_true_true.
Definition p4 := @PosNat 4 is_true_true.
Definition p8 := @PosNat 8 is_true_true.
Definition p16 := @PosNat 16 is_true_true.
Definition p32 := @PosNat 32 is_true_true.

Lemma gcd_q23 : gcdn (Zabs_nat 2) p3 = 1.
Definition q23 := Rat 2 p3 gcd_q23.
Definition q12 := Rat 1 p2 (gcd1n _).
Definition q14 := Rat 1 p4 (gcd1n _).
Definition q13 := Rat 1 p3 (gcd1n _).
Definition q18 := Rat 1 p8 (gcd1n _).
Definition q116 := Rat 1 p16 (gcd1n _).
Definition q132 := Rat 1 p32 (gcd1n _).

eqType for rat

Definition eqrat p q := Zeq_bool (num p) (num q) && eqn (den p) (den q).

Lemma eqratP : Equality.axiom eqrat.

Canonical Structure rat_eqMixin := EqMixin eqratP.
Canonical Structure rat_eqType := Eval hnf in EqType _ rat_eqMixin.

Lemma rat_irrelevance : forall (x y : rat) (E E' : x = y), E = E'.

irreducible fraction

Definition redu_num n (d:pos_nat) :=
  let: new_num := Z_of_nat (Zabs_nat n %/ gcdn (Zabs_nat n) d) in
    if Zlt_bool n 0 then Zopp new_num else new_num.

Lemma redu_num_gcdn1 : forall n (m : pos_nat), gcdn (Zabs_nat n) m = 1 ->
  redu_num n m = n.

Definition redu_den' n (d:pos_nat) := d %/ gcdn (Zabs_nat n) d.
Lemma redu_den'_prop : forall n d, 0 < redu_den' n d.
Definition redu_den n d := PosNat _ (redu_den'_prop n d).

Lemma redu_prop' : forall n d, 0 < d ->
  gcdn (n %/ gcdn n d) (d %/ gcdn n d) = 1.

NB: statement similar to Znumtheory/Zis_gcd_rel_prime (Coq8.2)

Lemma redu_prop : forall n d, gcdn (Zabs_nat (redu_num n d)) (redu_den n d) = 1.

addition

Definition addq_num p q := (num p * Z_of_nat (den q) + num q * Z_of_nat (den p))%Z.
Definition addq_den' p q := den p * den q.
Lemma addq_den'_prop : forall n d, 0 < addq_den' n d.
Definition addq_den p q := PosNat _ (addq_den'_prop p q).
Definition addq p q :=
  let: num := addq_num p q in
    let: den := addq_den p q in
      Rat (redu_num num den) (redu_den num den) (redu_prop num den).

Notation "p + q" := (addq p q) : rat_scope.
Open Local Scope rat_scope.

Lemma pos_nat_eq : forall a b, a = b ->
  forall (H: 0 < a) (H': 0 < b),
    PosNat _ H = PosNat _ H'.

Lemma addq_num_q0 : forall p, addq_num p q0 = num p.

Lemma addq_den_q0 : forall p, addq_den p q0 = den p.

Lemma rat_eq : forall a b a' b', a = a' -> b = b' ->
  forall H H', Rat a b H = Rat a' b' H'.

Lemma addq0 : right_id q0 addq.

Definition pr p := let: Rat n d _ := p in (n, pos_nat_val d).

Lemma pr_prop : forall q p, pr q = pr p -> q = p.

Lemma q12_plus_q12 : pr (q12 + q12) = (1%Z, 1).

Lemma q13_plus_q23 : pr (q13 + q23) = (1%Z, 1).

multiplication

Definition mulq_num p q := (num p * num q)%Z.
Definition mulq_den' p q := den p * den q.
Lemma mulq_den'_prop : forall n d, 0 < mulq_den' n d.
Definition mulq_den p q := PosNat _ (mulq_den'_prop p q).
Definition mulq p q :=
  let: num := mulq_num p q in
    let: den := mulq_den p q in
      Rat (redu_num num den) (redu_den num den) (redu_prop num den).

Notation "p * q" := (mulq p q) : rat_scope.

inverse

Definition PosNat_of_pos p := PosNat _ (introTF (c:=true) ltP (lt_O_nat_of_P p)).

Lemma gcdnC_pos : forall n d, gcdn (Zabs_nat (Zpos n)) d = 1 ->
gcdn (Zabs_nat (Z_of_nat d)) (PosNat_of_pos n) = 1.

Lemma gcdnC_neg : forall n d, gcdn (Zabs_nat (Zneg n)) d = 1 ->
gcdn (Zabs_nat (-(Z_of_nat d))) (PosNat_of_pos n) = 1.

NB: invq returns 0 for division by 0

Definition invq p : rat :=
  let: Rat n d i := p in
    match n as z return gcdn (Zabs_nat z) d = 1 -> rat with
      | Z0 => fun _ => q0
      | Zpos p => fun i => Rat (Z_of_nat d) (PosNat_of_pos p) (gcdnC_pos p d i)
      | Zneg p => fun i => Rat (- Z_of_nat d) (PosNat_of_pos p) (gcdnC_neg p d i)
    end i.

Notation "/ p" := (invq p) : rat_scope.

division

NB: divq returns 0 for division by 0

Definition divq p q := mulq p (invq q).

Notation "p / q" := (divq p q) : rat_scope.

comparison

Definition ltq p q :=
  Zlt_bool (num p * Z_of_nat (den q)) (num q * Z_of_nat (den p)).

Notation "p < q" := (ltq p q) : rat_scope.

Lemma ltq_trans : forall (q p r:rat), p < q -> q < r -> p < r.

Lemma ltq_irr : forall p, p < p = false.

Lemma ltq_neq : forall (p q:rat), p < q -> p <> q.

Close Local Scope rat_scope.

Lemma tmp : forall a b c d,
  0 < a -> 0 < c ->
  coprime a b ->
  coprime c d ->
  a * d = c * b ->
  a = c /\ b = d.

Lemma tmp' : forall a b c d,
  coprime a b -> coprime c d ->
  a * d = c * b ->
  a = c /\ b = d.

Lemma tmp'' : forall (a:Z) b (c:Z) d,
  0 < b -> 0 < d ->
  coprime (Zabs_nat a) b -> coprime (Zabs_nat c) d ->
  (a * (Z_of_nat d) = c * (Z_of_nat b))%Z ->
  a = c /\ b = d.

Open Local Scope rat_scope.

Lemma ltq_total : forall p q, (p != q) = (p < q) || (q < p).

Definition leq p q :=
  Zle_bool (num p * Z_of_nat (den q)) (num q * Z_of_nat (den p)).

Notation "p <= q" := (ltq p q) : rat_scope.

Fixpoint sumq (l: seq rat_eqType) :=
  if l is h :: t then addq h (sumq t) else q0.

Lemma seq_pr_prop : forall (l l':seq rat_eqType), size l = size l' ->
  List.map pr (s2l l) = List.map pr (s2l l') ->
  l = l'.

strictly positive rationals

Record pos_rat : Set := PosRat {
val : rat ;
Hval : (0 < num val)%Z
}.

Lemma prat1_prop : (0 < num q1)%Z.
Definition prat1 := PosRat q1 prat1_prop.

Lemma q12p_prop : (0 < num q12)%Z.
Definition q12p := PosRat q12 q12p_prop.

Lemma q14p_prop : (0 < num q14)%Z.
Definition q14p := PosRat q14 q14p_prop.

Lemma q18p_prop : (0 < num q18)%Z.
Definition q18p := PosRat q18 q18p_prop.

Definition eqpos_rat p q := eqrat (val p) (val q).

Lemma eqposratP : Equality.axiom eqpos_rat.

Canonical Structure posrat_eqMixin := EqMixin eqposratP.
Canonical Structure posrat_eqType := Eval hnf in EqType _ posrat_eqMixin.

Definition inj_pos_rat q := let: PosRat v _ := q in v.

Coercion inj_pos_rat : pos_rat >-> rat.

Definition rat2R p := let: Rat n d _ := p in (IZR n / INR d)%R.

Coercion rat2R : rat >-> R.