Library Coq.Numbers.Rational.BigQ.QMake
Require Import BigNumPrelude ROmega.
Require Import QArith Qcanon Qpower.
Require Import NSig ZSig QSig.
Module Type NType_ZType (N:NType)(Z:ZType).
Parameter Z_of_N : N.t -> Z.t.
Parameter spec_Z_of_N : forall n, Z.to_Z (Z_of_N n) = N.to_Z n.
Parameter Zabs_N : Z.t -> N.t.
Parameter spec_Zabs_N : forall z, N.to_Z (Zabs_N z) = Zabs (Z.to_Z z).
End NType_ZType.
Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
The notation of a rational number is either an integer x,
interpreted as itself or a pair (x,y) of an integer x and a natural
number y interpreted as x/y. The pairs (x,0) and (0,y) are all
interpreted as 0.
Specification with respect to QArith
Open Local Scope Q_scope.
Definition of_Z x: t := Qz (Z.of_Z x).
Definition of_Q (q:Q) : t :=
let (x,y) := q in
match y with
| 1%positive => Qz (Z.of_Z x)
| _ => Qq (Z.of_Z x) (N.of_N (Npos y))
end.
Definition to_Q (q: t) :=
match q with
| Qz x => Z.to_Z x # 1
| Qq x y => if N.eq_bool y N.zero then 0
else Z.to_Z x # Z2P (N.to_Z y)
end.
Notation "[ x ]" := (to_Q x).
Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q.
Theorem spec_of_Q: forall q: Q, [of_Q q] == q.
Definition eq x y := [x] == [y].
Definition zero: t := Qz Z.zero.
Definition one: t := Qz Z.one.
Definition minus_one: t := Qz Z.minus_one.
Lemma spec_0: [zero] == 0.
Lemma spec_1: [one] == 1.
Lemma spec_m1: [minus_one] == -(1).
Definition compare (x y: t) :=
match x, y with
| Qz zx, Qz zy => Z.compare zx zy
| Qz zx, Qq ny dy =>
if N.eq_bool dy N.zero then Z.compare zx Z.zero
else Z.compare (Z.mul zx (Z_of_N dy)) ny
| Qq nx dx, Qz zy =>
if N.eq_bool dx N.zero then Z.compare Z.zero zy
else Z.compare nx (Z.mul zy (Z_of_N dx))
| Qq nx dx, Qq ny dy =>
match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
| true, true => Eq
| true, false => Z.compare Z.zero ny
| false, true => Z.compare nx Z.zero
| false, false => Z.compare (Z.mul nx (Z_of_N dy))
(Z.mul ny (Z_of_N dx))
end
end.
Lemma Zcompare_spec_alt :
forall z z', Z.compare z z' = (Z.to_Z z ?= Z.to_Z z')%Z.
Lemma Ncompare_spec_alt :
forall n n', N.compare n n' = (N.to_Z n ?= N.to_Z n')%Z.
Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z ->
Zpos (Z2P (N.to_Z n)) = N.to_Z n.
Hint Rewrite
Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l
Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
Zcompare_spec_alt Ncompare_spec_alt
Z.spec_add N.spec_add Z.spec_mul N.spec_mul
Z.spec_gcd N.spec_gcd Zgcd_Zabs
spec_Z_of_N spec_Zabs_N
: nz.
Ltac nzsimpl := autorewrite with nz in *.
Ltac destr_neq_bool := repeat
(match goal with |- context [N.eq_bool ?x ?y] =>
generalize (N.spec_eq_bool x y); case N.eq_bool
end).
Ltac destr_zeq_bool := repeat
(match goal with |- context [Z.eq_bool ?x ?y] =>
generalize (Z.spec_eq_bool x y); case Z.eq_bool
end).
Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega).
Tactic Notation "simpl_ndiv" "in" "*" :=
rewrite N.spec_div in * by (nzsimpl; romega).
Ltac simpl_zdiv := rewrite Z.spec_div by (nzsimpl; romega).
Tactic Notation "simpl_zdiv" "in" "*" :=
rewrite Z.spec_div in * by (nzsimpl; romega).
Ltac qsimpl := try red; unfold to_Q; simpl; intros;
destr_neq_bool; destr_zeq_bool; simpl; nzsimpl; auto; intros.
Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
Definition lt n m := compare n m = Lt.
Definition le n m := compare n m <> Gt.
Definition min n m := match compare n m with Gt => m | _ => n end.
Definition max n m := match compare n m with Lt => m | _ => n end.
Definition eq_bool n m :=
match compare n m with Eq => true | _ => false end.
Theorem spec_eq_bool: forall x y,
if eq_bool x y then [x] == [y] else ~([x] == [y]).
Normalisation function
Definition norm n d : t :=
let gcd := N.gcd (Zabs_N n) d in
match N.compare N.one gcd with
| Lt =>
let n := Z.div n (Z_of_N gcd) in
let d := N.div d gcd in
match N.compare d N.one with
| Gt => Qq n d
| Eq => Qz n
| Lt => zero
end
| Eq => Qq n d
| Gt => zero
end.
Theorem spec_norm: forall n q, [norm n q] == [Qq n q].
Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q].
Reduction function : producing irreducible fractions
Definition red (x : t) : t :=
match x with
| Qz z => x
| Qq n d => norm n d
end.
Definition Reduced x := [red x] = [x].
Theorem spec_red : forall x, [red x] == [x].
Theorem strong_spec_red : forall x, [red x] = Qred [x].
Definition add (x y: t): t :=
match x with
| Qz zx =>
match y with
| Qz zy => Qz (Z.add zx zy)
| Qq ny dy =>
if N.eq_bool dy N.zero then x
else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
end
| Qq nx dx =>
if N.eq_bool dx N.zero then y
else match y with
| Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
| Qq ny dy =>
if N.eq_bool dy N.zero then x
else
let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
let d := N.mul dx dy in
Qq n d
end
end.
Theorem spec_add : forall x y, [add x y] == [x] + [y].
Definition add_norm (x y: t): t :=
match x with
| Qz zx =>
match y with
| Qz zy => Qz (Z.add zx zy)
| Qq ny dy =>
if N.eq_bool dy N.zero then x
else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
end
| Qq nx dx =>
if N.eq_bool dx N.zero then y
else match y with
| Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
| Qq ny dy =>
if N.eq_bool dy N.zero then x
else
let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
let d := N.mul dx dy in
norm n d
end
end.
Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y].
Theorem strong_spec_add_norm : forall x y : t,
Reduced x -> Reduced y -> Reduced (add_norm x y).
Definition opp (x: t): t :=
match x with
| Qz zx => Qz (Z.opp zx)
| Qq nx dx => Qq (Z.opp nx) dx
end.
Theorem strong_spec_opp: forall q, [opp q] = -[q].
Theorem spec_opp : forall q, [opp q] == -[q].
Theorem strong_spec_opp_norm : forall q, Reduced q -> Reduced (opp q).
Definition sub x y := add x (opp y).
Theorem spec_sub : forall x y, [sub x y] == [x] - [y].
Definition sub_norm x y := add_norm x (opp y).
Theorem spec_sub_norm : forall x y, [sub_norm x y] == [x] - [y].
Theorem strong_spec_sub_norm : forall x y,
Reduced x -> Reduced y -> Reduced (sub_norm x y).
Definition mul (x y: t): t :=
match x, y with
| Qz zx, Qz zy => Qz (Z.mul zx zy)
| Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy
| Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx
| Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
end.
Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
Lemma norm_denum : forall n d,
[if N.eq_bool d N.one then Qz n else Qq n d] == [Qq n d].
Definition irred n d :=
let gcd := N.gcd (Zabs_N n) d in
match N.compare gcd N.one with
| Gt => (Z.div n (Z_of_N gcd), N.div d gcd)
| _ => (n, d)
end.
Lemma spec_irred : forall n d, exists g,
let (n',d') := irred n d in
(Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z.
Lemma spec_irred_zero : forall n d,
(N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z.
Lemma strong_spec_irred : forall n d,
(N.to_Z d <> 0%Z) ->
let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z.
Definition mul_norm_Qz_Qq z n d :=
if Z.eq_bool z Z.zero then zero
else
let gcd := N.gcd (Zabs_N z) d in
match N.compare gcd N.one with
| Gt =>
let z := Z.div z (Z_of_N gcd) in
let d := N.div d gcd in
if N.eq_bool d N.one then Qz (Z.mul z n) else Qq (Z.mul z n) d
| _ => Qq (Z.mul z n) d
end.
Definition mul_norm (x y: t): t :=
match x, y with
| Qz zx, Qz zy => Qz (Z.mul zx zy)
| Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy
| Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx
| Qq nx dx, Qq ny dy =>
let (nx, dy) := irred nx dy in
let (ny, dx) := irred ny dx in
let d := N.mul dx dy in
if N.eq_bool d N.one then Qz (Z.mul ny nx) else Qq (Z.mul ny nx) d
end.
Lemma spec_mul_norm_Qz_Qq : forall z n d,
[mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d].
Lemma strong_spec_mul_norm_Qz_Qq : forall z n d,
Reduced (Qq n d) -> Reduced (mul_norm_Qz_Qq z n d).
Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y].
Theorem strong_spec_mul_norm : forall x y,
Reduced x -> Reduced y -> Reduced (mul_norm x y).
Definition inv (x: t): t :=
match x with
| Qz z =>
match Z.compare Z.zero z with
| Eq => zero
| Lt => Qq Z.one (Zabs_N z)
| Gt => Qq Z.minus_one (Zabs_N z)
end
| Qq n d =>
match Z.compare Z.zero n with
| Eq => zero
| Lt => Qq (Z_of_N d) (Zabs_N n)
| Gt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
end
end.
Theorem spec_inv : forall x, [inv x] == /[x].
Definition inv_norm (x: t): t :=
match x with
| Qz z =>
match Z.compare Z.zero z with
| Eq => zero
| Lt => Qq Z.one (Zabs_N z)
| Gt => Qq Z.minus_one (Zabs_N z)
end
| Qq n d =>
if N.eq_bool d N.zero then zero else
match Z.compare Z.zero n with
| Eq => zero
| Lt =>
match Z.compare n Z.one with
| Gt => Qq (Z_of_N d) (Zabs_N n)
| _ => Qz (Z_of_N d)
end
| Gt =>
match Z.compare n Z.minus_one with
| Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
| _ => Qz (Z.opp (Z_of_N d))
end
end
end.
Theorem spec_inv_norm : forall x, [inv_norm x] == /[x].
Theorem strong_spec_inv_norm : forall x, Reduced x -> Reduced (inv_norm x).
Definition div x y := mul x (inv y).
Theorem spec_div x y: [div x y] == [x] / [y].
Definition div_norm x y := mul_norm x (inv_norm y).
Theorem spec_div_norm x y: [div_norm x y] == [x] / [y].
Theorem strong_spec_div_norm : forall x y,
Reduced x -> Reduced y -> Reduced (div_norm x y).
Definition square (x: t): t :=
match x with
| Qz zx => Qz (Z.square zx)
| Qq nx dx => Qq (Z.square nx) (N.square dx)
end.
Theorem spec_square : forall x, [square x] == [x] ^ 2.
Definition power_pos (x : t) p : t :=
match x with
| Qz zx => Qz (Z.power_pos zx p)
| Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
end.
Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p.
Theorem strong_spec_power_pos : forall x p,
Reduced x -> Reduced (power_pos x p).
Definition power (x : t) (z : Z) : t :=
match z with
| Z0 => one
| Zpos p => power_pos x p
| Zneg p => inv (power_pos x p)
end.
Theorem spec_power : forall x z, [power x z] == [x]^z.
Definition power_norm (x : t) (z : Z) : t :=
match z with
| Z0 => one
| Zpos p => power_pos x p
| Zneg p => inv_norm (power_pos x p)
end.
Theorem spec_power_norm : forall x z, [power_norm x z] == [x]^z.
Theorem strong_spec_power_norm : forall x z,
Reduced x -> Reduced (power_norm x z).
Interaction with Qcanon.Qc
Open Scope Qc_scope.
Definition of_Qc q := of_Q (this q).
Definition to_Qc q := !! [q].
Notation "[[ x ]]" := (to_Qc x).
Theorem strong_spec_of_Qc : forall q, [of_Qc q] = q.
Lemma strong_spec_of_Qc_bis : forall q, Reduced (of_Qc q).
Theorem spec_of_Qc: forall q, [[of_Qc q]] = q.
Theorem spec_oppc: forall q, [[opp q]] = -[[q]].
Theorem spec_oppc_bis : forall q : Qc, [opp (of_Qc q)] = - q.
Theorem spec_comparec: forall q1 q2,
compare q1 q2 = ([[q1]] ?= [[q2]]).
Theorem spec_addc x y:
[[add x y]] = [[x]] + [[y]].
Theorem spec_add_normc x y:
[[add_norm x y]] = [[x]] + [[y]].
Theorem spec_add_normc_bis : forall x y : Qc,
[add_norm (of_Qc x) (of_Qc y)] = x+y.
Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]].
Theorem spec_sub_normc x y:
[[sub_norm x y]] = [[x]] - [[y]].
Theorem spec_sub_normc_bis : forall x y : Qc,
[sub_norm (of_Qc x) (of_Qc y)] = x-y.
Theorem spec_mulc x y:
[[mul x y]] = [[x]] * [[y]].
Theorem spec_mul_normc x y:
[[mul_norm x y]] = [[x]] * [[y]].
Theorem spec_mul_normc_bis : forall x y : Qc,
[mul_norm (of_Qc x) (of_Qc y)] = x*y.
Theorem spec_invc x:
[[inv x]] = /[[x]].
Theorem spec_inv_normc x:
[[inv_norm x]] = /[[x]].
Theorem spec_inv_normc_bis : forall x : Qc,
[inv_norm (of_Qc x)] = /x.
Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]].
Theorem spec_div_normc_bis : forall x y : Qc,
[div_norm (of_Qc x) (of_Qc y)] = x/y.
Theorem spec_squarec x: [[square x]] = [[x]]^2.
Theorem spec_power_posc x p:
[[power_pos x p]] = [[x]] ^ nat_of_P p.
End Make.