Library Coq.Numbers.Rational.BigQ.QMake
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
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.